%
\begin{isabellebody}%
\setisabellecontext{ListNat}%
%
\isamarkupsection{Representing lists of natural numbers by natural numbers%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ ListNat\isanewline
\isakeyword{imports}\ Main\ {\isachardoublequoteopen}More{\isachardot}MoreNat{\isachardoublequoteclose}\ {\isachardoublequoteopen}More{\isachardot}MoreBigOperators{\isachardoublequoteclose}\ {\isachardoublequoteopen}More{\isachardot}MoreList{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
In this section, we define of representation of sets of natural
numbers by single natural numbers. The set $\{a_0, a_1, \ldots, a_n\}$
is represented by $2^{a_0} + 2^{a_1} + \ldots + 2^{a_n}$.%
\end{isamarkuptext}\isamarkuptrue%
%
\isamarkupsubsection{sumpows%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
If the set is stored in a distinct list, the function \isa{sumpows{\isadigit{2}}} returns the natural number that represents it.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ sumpows{\isadigit{2}}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ l\ {\isasymequiv}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ l{\isacharparenright}\ {\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}mod{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X{\isacharparenright}\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isadigit{0}}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isacharequal}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ X\ {\isacharequal}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}insert\ {\isadigit{0}}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}insert{\isacharcomma}\ simp{\isacharunderscore}all\ add{\isacharcolon}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ X\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}mod{\isacharcomma}\ auto\ simp\ add{\isacharcolon}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\ power{\isacharunderscore}mod{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}mod{\isacharcomma}\ auto\ simp\ add{\isacharcolon}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\ {\isacharparenleft}rule\ ccontr{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharcircum}\ x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ power{\isacharunderscore}mod\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ unique{\isacharunderscore}sumpows{\isadigit{2}}{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}{\isacharbang}X{\isachardot}\ finite\ X\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ n\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ n{\isacharcolon}{\isacharcolon}nat\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ hyp{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymexists}{\isacharbang}X{\isachardot}\ finite\ X\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}{\isacharbang}X{\isachardot}\ finite\ X\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ X\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ X{\isachardot}\ {\isadigit{2}}\ {\isacharcircum}\ a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}n\ div\ {\isadigit{2}}\ {\isacharless}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ X{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}finite\ X{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ \ X{\isacharprime}\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ X{\isacharprime}{\isacharprime}{\isachardot}\ finite\ X{\isacharprime}{\isacharprime}\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X{\isacharprime}{\isacharprime}\ {\isacharequal}\ n\ div\ {\isadigit{2}}\ {\isasymlongrightarrow}\ X{\isacharprime}{\isacharprime}\ {\isacharequal}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ hyp\ {\isacharbackquoteopen}n\ div\ {\isadigit{2}}\ {\isacharless}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}erule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}n\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharquery}X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{2}}\ {\isacharcircum}\ x{\isacharparenright}\ X{\isacharprime}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ \ X{\isacharprime}\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}distrib{\isacharunderscore}left{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ X\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}mod{\isacharbrackleft}of\ X{\isacharbrackright}\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ x\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharbackquote}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}X\ {\isacharequal}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ {\isacharbackquoteopen}{\isasymforall}\ X{\isacharprime}{\isacharprime}{\isachardot}\ finite\ X{\isacharprime}{\isacharprime}\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X{\isacharprime}{\isacharprime}\ {\isacharequal}\ n\ div\ {\isadigit{2}}\ {\isasymlongrightarrow}\ X{\isacharprime}{\isacharprime}\ {\isacharequal}\ X{\isacharprime}{\isacharbackquoteclose}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharquery}X\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharminus}\ {\isacharparenleft}rule\ ccontr{\isacharcomma}\ auto{\isacharparenright}{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharminus}\ Suc\ {\isadigit{0}}\ {\isacharequal}\ y\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharasterisk}\ sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isadigit{2}}\ {\isacharcircum}\ {\isacharparenleft}x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}\ X\ {\isacharequal}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}distrib{\isacharunderscore}left{\isacharcomma}\ rule\ sum{\isachardot}cong{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x{\isacharcolon}{\isacharcolon}nat\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymin}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharasterisk}\ {\isadigit{2}}\ {\isacharcircum}\ {\isacharparenleft}x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharcircum}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ power{\isacharunderscore}eq{\isacharunderscore}if{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isadigit{2}}\ {\isacharcircum}\ {\isacharparenleft}x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}\ X\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isacharequal}\ op\ {\isacharplus}\ {\isadigit{1}}\ {\isacharbackquote}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharminus}\ {\isadigit{1}}\ {\isasymin}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}image\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ X\ {\isacharequal}\ X{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}rule\ ccontr{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isacharplus}\ {\isadigit{1}}\ {\isacharbackquote}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}x\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{in}\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharparenright}\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x{\isacharprime}{\isacharcolon}{\isacharcolon}nat\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isasymin}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ x\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ x\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}image\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ X\ {\isacharequal}\ X{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymnotin}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ x{\isacharprime}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharquery}X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharcomma}\ subst\ sum{\isachardot}insert{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}op\ {\isacharplus}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymnotin}\ op\ {\isacharplus}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharcircum}\ {\isadigit{0}}\ {\isacharplus}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}op\ {\isacharplus}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharprime}{\isacharparenright}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}op\ {\isacharplus}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharprime}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}x{\isasymin}X{\isacharprime}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{2}}\ {\isacharcircum}\ x{\isacharparenright}\ {\isacharequal}\ n\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}distrib{\isacharunderscore}left{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X{\isacharprime}\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ div{\isacharunderscore}mult{\isacharunderscore}mod{\isacharunderscore}eq{\isacharbrackleft}of\ n\ {\isadigit{2}}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ X\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}mod{\isacharbrackleft}of\ X{\isacharbrackright}\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ x\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharbackquote}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}X\ {\isacharequal}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ {\isacharbackquoteopen}{\isasymforall}\ X{\isacharprime}{\isacharprime}{\isachardot}\ finite\ X{\isacharprime}{\isacharprime}\ {\isasymand}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X{\isacharprime}{\isacharprime}\ {\isacharequal}\ n\ div\ {\isadigit{2}}\ {\isasymlongrightarrow}\ X{\isacharprime}{\isacharprime}\ {\isacharequal}\ X{\isacharprime}{\isacharbackquoteclose}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharquery}X\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharasterisk}\ sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isadigit{2}}\ {\isacharcircum}\ {\isacharparenleft}x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}distrib{\isacharunderscore}left{\isacharcomma}\ rule\ sum{\isachardot}cong{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x{\isacharcolon}{\isacharcolon}nat\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X\ {\isasymand}\ {\isadigit{0}}\ {\isacharless}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharasterisk}\ {\isadigit{2}}\ {\isacharcircum}\ {\isacharparenleft}x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharcircum}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ power{\isacharunderscore}eq{\isacharunderscore}if{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}diff{\isadigit{1}}{\isacharunderscore}nat{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isadigit{2}}\ {\isacharcircum}\ {\isacharparenleft}x\ {\isacharminus}\ Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}X\ {\isacharminus}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ n\ div\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ X\ {\isacharequal}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isacharequal}\ {\isacharquery}X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymnotin}\ op\ {\isacharplus}\ {\isadigit{1}}\ {\isacharbackquote}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharminus}\ {\isadigit{1}}\ {\isasymin}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isacharquery}X\ {\isacharequal}\ X{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isacharplus}\ {\isadigit{1}}\ {\isacharbackquote}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}x\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{in}\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharparenright}\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymnotin}\ image\ {\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ X{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x{\isacharprime}{\isacharcolon}{\isacharcolon}nat\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isasymin}\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ x\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ x\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}X\ {\isacharequal}\ X{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ x{\isacharprime}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isasymin}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}inj{\isacharcolon}\isanewline
\isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ l\ {\isacharequal}\ sumpows{\isadigit{2}}\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isachardoublequoteopen}l\ {\isacharequal}\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ l\ {\isacharequal}\ Sum\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharbackquote}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ distinct{\isacharunderscore}sum{\isacharunderscore}list{\isacharunderscore}conv{\isacharunderscore}Sum{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ l{\isacharprime}\ {\isacharequal}\ Sum\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharbackquote}\ set\ l{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ distinct{\isacharunderscore}sum{\isacharunderscore}list{\isacharunderscore}conv{\isacharunderscore}Sum{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ l{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymSum}{\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharbackquote}\ set\ l{\isacharparenright}\ {\isacharequal}\ {\isasymSum}{\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharbackquote}\ set\ l{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sumpows{\isadigit{2}}\ l\ {\isacharequal}\ sumpows{\isadigit{2}}\ l{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}set\ l{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}set\ l{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ sum{\isachardot}reindex{\isacharcomma}\ simp{\isacharunderscore}all\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}{\isacharplus}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ l\ {\isacharequal}\ set\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ unique{\isacharunderscore}sumpows{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequoteopen}sum\ {\isacharparenleft}op\ {\isacharcircum}\ {\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}set\ l{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}sorted\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ l{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}sorted\ l{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}shift{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ sumpows{\isadigit{2}}\ l\ {\isacharequal}\ sumpows{\isadigit{2}}\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{nat2list%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The function \isa{nat{\isadigit{2}}list} deconstructs the natural number
back to the set it represents (for executability, given by a sorted,
distinct list).%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ k\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ \isanewline
\ \ \ \ \ \ \ \ \ {\isacharbrackleft}{\isacharbrackright}\ \isanewline
\ \ \ \ \ else\ if\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ then\ \isanewline
\ \ \ \ \ \ \ \ \ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}n\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ else\ \isanewline
\ \ \ \ \ \ \ \ \ k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}n\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ nat{\isadigit{2}}list\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nat{\isadigit{2}}list\ n\ {\isasymequiv}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ {\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ k{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isadigit{2}}{\isacharcircum}k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ n\ k\ rule{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharbackquoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mult{\isacharunderscore}eq{\isacharunderscore}if{\isacharbrackleft}of\ n\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharcircum}\ k{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ n\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharbrackleft}of\ n\ {\isadigit{0}}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ x\ k\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ x\ k\ rule{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharunderscore}shift{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ map\ {\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ n\ k\ rule{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharcolon}\isanewline
\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ k{\isacharparenright}\ {\isasymand}\isanewline
\ \ distinct\ {\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ k{\isacharparenright}\ {\isasymand}\isanewline
\ \ {\isacharparenleft}{\isasymforall}\ a\ {\isasymin}\ List{\isachardot}set\ {\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ n\ k{\isacharparenright}{\isachardot}\ a\ {\isasymge}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ rule{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps\ intro{\isacharbang}{\isacharcolon}\ sorted{\isachardot}Cons{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \isanewline
\ \ sorted{\isacharunderscore}nat{\isadigit{2}}list{\isacharcolon}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isanewline
\ \ distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharcolon}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharbrackleft}of\ n\ {\isadigit{0}}{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}unique{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ l\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}l\ {\isacharequal}\ nat{\isadigit{2}}list\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ n{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}inj{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ n{\isachardoublequoteclose}\ l{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}nat{\isadigit{2}}list\ distinct{\isacharunderscore}nat{\isadigit{2}}list\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ x\ k\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ x\ k\ arbitrary{\isacharcolon}\ y\ rule{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ x\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharunderscore}empty{\isacharbrackleft}of\ y\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ x\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ y\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ div\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharunderscore}empty{\isacharbrackleft}of\ {\isachardoublequoteopen}x\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}y\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}y\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ y\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ div\ {\isadigit{2}}\ {\isacharequal}\ y\ div\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}y\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}y\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ y\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharbrackleft}of\ {\isachardoublequoteopen}x\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ x\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}y\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}y\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ y\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isasymin}\ set\ {\isacharparenleft}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}y\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}y\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}{\isacharbackquoteclose}{\isacharbrackleft}THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharbrackleft}of\ {\isachardoublequoteopen}y\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}y\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharhash}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ {\isacharparenleft}x\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}Suc\ k{\isacharparenright}\ {\isacharequal}\ nat{\isadigit{2}}list{\isacharunderscore}aux\ y\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ y\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ del{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ div\ {\isadigit{2}}\ {\isacharequal}\ y\ div\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}y\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ x\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ y\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}nat{\isadigit{2}}list{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}inj\ nat{\isadigit{2}}list{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ x\ {\isacharequal}\ nat{\isadigit{2}}list\ y{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharprime}{\isacharbrackleft}of\ x\ {\isadigit{0}}\ y{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}even{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}nat{\isadigit{2}}list\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ map\ {\isacharparenleft}op\ {\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}unique{\isacharbrackleft}of\ {\isachardoublequoteopen}map\ {\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{2}}{\isacharasterisk}n{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ {\isachardoublequoteopen}n{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}shift{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ n{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}nat{\isadigit{2}}list\ sorted{\isacharunderscore}map\ distinct{\isacharunderscore}nat{\isadigit{2}}list\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}odd{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}nat{\isadigit{2}}list\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}\ {\isacharhash}\ map\ {\isacharparenleft}op\ {\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}\ div\ {\isadigit{2}}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}aux{\isacharunderscore}shift\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{list2nat%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Although the function \isa{sumpows{\isadigit{2}}} converts a set (given
by a distinct list) to its representing natural number, we define the
function \isa{list{\isadigit{2}}nat} that does the same, but is somewhat more
efficient.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure\ {\isacharparenleft}l{\isacharcomma}\ i{\isacharcomma}\ s{\isacharcomma}\ r{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ {\isacharparenleft}case\ l\ of\ \isanewline
\ \ \ \ \ \ \ \ \ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\isanewline
\ \ \ \ \ \ \ {\isacharbar}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isasymRightarrow}\ if\ i\ {\isachargreater}\ h\ then\ {\isadigit{0}}\ else\ Max\ {\isacharparenleft}set\ l{\isacharparenright}\ {\isacharminus}\ i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{function}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}list{\isadigit{2}}nat{\isacharunderscore}aux\ {\isacharbrackleft}{\isacharbrackright}\ i\ s\ r\ {\isacharequal}\ r{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}list{\isadigit{2}}nat{\isacharunderscore}aux\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ i\ s\ r\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ {\isacharparenleft}if\ i\ {\isacharequal}\ h\ then\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ list{\isadigit{2}}nat{\isacharunderscore}aux\ t\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}s{\isacharparenright}\ {\isacharparenleft}s\ {\isacharplus}\ r{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ \ else\ if\ i\ {\isacharless}\ h\ then\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ list{\isadigit{2}}nat{\isacharunderscore}aux\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}s{\isacharparenright}\ r\isanewline
\ \ \ \ \ \ \ \ \ else\ r{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ h\ i\ s\ r\ {\isacharcolon}{\isacharcolon}\ nat\ \isakeyword{and}\ t\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isacharequal}\ h{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure\ {\isacharparenleft}t{\isacharcomma}\ i\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}\ {\isacharasterisk}\ s{\isacharcomma}\ s\ {\isacharplus}\ r{\isacharparenright}\ {\isacharless}\ \isanewline
\ \ \ \ \ \ \ \ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharcomma}\ i{\isacharcomma}\ s{\isacharcomma}\ r{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ t{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharequal}\ h{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h{\isacharprime}\ t{\isacharprime}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharequal}\ h{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Max{\isacharunderscore}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}set\ t{\isacharprime}{\isachardoublequoteclose}\ h{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}t{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}t{\isacharcomma}\ i\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}\ {\isacharasterisk}\ s{\isacharcomma}\ s\ {\isacharplus}\ r{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharcomma}\ i{\isacharcomma}\ s{\isacharcomma}\ r{\isacharparenright}{\isacharparenright}\ {\isasymin}\ measure\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ h\ i\ s\ r{\isacharcolon}{\isacharcolon}nat\ \isakeyword{and}\ t\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isasymnoteq}\ h{\isachardoublequoteclose}\ {\isachardoublequoteopen}i\ {\isacharless}\ h{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}h\ {\isacharhash}\ t{\isacharcomma}\ i\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}\ {\isacharasterisk}\ s{\isacharcomma}\ r{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharcomma}\ i{\isacharcomma}\ s{\isacharcomma}\ r{\isacharparenright}{\isacharparenright}\ {\isasymin}\ measure\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}measure{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Max{\isacharunderscore}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}set\ t{\isachardoublequoteclose}\ h{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}t\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ list{\isadigit{2}}nat\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}list{\isadigit{2}}nat\ l\ {\isacharequal}\ list{\isadigit{2}}nat{\isacharunderscore}aux\ l\ {\isadigit{0}}\ {\isadigit{1}}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}sumpows{\isadigit{2}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}s\ {\isacharequal}\ {\isadigit{2}}\ {\isacharcircum}\ i{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}l\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ i\ {\isasymle}\ hd\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}list{\isadigit{2}}nat{\isacharunderscore}aux\ l\ i\ s\ r\ {\isacharequal}\ r\ {\isacharplus}\ sumpows{\isadigit{2}}\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ i\ s\ r\ rule{\isacharcolon}\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ i\ s\ r{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{2}}\ h\ t\ i\ s\ r{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}h\ {\isacharequal}\ i{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}t\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ i\ {\isacharplus}\ {\isadigit{1}}\ {\isasymle}\ hd\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{2}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ t{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isacharequal}\ i{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{2}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}i\ {\isacharless}\ h{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{2}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ {\isacharbackquoteopen}h\ {\isasymnoteq}\ i{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymnoteq}\ i{\isacharbackquoteclose}\ {\isadigit{2}}{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}sumpows{\isadigit{2}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}list{\isadigit{2}}nat\ l\ {\isacharequal}\ sumpows{\isadigit{2}}\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}aux{\isacharunderscore}sumpows{\isadigit{2}}{\isacharbrackleft}of\ {\isadigit{1}}\ {\isadigit{0}}\ l\ {\isadigit{0}}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}list{\isadigit{2}}nat{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ {\isacharparenleft}list{\isadigit{2}}nat\ l{\isacharparenright}\ {\isacharequal}\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ list{\isadigit{2}}nat{\isacharunderscore}sumpows{\isadigit{2}}{\isacharbrackleft}of\ l{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sumpows{\isadigit{2}}{\isacharunderscore}nat{\isadigit{2}}list{\isacharunderscore}unique{\isacharbrackleft}of\ l\ {\isachardoublequoteopen}list{\isadigit{2}}nat\ l{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}list{\isadigit{2}}nat{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isadigit{2}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}list{\isadigit{2}}nat\ l{\isadigit{1}}\ {\isacharequal}\ list{\isadigit{2}}nat\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}l{\isadigit{1}}\ {\isacharequal}\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sumpows{\isadigit{2}}\ l{\isadigit{1}}\ {\isacharequal}\ sumpows{\isadigit{2}}\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isadigit{2}}nat{\isacharunderscore}sumpows{\isadigit{2}}{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ sumpows{\isadigit{2}}{\isacharunderscore}inj{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
