--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tphols-2011/generated/List_Prefix.tex	Mon Jan 24 11:29:55 2011 +0000
@@ -0,0 +1,1578 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{List{\isacharunderscore}Prefix}%
+%
+\isamarkupheader{List prefixes and postfixes%
+}
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ List{\isacharunderscore}Prefix\isanewline
+\isakeyword{imports}\ List\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsubsection{Prefix order on lists%
+}
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ order\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ prefix{\isacharunderscore}def\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys\ {\isacharequal}\ {\isacharparenleft}xs\ {\isasymle}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ intro{\isacharunderscore}classes\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def\ strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{end}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ prefixI\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ zs\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ prefixE\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{obtains}\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ assms\ \isacommand{unfolding}\isamarkupfalse%
+\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}prefixI{\isacharprime}\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ z\ {\isacharhash}\ zs\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}prefixE{\isacharprime}\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{obtains}\ z\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ z\ {\isacharhash}\ zs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ {\isacharbackquoteopen}xs\ {\isacharless}\ ys{\isacharbackquoteclose}\ \isacommand{obtain}\isamarkupfalse%
+\ us\ \isakeyword{where}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ us{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast\isanewline
+\ \ \isacommand{with}\isamarkupfalse%
+\ that\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ neq{\isacharunderscore}Nil{\isacharunderscore}conv{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}prefixI\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymnoteq}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}prefixE\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ xs\ ys\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{obtains}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ assms\ \isacommand{unfolding}\isamarkupfalse%
+\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Basic properties of prefixes%
+}
+\isamarkuptrue%
+\isacommand{theorem}\isamarkupfalse%
+\ Nil{\isacharunderscore}prefix\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{theorem}\isamarkupfalse%
+\ prefix{\isacharunderscore}Nil\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ prefix{\isacharunderscore}snoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isasymor}\ xs\ {\isasymle}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ zs\ \isakeyword{where}\ zs{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isacharequal}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isasymor}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ butlast{\isacharunderscore}append\ butlast{\isacharunderscore}snoc\ prefixI\ zs{\isacharparenright}\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isacharequal}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isasymor}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ order{\isacharunderscore}eq{\isacharunderscore}iff\ strict{\isacharunderscore}prefixE\ strict{\isacharunderscore}prefixI{\isacharprime}\ xt{\isadigit{1}}{\isacharparenleft}{\isadigit{7}}{\isacharparenright}{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ Cons{\isacharunderscore}prefix{\isacharunderscore}Cons\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs\ {\isasymle}\ y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isasymle}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ same{\isacharunderscore}prefix{\isacharunderscore}prefix\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys\ {\isasymle}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}ys\ {\isasymle}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ same{\isacharunderscore}prefix{\isacharunderscore}nil\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys\ {\isasymle}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ append{\isacharunderscore}self{\isacharunderscore}conv\ order{\isacharunderscore}eq{\isacharunderscore}iff\ prefixI{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ prefix{\isacharunderscore}prefix\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymle}\ ys\ {\isacharat}\ zs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ order{\isacharunderscore}le{\isacharunderscore}less{\isacharunderscore}trans\ prefixI\ strict{\isacharunderscore}prefixE\ strict{\isacharunderscore}prefixI{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ append{\isacharunderscore}prefixD{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharat}\ ys\ {\isasymle}\ zs\ {\isasymLongrightarrow}\ xs\ {\isasymle}\ zs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{theorem}\isamarkupfalse%
+\ prefix{\isacharunderscore}Cons{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}zs{\isachardot}\ xs\ {\isacharequal}\ y\ {\isacharhash}\ zs\ {\isasymand}\ zs\ {\isasymle}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ xs{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{theorem}\isamarkupfalse%
+\ prefix{\isacharunderscore}append{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ ys\ {\isacharat}\ zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isasymle}\ ys\ {\isasymor}\ {\isacharparenleft}{\isasymexists}us{\isachardot}\ xs\ {\isacharequal}\ ys\ {\isacharat}\ us\ {\isasymand}\ us\ {\isasymle}\ zs{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}induct\ zs\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
+\ \ \ \isacommand{apply}\isamarkupfalse%
+\ force\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}assoc\ add{\isacharcolon}\ append{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}eq{\isacharunderscore}appendI{\isacharparenright}\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ append{\isacharunderscore}one{\isacharunderscore}prefix{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ length\ xs\ {\isacharless}\ length\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ {\isacharbrackleft}ys\ {\isacharbang}\ length\ xs{\isacharbrackright}\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ prefix{\isacharunderscore}def\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ Cons{\isacharunderscore}eq{\isacharunderscore}appendI\ append{\isacharunderscore}eq{\isacharunderscore}appendI\ append{\isacharunderscore}eq{\isacharunderscore}conv{\isacharunderscore}conj\isanewline
+\ \ \ \ eq{\isacharunderscore}Nil{\isacharunderscore}appendI\ nth{\isacharunderscore}drop{\isacharprime}{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{theorem}\isamarkupfalse%
+\ prefix{\isacharunderscore}length{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ length\ xs\ {\isasymle}\ length\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ prefix{\isacharunderscore}same{\isacharunderscore}cases{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}xs\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ xs\isactrlisub {\isadigit{2}}\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ xs\isactrlisub {\isadigit{1}}\ {\isasymle}\ xs\isactrlisub {\isadigit{2}}\ {\isasymor}\ xs\isactrlisub {\isadigit{2}}\ {\isasymle}\ xs\isactrlisub {\isadigit{1}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}eq{\isacharunderscore}append{\isacharunderscore}conv{\isadigit{2}}{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ set{\isacharunderscore}mono{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ set\ xs\ {\isasymsubseteq}\ set\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ take{\isacharunderscore}is{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}take\ n\ xs\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ map{\isacharunderscore}prefixI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ map\ f\ xs\ {\isasymle}\ map\ f\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ prefix{\isacharunderscore}length{\isacharunderscore}less{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys\ {\isasymLongrightarrow}\ length\ xs\ {\isacharless}\ length\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp{\isacharcolon}\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ prefix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}prefix{\isacharunderscore}simps\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}xs\ {\isacharless}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isacharless}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ cong{\isacharcolon}\ conj{\isacharunderscore}cong{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ take{\isacharunderscore}strict{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys\ {\isasymLongrightarrow}\ take\ n\ xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}induct\ n\ arbitrary{\isacharcolon}\ xs\ ys{\isacharparenright}\isanewline
+\ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}case{\isacharunderscore}tac\ ys{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}metis\ order{\isacharunderscore}less{\isacharunderscore}trans\ strict{\isacharunderscore}prefixI\ take{\isacharunderscore}is{\isacharunderscore}prefix{\isacharparenright}\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ not{\isacharunderscore}prefix{\isacharunderscore}cases{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ pfx{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ ps\ {\isasymle}\ ls{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{obtains}\isanewline
+\ \ \ \ {\isacharparenleft}c{\isadigit{1}}{\isacharparenright}\ {\isachardoublequoteopen}ps\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}ls\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isacharparenleft}c{\isadigit{2}}{\isacharparenright}\ a\ as\ x\ xs\ \isakeyword{where}\ {\isachardoublequoteopen}ps\ {\isacharequal}\ a{\isacharhash}as{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}ls\ {\isacharequal}\ x{\isacharhash}xs{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isacharequal}\ a{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymnot}\ as\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isacharparenleft}c{\isadigit{3}}{\isacharparenright}\ a\ as\ x\ xs\ \isakeyword{where}\ {\isachardoublequoteopen}ps\ {\isacharequal}\ a{\isacharhash}as{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}ls\ {\isacharequal}\ x{\isacharhash}xs{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ a{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}cases\ ps{\isacharparenright}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ Nil\ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{using}\isamarkupfalse%
+\ pfx\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ {\isacharparenleft}Cons\ a\ as{\isacharparenright}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ c\ {\isacharequal}\ {\isacharbackquoteopen}ps\ {\isacharequal}\ a{\isacharhash}as{\isacharbackquoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}cases\ ls{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ Nil\ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ pfx\ c{\isadigit{1}}\ same{\isacharunderscore}prefix{\isacharunderscore}nil{\isacharparenright}\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ {\isacharparenleft}Cons\ x\ xs{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\isanewline
+\ \ \ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isacharequal}\ a{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
+\ True\isanewline
+\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymnot}\ as\ {\isasymle}\ xs{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
+\ pfx\ c\ Cons\ True\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
+\ c\ Cons\ True\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ c{\isadigit{2}}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
+\ False\isanewline
+\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
+\ c\ Cons\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ c{\isadigit{3}}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ not{\isacharunderscore}prefix{\isacharunderscore}induct\ {\isacharbrackleft}consumes\ {\isadigit{1}}{\isacharcomma}\ case{\isacharunderscore}names\ Nil\ Neq\ Eq{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ np{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ ps\ {\isasymle}\ ls{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ base{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ xs{\isachardot}\ P\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ r{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ xs\ y\ ys{\isachardot}\ x\ {\isasymnoteq}\ y\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}y{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ r{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ xs\ y\ ys{\isachardot}\ {\isasymlbrakk}\ x\ {\isacharequal}\ y{\isacharsemicolon}\ {\isasymnot}\ xs\ {\isasymle}\ ys{\isacharsemicolon}\ P\ xs\ ys\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}y{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}P\ ps\ ls{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ np\isanewline
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}induct\ ls\ arbitrary{\isacharcolon}\ ps{\isacharparenright}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ Nil\ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp{\isacharcolon}\ neq{\isacharunderscore}Nil{\isacharunderscore}conv\ elim{\isacharbang}{\isacharcolon}\ not{\isacharunderscore}prefix{\isacharunderscore}cases\ intro{\isacharbang}{\isacharcolon}\ base{\isacharparenright}\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ {\isacharparenleft}Cons\ y\ ys{\isacharparenright}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ npfx{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ ps\ {\isasymle}\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ x\ xs\ \isakeyword{where}\ pv{\isacharcolon}\ {\isachardoublequoteopen}ps\ {\isacharequal}\ x\ {\isacharhash}\ xs{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ not{\isacharunderscore}prefix{\isacharunderscore}cases{\isacharparenright}\ auto\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ Cons{\isachardot}hyps\ Cons{\isacharunderscore}prefix{\isacharunderscore}Cons\ npfx\ pv\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Parallel lists%
+}
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ parallel\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymparallel}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymparallel}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ xs\ {\isasymle}\ ys\ {\isasymand}\ {\isasymnot}\ ys\ {\isasymle}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallelI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ {\isasymnot}\ ys\ {\isasymle}\ xs\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallelE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{obtains}\ {\isachardoublequoteopen}{\isasymnot}\ xs\ {\isasymle}\ ys\ {\isasymand}\ {\isasymnot}\ ys\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ assms\ \isacommand{unfolding}\isamarkupfalse%
+\ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{theorem}\isamarkupfalse%
+\ prefix{\isacharunderscore}cases{\isacharcolon}\isanewline
+\ \ \isakeyword{obtains}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\ {\isacharbar}\ {\isachardoublequoteopen}ys\ {\isacharless}\ xs{\isachardoublequoteclose}\ {\isacharbar}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ parallel{\isacharunderscore}def\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{theorem}\isamarkupfalse%
+\ parallel{\isacharunderscore}decomp{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ {\isasymexists}as\ b\ bs\ c\ cs{\isachardot}\ b\ {\isasymnoteq}\ c\ {\isasymand}\ xs\ {\isacharequal}\ as\ {\isacharat}\ b\ {\isacharhash}\ bs\ {\isasymand}\ ys\ {\isacharequal}\ as\ {\isacharat}\ c\ {\isacharhash}\ cs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ Nil\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ False\ \isacommand{by}\isamarkupfalse%
+\ auto\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ {\isacharparenleft}snoc\ x\ xs{\isacharparenright}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}rule\ prefix{\isacharunderscore}cases{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ le{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ ys{\isacharprime}\ \isakeyword{where}\ ys{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ ys{\isacharprime}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\isanewline
+\ \ \ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}cases\ ys{\isacharprime}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}ys{\isacharprime}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ parallelE\ prefixI\ snoc{\isachardot}prems\ ys{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ c\ cs\ \isacommand{assume}\isamarkupfalse%
+\ ys{\isacharprime}{\isacharcolon}\ {\isachardoublequoteopen}ys{\isacharprime}\ {\isacharequal}\ c\ {\isacharhash}\ cs{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\isanewline
+\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ Cons{\isacharunderscore}eq{\isacharunderscore}appendI\ eq{\isacharunderscore}Nil{\isacharunderscore}appendI\ parallelE\ prefixI\isanewline
+\ \ \ \ \ \ \ \ \ \ same{\isacharunderscore}prefix{\isacharunderscore}prefix\ snoc{\isachardot}prems\ ys{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}ys\ {\isacharless}\ xs{\isachardoublequoteclose}\ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}ys\ {\isasymle}\ xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ snoc\ \isacommand{have}\isamarkupfalse%
+\ False\ \isacommand{by}\isamarkupfalse%
+\ blast\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ snoc\ \isacommand{obtain}\isamarkupfalse%
+\ as\ b\ bs\ c\ cs\ \isakeyword{where}\ neq{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}b{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharparenright}\ {\isasymnoteq}\ c{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ xs{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ as\ {\isacharat}\ b\ {\isacharhash}\ bs{\isachardoublequoteclose}\ \isakeyword{and}\ ys{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ as\ {\isacharat}\ c\ {\isacharhash}\ cs{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ blast\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ xs\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ as\ {\isacharat}\ b\ {\isacharhash}\ {\isacharparenleft}bs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ neq\ ys\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ blast\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallel{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymparallel}\ b\ {\isasymLongrightarrow}\ a\ {\isacharat}\ c\ {\isasymparallel}\ b\ {\isacharat}\ d{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}rule\ parallelI{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}erule\ parallelE{\isacharcomma}\ erule\ conjE{\isacharcomma}\isanewline
+\ \ \ \ \ \ induct\ rule{\isacharcolon}\ not{\isacharunderscore}prefix{\isacharunderscore}induct{\isacharcomma}\ simp{\isacharplus}{\isacharparenright}{\isacharplus}\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallel{\isacharunderscore}appendI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ xs\ {\isacharat}\ xs{\isacharprime}\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ ys\ {\isacharat}\ ys{\isacharprime}\ {\isasymLongrightarrow}\ x\ {\isasymparallel}\ y{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ parallel{\isacharunderscore}append{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallel{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymparallel}\ b\ {\isasymlongleftrightarrow}\ b\ {\isasymparallel}\ a{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Postfix order on lists%
+}
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ postfix\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequoteclose}\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isacharslash}\ {\isachargreater}{\isachargreater}{\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{5}}{\isadigit{1}}{\isacharcomma}\ {\isadigit{5}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}zs{\isachardot}\ xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfixI\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ postfix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfixE\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{obtains}\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ assms\ \isacommand{unfolding}\isamarkupfalse%
+\ postfix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}refl\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isacharsemicolon}\ ys\ {\isachargreater}{\isachargreater}{\isacharequal}\ zs{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ zs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}antisym{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isacharsemicolon}\ ys\ {\isachargreater}{\isachargreater}{\isacharequal}\ xs{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ Nil{\isacharunderscore}postfix\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}Nil\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isachargreater}{\isachargreater}{\isacharequal}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}ConsI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ x{\isacharhash}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}ConsD{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ y{\isacharhash}ys\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}appendI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ zs\ {\isacharat}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}appendD{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ zs\ {\isacharat}\ ys\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}is{\isacharunderscore}subset{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ set\ ys\ {\isasymsubseteq}\ set\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ zs{\isacharparenright}\ auto\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}ConsD{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}x{\isacharhash}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ y{\isacharhash}ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x{\isacharhash}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ y{\isacharhash}ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}x{\isacharhash}xs\ {\isacharequal}\ zs\ {\isacharat}\ y{\isacharhash}ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ zs{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharbang}{\isacharcolon}\ postfix{\isacharunderscore}appendI\ postfix{\isacharunderscore}ConsI{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}to{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymlongleftrightarrow}\ rev\ ys\ {\isasymle}\ rev\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ xs\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ zs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ ys\ {\isacharless}{\isacharequal}\ rev\ xs{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ ys\ {\isacharless}{\isacharequal}\ rev\ xs{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}rev\ xs\ {\isacharequal}\ rev\ ys\ {\isacharat}\ zs{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ zs\ {\isacharat}\ rev\ {\isacharparenleft}rev\ ys{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isacharequal}\ rev\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ distinct{\isacharunderscore}postfix{\isacharcolon}\ {\isachardoublequoteopen}distinct\ xs\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ distinct\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}clarsimp\ elim{\isacharbang}{\isacharcolon}\ postfixE{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}map{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ map\ f\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ map\ f\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto\ elim{\isacharbang}{\isacharcolon}\ postfixE\ intro{\isacharcolon}\ postfixI{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}drop{\isacharcolon}\ {\isachardoublequoteopen}as\ {\isachargreater}{\isachargreater}{\isacharequal}\ drop\ n\ as{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ postfix{\isacharunderscore}def\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}rule\ exI\ {\isacharbrackleft}\isakeyword{where}\ x\ {\isacharequal}\ {\isachardoublequoteopen}take\ n\ as{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ postfix{\isacharunderscore}take{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ xs\ {\isacharequal}\ take\ {\isacharparenleft}length\ xs\ {\isacharminus}\ length\ ys{\isacharparenright}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}clarsimp\ elim{\isacharbang}{\isacharcolon}\ postfixE{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallelD{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymparallel}\ y\ {\isasymLongrightarrow}\ {\isasymnot}\ x\ {\isasymle}\ y{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallelD{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymparallel}\ y\ {\isasymLongrightarrow}\ {\isasymnot}\ y\ {\isasymle}\ x{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallel{\isacharunderscore}Nil{\isadigit{1}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ x\ {\isasymparallel}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ parallel{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymparallel}\ x{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ Cons{\isacharunderscore}parallelI{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymnoteq}\ b\ {\isasymLongrightarrow}\ a\ {\isacharhash}\ as\ {\isasymparallel}\ b\ {\isacharhash}\ bs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ Cons{\isacharunderscore}parallelI{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ a\ {\isacharequal}\ b{\isacharsemicolon}\ as\ {\isasymparallel}\ bs\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a\ {\isacharhash}\ as\ {\isasymparallel}\ b\ {\isacharhash}\ bs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}metis\ Cons{\isacharunderscore}prefix{\isacharunderscore}Cons\ parallelE\ parallelI{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ not{\isacharunderscore}equal{\isacharunderscore}is{\isacharunderscore}parallel{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ neq{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ len{\isacharcolon}\ {\isachardoublequoteopen}length\ xs\ {\isacharequal}\ length\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ len\ neq\isanewline
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}induct\ rule{\isacharcolon}\ list{\isacharunderscore}induct{\isadigit{2}}{\isacharparenright}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ Nil\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ {\isacharparenleft}Cons\ a\ as\ b\ bs{\isacharparenright}\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ ih{\isacharcolon}\ {\isachardoublequoteopen}as\ {\isasymnoteq}\ bs\ {\isasymLongrightarrow}\ as\ {\isasymparallel}\ bs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ fact\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}cases\ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ True\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}as\ {\isasymnoteq}\ bs{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
+\ Cons\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ Cons{\isacharunderscore}parallelI{\isadigit{2}}\ {\isacharbrackleft}OF\ True\ ih{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ False\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ Cons{\isacharunderscore}parallelI{\isadigit{1}}{\isacharparenright}\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Executable code%
+}
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ less{\isacharunderscore}eq{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ list{\isacharparenright}\ {\isasymle}\ xs\ {\isasymlongleftrightarrow}\ True{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharhash}\ xs\ {\isasymle}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ False{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharhash}\ xs\ {\isasymle}\ y\ {\isacharhash}\ ys\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ less{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}xs\ {\isacharless}\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ list{\isacharparenright}\ {\isasymlongleftrightarrow}\ False{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}{\isacharhash}\ xs\ {\isasymlongleftrightarrow}\ True{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharhash}\ xs\ {\isacharless}\ y\ {\isacharhash}\ ys\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemmas}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}\ {\isacharequal}\ postfix{\isacharunderscore}to{\isacharunderscore}prefix\isanewline
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: