%
\begin{isabellebody}%
\setisabellecontext{MoreList}%
%
\isamarkupsection{Auxiliary lemmas about lists%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ MoreList\isanewline
\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ex{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ l{\isachardot}\ distinct\ l\ {\isasymand}\ set\ l\ {\isacharequal}\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ A{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ empty\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}insert\ x\ A{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ l\ \isakeyword{where}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ l\ {\isacharequal}\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}x\ {\isacharhash}\ l{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isacharparenleft}x\ {\isacharhash}\ l{\isacharparenright}\ {\isacharequal}\ insert\ x\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ map{\isacharunderscore}of{\isacharunderscore}sort{\isacharunderscore}key{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ P{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}map{\isacharunderscore}of\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}of\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ext{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}map{\isacharunderscore}of\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharparenright}\ x\ {\isacharequal}\ map{\isacharunderscore}of\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}\ x{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ P{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ f\ x{\isacharparenright}\ {\isasymin}\ set\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ f\ x{\isacharparenright}\ {\isasymin}\ set\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}zip\ in{\isacharunderscore}set{\isacharunderscore}conv{\isacharunderscore}nth{\isacharparenright}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}map\ fst\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ P{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def\ set{\isacharunderscore}zip\ intro{\isacharcolon}\ distinct{\isacharunderscore}zipI{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ P{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Some{\isacharunderscore}eq{\isacharunderscore}map{\isacharunderscore}of{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ x{\isachardoublequoteclose}\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Some{\isacharunderscore}eq{\isacharunderscore}map{\isacharunderscore}of{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ x{\isachardoublequoteclose}\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}map{\isacharunderscore}of\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}\ x\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}map{\isacharunderscore}of\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharparenright}\ x\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ map{\isacharunderscore}of{\isacharunderscore}eq{\isacharunderscore}None{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isachardoublequoteclose}\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ map{\isacharunderscore}of{\isacharunderscore}eq{\isacharunderscore}None{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharasterisk}{\isacharcomma}\ subst\ {\isacharasterisk}{\isacharparenright}\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}first{\isacharunderscore}min{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlbrakk}sorted\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isasymin}\ set\ xs{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymle}\ x{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs\ arbitrary{\isacharcolon}\ x{\isacharparenright}{\isacharparenleft}auto{\isacharcomma}\ force{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}tl{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}sorted\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ sorted\ xs{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{context}\isamarkupfalse%
\ linorder\isanewline
\isakeyword{begin}\isanewline
\isacommand{inductive}\isamarkupfalse%
\ sorted{\isacharunderscore}desc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ Nil\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}sorted{\isacharunderscore}desc\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ Cons{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}y{\isasymin}set\ xs{\isachardot}\ x\ {\isasymge}\ y\ {\isasymLongrightarrow}\ sorted{\isacharunderscore}desc\ xs\ {\isasymLongrightarrow}\ sorted{\isacharunderscore}desc\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{end}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}desc{\isacharunderscore}single\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}sorted{\isacharunderscore}desc\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sorted{\isacharunderscore}desc{\isachardot}Cons{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}desc{\isacharunderscore}many{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymge}\ y\ {\isasymLongrightarrow}\ sorted{\isacharunderscore}desc\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isasymLongrightarrow}\ sorted{\isacharunderscore}desc\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sorted{\isacharunderscore}desc{\isachardot}Cons{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}y\ {\isacharhash}\ zs{\isachardoublequoteclose}\ rule{\isacharcolon}\ sorted{\isacharunderscore}desc{\isachardot}cases{\isacharcomma}\ auto{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}desc{\isacharunderscore}many{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharcomma}\ code{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}sorted{\isacharunderscore}desc\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}\ {\isasymlongleftrightarrow}\ x\ {\isasymge}\ y\ {\isasymand}\ sorted{\isacharunderscore}desc\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ intro{\isacharcolon}\ sorted{\isacharunderscore}desc{\isacharunderscore}many\ elim{\isacharcolon}\ sorted{\isacharunderscore}desc{\isachardot}cases{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}desc{\isacharunderscore}first{\isacharunderscore}max{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}sorted{\isacharunderscore}desc\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isasymin}\ set\ xs{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymge}\ x{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs\ arbitrary{\isacharcolon}\ x{\isacharparenright}{\isacharparenleft}auto{\isacharcomma}\ force{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}desc{\isacharunderscore}tl{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}sorted{\isacharunderscore}desc\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ sorted{\isacharunderscore}desc\ xs{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}sorted{\isacharunderscore}desc{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequoteopen}sorted\ xs\ {\isacharequal}\ sorted{\isacharunderscore}desc\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}append\ elim{\isacharcolon}\ sorted{\isacharunderscore}desc{\isachardot}cases{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}negate{\isacharcolon}\ {\isachardoublequoteopen}sorted\ xs\ {\isacharequal}\ sorted{\isacharunderscore}desc\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linordered{\isacharunderscore}ab{\isacharunderscore}group{\isacharunderscore}add{\isachardot}\ {\isacharminus}\ x{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ x\ xs{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}tl{\isacharbrackleft}of\ x\ xs{\isacharbrackright}\ sorted{\isacharunderscore}desc{\isacharunderscore}tl{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharminus}x{\isachardoublequoteclose}\ {\isachardoublequoteopen}map\ uminus\ xs{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}first{\isacharunderscore}min{\isacharbrackleft}of\ x\ xs{\isacharbrackright}\ sorted{\isacharunderscore}desc{\isacharunderscore}first{\isacharunderscore}max{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharminus}x{\isachardoublequoteclose}\ {\isachardoublequoteopen}map\ uminus\ xs{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ intro{\isacharbang}{\isacharcolon}\ sorted{\isacharunderscore}desc{\isachardot}Cons\ sorted{\isachardot}Cons{\isacharparenright}\ force\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}rev{\isacharunderscore}uminus{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ l{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharcolon}{\isacharcolon}linordered{\isacharunderscore}ab{\isacharunderscore}group{\isacharunderscore}add{\isacharparenright}\ list{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}rev\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ {\isacharminus}\ b{\isacharparenright}\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sorted{\isacharunderscore}sorted{\isacharunderscore}desc{\isacharunderscore}rev{\isacharparenright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}negate{\isacharbrackleft}of\ {\isachardoublequoteopen}map\ snd\ {\isacharparenleft}sort{\isacharunderscore}key\ snd\ l{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ comp{\isacharunderscore}def\ split{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}takeWhile{\isacharunderscore}snd{\isacharunderscore}neg{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharcolon}{\isacharcolon}linordered{\isacharunderscore}ab{\isacharunderscore}group{\isacharunderscore}add{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}U\ {\isacharequal}\ sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ P{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}f\ A\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}A{\isacharcomma}\ f\ A{\isacharparenright}\ {\isasymin}\ set\ {\isacharparenleft}takeWhile\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ b\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}\ U{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}rev\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ {\isacharminus}\ b{\isacharparenright}\ U{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}rev{\isacharunderscore}uminus\ {\isacharbackquoteopen}U\ {\isacharequal}\ sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ filter{\isacharunderscore}equals{\isacharunderscore}takeWhile{\isacharunderscore}sorted{\isacharunderscore}rev{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ {\isacharminus}b{\isachardoublequoteclose}\ {\isachardoublequoteopen}U{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{0}}{\isachardoublequoteclose}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ set\ P{\isacharbackquoteclose}\ {\isacharbackquoteopen}f\ A\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}U\ {\isacharequal}\ sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ {\isacharparenleft}map\ f\ P{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ split{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ zip{\isacharunderscore}map{\isadigit{2}}\ zip{\isacharunderscore}same{\isacharunderscore}conv{\isacharunderscore}map{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}map{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ x\ y{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ f\ x\ {\isasymle}\ f\ y{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}map\ f\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ subset{\isacharunderscore}card{\isacharunderscore}length{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ set\ l{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ l\ {\isacharequal}\ card\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isacharequal}\ set\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ List{\isachardot}finite{\isacharunderscore}set\ card{\isacharunderscore}length\ card{\isacharunderscore}seteq{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ length{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}set\ l\ {\isacharequal}\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ l\ {\isacharequal}\ card\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ X\ arbitrary{\isacharcolon}\ l{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ empty\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}insert\ a\ l{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ l\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ insert{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ insert{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}remove{\isadigit{1}}\ a\ l{\isachardoublequoteclose}{\isacharbrackright}\ insert{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ insert{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ insert{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}remove{\isadigit{1}}\ length{\isacharunderscore}remove{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ l\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ arith\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ length{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ X{\isacharparenright}\ {\isacharequal}\ card\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ X{\isacharbrackright}\ length{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharprime}{\isacharbrackleft}of\ X\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ X{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharunderscore}inj{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ y{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ x\ {\isacharequal}\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ y{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ set\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ x{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isacharequal}\ set\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ x{\isacharbrackright}\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ y{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ x{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ x\ {\isacharequal}\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ length{\isacharunderscore}filter{\isacharunderscore}less\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}length\ {\isacharbrackleft}l{\isasymleftarrow}list\ {\isachardot}\ P\ l{\isacharbrackright}\ {\isacharless}\ Suc\ {\isacharparenleft}length\ list{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ length{\isacharunderscore}filter{\isacharunderscore}le{\isacharbrackleft}of\ P\ list{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ arith%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ exists{\isacharunderscore}zip{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ set\ L{\isacharprime}{\isachardot}\ y\ {\isacharequal}\ f\ x\ {\isasymLongrightarrow}\ \ L{\isacharprime}\ {\isacharequal}\ zip\ {\isacharparenleft}map\ fst\ L{\isacharprime}{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}map\ fst\ L{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ nth{\isacharunderscore}equalityI{\isacharparenright}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ set\ L{\isacharprime}{\isachardot}\ y\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ i\ {\isacharless}\ length\ L{\isacharprime}{\isachardot}\ L{\isacharprime}\ {\isacharbang}\ i\ {\isacharequal}\ {\isacharparenleft}zip\ {\isacharparenleft}map\ fst\ L{\isacharprime}{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}map\ fst\ L{\isacharprime}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ i\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isacharless}\ length\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}snd\ {\isacharparenleft}L{\isacharprime}\ {\isacharbang}\ i{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}fst\ {\isacharparenleft}L{\isacharprime}\ {\isacharbang}\ i{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ set\ L{\isacharprime}{\isachardot}\ y\ {\isacharequal}\ f\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ in{\isacharunderscore}set{\isacharunderscore}conv{\isacharunderscore}nth{\isacharbrackleft}of\ {\isachardoublequoteopen}L{\isacharprime}\ {\isacharbang}\ i{\isachardoublequoteclose}\ L{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isacharbang}\ i\ {\isacharequal}\ zip\ {\isacharparenleft}map\ fst\ L{\isacharprime}{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}map\ fst\ L{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharless}\ length\ L{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ surjective{\isacharunderscore}pairing{\isacharbrackleft}of\ {\isachardoublequoteopen}L{\isacharprime}\ {\isacharbang}\ i{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}fst{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ set\ l{\isachardot}\ y\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ fst\ {\isacharparenleft}set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\ split{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}b\ {\isacharequal}\ f\ aa{\isachardoublequoteclose}{\isacharcomma}\ auto{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ distinct{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}sorted{\isacharunderscore}elems{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}i\ {\isasymnoteq}\ j{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}i\ {\isacharless}\ length\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}j\ {\isacharless}\ length\ F{\isachardoublequoteclose}\ \isanewline
\ \ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ List{\isachardot}set\ F{\isachardot}\ distinct\ l\ {\isasymand}\ sorted\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}List{\isachardot}set\ {\isacharparenleft}F\ {\isacharbang}\ i{\isacharparenright}\ {\isasymnoteq}\ List{\isachardot}set\ {\isacharparenleft}F\ {\isacharbang}\ j{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ nth{\isacharunderscore}eq{\isacharunderscore}iff{\isacharunderscore}index{\isacharunderscore}eq{\isacharbrackleft}of\ F\ i\ j{\isacharbrackright}\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isacharbang}\ i{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isacharbang}\ j{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ drop{\isacharunderscore}nth\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}drop{\isacharunderscore}nth\ n\ l\ {\isacharequal}\ {\isacharparenleft}take\ n\ l{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}drop\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ distinct{\isacharunderscore}drop{\isacharunderscore}nth{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}drop{\isacharunderscore}nth\ i\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{unfolding}\isamarkupfalse%
\ drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}take{\isacharunderscore}disj{\isacharunderscore}set{\isacharunderscore}drop{\isacharunderscore}if{\isacharunderscore}distinct{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ length{\isacharunderscore}drop{\isacharunderscore}nth{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}i\ {\isacharless}\ length\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ {\isacharparenleft}drop{\isacharunderscore}nth\ i\ l{\isacharparenright}\ {\isacharequal}\ length\ l\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}i\ {\isacharless}\ length\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}drop{\isacharunderscore}nth\ i\ l{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}l\ {\isacharbang}\ i{\isacharbraceright}\ {\isacharequal}\ set\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}drop{\isacharunderscore}nth\ i\ l{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}l\ {\isacharbang}\ i{\isacharbraceright}\ {\isasymsubseteq}\ set\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ \isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharcolon}\ in{\isacharunderscore}set{\isacharunderscore}takeD\ in{\isacharunderscore}set{\isacharunderscore}dropD{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ l\ {\isasymsubseteq}\ set\ {\isacharparenleft}drop{\isacharunderscore}nth\ i\ l{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}l\ {\isacharbang}\ i{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ id{\isacharunderscore}take{\isacharunderscore}nth{\isacharunderscore}drop{\isacharbrackleft}of\ i\ l{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}i\ {\isacharless}\ length\ l{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}drop{\isacharunderscore}nth\ i\ l{\isacharparenright}\ {\isacharequal}\ set\ l\ {\isacharminus}\ {\isacharbraceleft}l\ {\isacharbang}\ i{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}take\ i\ l\ {\isacharat}\ l\ {\isacharbang}\ i\ {\isacharhash}\ \ drop\ {\isacharparenleft}Suc\ i{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}i\ {\isacharless}\ length\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ id{\isacharunderscore}take{\isacharunderscore}nth{\isacharunderscore}drop{\isacharbrackleft}of\ i\ l{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}l\ {\isacharbang}\ i\ {\isasymnotin}\ set\ {\isacharparenleft}take\ i\ l{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}l\ {\isacharbang}\ i\ {\isasymnotin}\ set\ {\isacharparenleft}drop\ {\isacharparenleft}Suc\ i{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharbrackleft}of\ i\ l{\isacharbrackright}\ {\isacharbackquoteopen}i\ {\isacharless}\ length\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ \ {\isacharparenleft}auto\ dest{\isacharcolon}\ in{\isacharunderscore}set{\isacharunderscore}takeD\ in{\isacharunderscore}set{\isacharunderscore}dropD{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ spread\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}spread\ w\ l\ {\isacharequal}\ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}w{\isacharcomma}\ a{\isacharparenright}{\isachardot}\ replicate\ w\ a{\isacharparenright}\ {\isacharparenleft}zip\ w\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ length{\isacharunderscore}spread{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}length\ w\ {\isacharequal}\ length\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ {\isacharparenleft}spread\ w\ l{\isacharparenright}\ {\isacharequal}\ sum{\isacharunderscore}list\ w{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}length\ {\isasymcirc}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ replicate\ x\ y{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}zip\ w\ l{\isacharparenright}\ {\isacharequal}\ w{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ w\ arbitrary{\isacharcolon}\ l{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ w{\isadigit{0}}\ w{\isacharprime}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ l{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ spread{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ length{\isacharunderscore}concat{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}spread{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}set\ {\isacharparenleft}spread\ w\ l{\isacharparenright}\ {\isasymsubseteq}\ set\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ spread{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}zip{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}spread\ {\isacharparenleft}w\ {\isacharhash}\ w{\isacharprime}{\isacharparenright}\ {\isacharparenleft}l\ {\isacharhash}\ l{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}replicate\ w\ l{\isacharparenright}\ {\isacharat}\ spread\ w{\isacharprime}\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ spread{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}sum{\isacharunderscore}list\ {\isacharparenleft}replicate\ wi\ li{\isacharparenright}\ {\isacharequal}\ int\ wi\ {\isacharasterisk}\ li{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ wi{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ int{\isacharunderscore}distrib{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ listsum{\isacharunderscore}spread{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}length\ w\ {\isacharequal}\ length\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sum{\isacharunderscore}list\ {\isacharparenleft}spread\ w\ l{\isacharparenright}\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ int\ x\ {\isacharasterisk}\ y{\isacharparenright}\ {\isacharparenleft}zip\ w\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ w\ arbitrary{\isacharcolon}\ l{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ spread{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ wi\ w{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ {\isacharparenleft}wi\ {\isacharhash}\ w{\isacharprime}{\isacharparenright}\ {\isacharequal}\ length\ l{\isacharbackquoteclose}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ li\ l{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}l\ {\isacharequal}\ li\ {\isacharhash}\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ l{\isacharparenright}\ auto\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ l{\isacharprime}{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l\ {\isacharequal}\ li\ {\isacharhash}\ l{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ map{\isacharunderscore}spread{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}spread\ w\ l{\isacharparenright}\ {\isacharequal}\ spread\ w\ {\isacharparenleft}map\ f\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ spread{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ map{\isacharunderscore}concat\ comp{\isacharunderscore}def\ split{\isacharunderscore}def\ zip{\isacharunderscore}map{\isadigit{2}}{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ inc{\isacharunderscore}nth\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ n\ {\isasymequiv}\ L{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ Suc\ {\isacharparenleft}L\ {\isacharbang}\ n{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ take{\isacharunderscore}inc{\isacharunderscore}nth\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}k\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}take\ k\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharparenright}\ {\isacharequal}\ take\ k\ L{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ take{\isacharunderscore}prefix{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}k\ {\isasymle}\ k{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}take\ k{\isacharprime}\ L\ {\isacharequal}\ take\ k{\isacharprime}\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}take\ k\ L\ {\isacharequal}\ take\ k\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ min{\isachardot}absorb{\isadigit{1}}\ take{\isacharunderscore}take{\isacharparenright}%
\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:
