%
\begin{isabellebody}%
\setisabellecontext{LPartitioningImpl}%
%
\isamarkupsubsection{Implementation by sorted and distinct lists%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioningImpl\isanewline
\isakeyword{imports}\ LPartitioning\ FamilyImpl\ NonIsomorphicFamiliesImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ A\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isacharparenleft}let\ F{\isacharprime}\ {\isacharequal}\ {\isacharbrackleft}f\ {\isasymleftarrow}\ F{\isachardot}\ A\ {\isasymnotin}\ set\ f\ {\isasymand}\ P\ A\ f{\isacharbrackright}\ in\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ A\ {\isacharhash}\ x{\isacharparenright}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sdff\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}dmf\ FFb\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}dmf\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ A{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}correctness{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ FFb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ list\ list{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sdff\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ FFb\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymAnd}\ A\ F{\isachardot}\ {\isasymlbrakk}sd\ A{\isacharsemicolon}\ sdf\ F{\isacharsemicolon}\ dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ A\ F\ {\isasymlongleftrightarrow}\ P{\isacharprime}\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ A{\isacharparenright}\ {\isacharequal}\ mult{\isacharunderscore}P\ P{\isacharprime}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ {\isacharparenleft}set\ A{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isasymsubseteq}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F\ \isakeyword{where}\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymnotin}\ set\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}P\ A\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ insert\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharbackquote}\ set\ FFb{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ set\ FFb{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ A\ {\isasymnotin}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ set\ FFb{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymnotin}\ set\ F{\isacharbackquoteclose}\ SetImpl{\isacharunderscore}lists{\isachardot}set{\isacharunderscore}set{\isacharbrackleft}of\ F\ A{\isacharbrackright}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}P{\isacharprime}\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}\ {\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sd\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}sdff\ FFb{\isacharbackquoteclose}\ {\isacharbackquoteopen}F\ {\isasymin}\ set\ FFb{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}dmf\ FFb\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}P\ A\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{5}}{\isacharparenright}{\isacharbrackleft}of\ A\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}rhs\ {\isasymsubseteq}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F\ \isakeyword{where}\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A\ {\isasymnotin}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}P{\isacharprime}\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F\ {\isasymunion}\ {\isacharbraceleft}set\ A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{5}}{\isacharparenright}{\isacharbrackleft}of\ A\ F{\isacharbrackright}\ {\isacharbackquoteopen}sdff\ FFb{\isacharbackquoteclose}\ {\isacharbackquoteopen}sd\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}dmf\ FFb\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ image{\isacharunderscore}eqI{\isacharbrackleft}\isakeyword{where}\ x{\isacharequal}\ {\isachardoublequoteopen}F{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m\ {\isacharequal}\ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ mult{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ A{\isacharparenright}\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sdff\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardot}\ sdff\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharparenright}\ \isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharbrackleft}of\ F\ A\ P{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}dmf\ FFb\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}dmf\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ n\ m{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
{\isacharparenleft}simp\ del{\isacharcolon}\ SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def{\isacharcomma}\ rule\ ballI{\isacharcomma}\ rule\ ballI{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ A\ F\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ A{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}dm\ F\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharbrackleft}OF\ assms{\isacharcomma}\ of\ A\ P{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharbrackleft}of\ n\ m{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}correctness{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ FFb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ list\ list{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sdff\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ FFb\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}{\isasymAnd}\ A\ F{\isachardot}\ {\isasymlbrakk}sd\ A{\isacharsemicolon}\ sdf\ F{\isacharsemicolon}\ dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ A\ F\ {\isasymlongleftrightarrow}\ P{\isacharprime}\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ n\ m{\isacharparenright}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}P\ P{\isacharprime}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ n\ m{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isasymsubseteq}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharbrackleft}of\ n\ m{\isacharbrackright}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}correctness{\isacharbrackleft}\isakeyword{where}\ P{\isacharequal}P\ \isakeyword{and}\ P{\isacharprime}{\isacharequal}P{\isacharprime}{\isacharcomma}\ OF\ {\isacharunderscore}\ {\isacharunderscore}\ {\isacharunderscore}\ {\isacharunderscore}\ assms{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}rhs\ {\isasymsubseteq}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ mult{\isacharunderscore}P\ P{\isacharprime}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ Al\ \isakeyword{where}\ {\isachardoublequoteopen}Al\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ Al\ {\isacharequal}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}sorted\ Al\ {\isasymand}\ distinct\ Al{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ m{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}completeness\ {\isacharbrackleft}of\ A\ m\ n{\isacharbrackright}\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}sorted{\isacharunderscore}distinct\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ mult{\isacharunderscore}P\ P{\isacharprime}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ {\isacharparenleft}set\ Al{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ mult{\isacharunderscore}P\ P{\isacharprime}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Al\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharbackquoteopen}sd\ Al{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}correctness{\isacharbrackleft}symmetric{\isacharcomma}\ of\ FFb\ Al\ n\ P\ P{\isacharprime}{\isacharcomma}\ OF\ {\isacharunderscore}\ {\isacharunderscore}\ {\isacharunderscore}\ {\isacharunderscore}\ assms{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m\ perms\ {\isacharequal}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ perms\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sdff\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isachardot}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}subset{\isacharbrackleft}of\ perms\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}dmf\ F\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}dmf\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m\ perms{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}dmf\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isachardot}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}subset{\isacharbrackleft}of\ perms\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ P\ F\ n\ m{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}correctness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}{\isasymAnd}\ A\ F{\isachardot}\ {\isasymlbrakk}sd\ A{\isacharsemicolon}\ sdf\ F{\isacharsemicolon}\ dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ Pinc{\isacharprime}\ A\ F\ {\isasymlongleftrightarrow}\ Pinc\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ Pinc\ P\ {\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ Pinc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}sdff\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ FFb\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}p{\isasymin}set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}length\ L\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}FFb{\isacharprime}\ {\isacharequal}\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb{\isacharprime}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharplus}{\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharplus}{\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharbrackleft}\isakeyword{where}\ FFb{\isacharprime}{\isacharequal}{\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ n{\isacharequal}n\ \isakeyword{and}\ L{\isacharequal}L\ \isakeyword{and}\ k{\isacharequal}k\ \isakeyword{and}\ P{\isacharequal}P\ \isakeyword{and}\ FFb{\isacharequal}{\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isachardoublequoteclose}\ \isakeyword{and}\ Pinc{\isacharequal}{\isachardoublequoteopen}Pinc{\isachardoublequoteclose}{\isacharcomma}\ OF\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ L\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact{\isacharplus}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}P\ Pinc\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FFb{\isacharparenright}\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}correctness{\isacharbrackleft}of\ FFb\ n\ Pinc{\isacharprime}\ Pinc{\isacharcomma}\ OF\ assms{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\ \isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ Pinc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ assms{\isacharparenleft}{\isadigit{9}}{\isacharparenright}{\isacharparenright}{\isacharplus}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ \isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharunderscore}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{6}}{\isacharparenright}{\isacharcomma}\ of\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{5}}{\isacharparenright}{\isacharcomma}\ of\ Pinc{\isacharprime}\ {\isachardoublequoteopen}length\ L{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Recursive enumeration procedure%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
For a given list L, find an iso-representing collection of all L-paritioned families that
satisfy some predicate P.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ dec{\isacharunderscore}last\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}dec{\isacharunderscore}last\ L\ {\isasymequiv}\ butlast\ L\ {\isacharat}\ {\isacharbrackleft}last\ L\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{function}\isamarkupfalse%
\ enum{\isacharunderscore}rec\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec\ L\ v{\isadigit{0}}\ f\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ {\isacharparenleft}if\ L\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ v{\isadigit{0}}\ \isanewline
\ \ \ \ \ \ \ else\ if\ last\ L\ {\isacharequal}\ {\isadigit{0}}\ then\ enum{\isacharunderscore}rec\ {\isacharparenleft}butlast\ L{\isacharparenright}\ v{\isadigit{0}}\ f\ \isanewline
\ \ \ \ \ \ \ else\ f\ {\isacharparenleft}enum{\isacharunderscore}rec\ {\isacharparenleft}dec{\isacharunderscore}last\ L{\isacharparenright}\ v{\isadigit{0}}\ f{\isacharparenright}\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}R\ {\isacharequal}\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}L{\isacharcomma}\ {\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardot}\ length\ L\ {\isacharplus}\ sum{\isacharunderscore}list\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharparenleft}relation\ {\isachardoublequoteopen}{\isacharquery}R{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list{\isachardoublequoteclose}\ \isakeyword{and}\ v{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{and}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}last\ L\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sum{\isacharunderscore}list\ L\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}butlast\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ append{\isacharunderscore}butlast{\isacharunderscore}last{\isacharunderscore}id{\isacharbrackleft}of\ L{\isacharcomma}\ symmetric{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}butlast\ L{\isacharcomma}\ v{\isadigit{0}}{\isacharcomma}\ f{\isacharparenright}{\isacharcomma}\ L{\isacharcomma}\ v{\isadigit{0}}{\isacharcomma}\ f{\isacharparenright}\ \ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ list{\isachardoublequoteclose}\ \isakeyword{and}\ v{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{and}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}last\ L\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sum{\isacharunderscore}list\ L\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}butlast\ L{\isacharparenright}\ {\isacharplus}\ last\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}list{\isacharunderscore}append{\isacharbrackleft}of\ {\isachardoublequoteopen}butlast\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}last\ L{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ append{\isacharunderscore}butlast{\isacharunderscore}last{\isacharunderscore}id{\isacharbrackleft}of\ L{\isacharcomma}\ symmetric{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}butlast\ L\ {\isacharat}\ {\isacharbrackleft}last\ L\ {\isacharminus}\ {\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ v{\isadigit{0}}{\isacharcomma}\ f{\isacharparenright}{\isacharcomma}\ L{\isacharcomma}\ v{\isadigit{0}}{\isacharcomma}\ f{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}last\ L\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{declare}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}P\ v{\isadigit{0}}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymAnd}\ v\ L{\isachardot}\ P\ v\ L\ {\isasymLongrightarrow}\ P\ v\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymAnd}\ v\ L{\isacharprime}{\isacharcolon}{\isacharcolon}{\isacharparenleft}nat\ list{\isacharparenright}{\isachardot}\ {\isasymlbrakk}L{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ last\ L{\isacharprime}\ {\isachargreater}\ {\isadigit{0}}{\isacharsemicolon}\ length\ L{\isacharprime}\ {\isasymle}\ length\ L{\isacharsemicolon}\ P\ v\ {\isacharparenleft}dec{\isacharunderscore}last\ L{\isacharprime}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}f\ v\ L{\isacharprime}{\isacharparenright}\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}P\ {\isacharparenleft}enum{\isacharunderscore}rec\ L\ v{\isadigit{0}}\ f{\isacharparenright}\ L{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ L\ v{\isadigit{0}}\ f\ rule{\isacharcolon}\ enum{\isacharunderscore}rec{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ L\ v{\isadigit{0}}\ f{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}L\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ enum{\isacharunderscore}rec{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}last\ L\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isachardot}simps{\isacharbrackleft}of\ L\ v{\isadigit{0}}\ f{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}OF\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}last\ L\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}enum{\isacharunderscore}rec\ {\isacharparenleft}butlast\ L{\isacharparenright}\ v{\isadigit{0}}\ f{\isachardoublequoteclose}\ {\isachardoublequoteopen}butlast\ L{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ append{\isacharunderscore}butlast{\isacharunderscore}last{\isacharunderscore}id{\isacharbrackleft}of\ L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isachardot}simps{\isacharbrackleft}of\ L\ v{\isadigit{0}}\ f{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}OF\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}last\ L\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ append{\isacharunderscore}butlast{\isacharunderscore}last{\isacharunderscore}id\ length{\isacharunderscore}append{\isacharunderscore}singleton\ neq{\isadigit{0}}{\isacharunderscore}conv\ order{\isacharunderscore}refl{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}{\isasymAnd}\ A\ F{\isachardot}\ {\isasymlbrakk}sd\ A{\isacharsemicolon}\ sdf\ F{\isacharsemicolon}\ dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ Pinc{\isacharprime}\ A\ F\ {\isasymlongleftrightarrow}\ Pinc\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ Pinc\ P{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ Pinc{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}p{\isasymin}set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}length\ L\ {\isacharminus}\ {\isadigit{1}}\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}P\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Mult\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}\ F\ L{\isachardot}\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ F\ n\ {\isacharparenleft}length\ L\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharparenleft}enum{\isacharunderscore}rec\ L\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ Mult{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}\ X\ L{\isachardot}\ iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ X{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharparenright}\ {\isasymand}\ sdff\ X\ {\isasymand}\ dmf\ X\ n{\isachardoublequoteclose}{\isacharcomma}\ THEN\ conjunct{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ sdff\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ {\isasymand}\ dmf\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ n{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharquery}X\ {\isacharquery}Y\ {\isasymand}\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Y\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zero{\isacharbrackleft}of\ {\isadigit{6}}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharcomma}\ symmetric{\isacharbrackright}\ {\isacharbackquoteopen}P\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ iso{\isacharunderscore}represents{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ v\ L\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ v{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharparenright}\ {\isasymand}\ sdff\ v\ {\isasymand}\ dmf\ v\ n{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ v{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isasymand}\ sdff\ v\ {\isasymand}\ dmf\ v\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zero\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ v\ \isakeyword{and}\ L{\isacharprime}{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ list{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}last\ L{\isacharprime}\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ L{\isacharprime}\ {\isasymle}\ length\ L{\isachardoublequoteclose}\ \isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}length\ {\isacharparenleft}butlast\ L{\isacharprime}{\isacharparenright}\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ L\ {\isacharminus}\ {\isadigit{1}}\ {\isasymle}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ v{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}dec{\isacharunderscore}last\ L{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isasymand}\ sdff\ v\ {\isasymand}\ dmf\ v\ n{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}sdff\ v{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ v\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ v{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}dec{\isacharunderscore}last\ L{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}butlast\ L{\isacharprime}\ {\isacharat}\ {\isacharbrackleft}last\ L{\isacharprime}\ {\isacharminus}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ assms{\isacharparenleft}{\isadigit{7}}{\isacharparenright}{\isacharparenright}{\isacharplus}\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}correctness{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharminus}{\isadigit{3}}{\isacharparenright}\ {\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharminus}{\isadigit{2}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ auto{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}T{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}last\ L{\isacharprime}\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}\ {\isasymand}\ dmf\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharbrackleft}of\ v\ Pinc{\isacharprime}\ n\ {\isachardoublequoteopen}length\ L{\isacharprime}\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ perms{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharbrackleft}of\ v\ n\ Pinc{\isacharprime}\ {\isachardoublequoteopen}length\ L{\isacharprime}\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ perms{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ assms{\isacharparenleft}{\isadigit{7}}{\isacharparenright}{\isacharparenright}{\isacharplus}\ blast\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharprime}{\isacharparenright}\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ sdff\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}\ {\isasymand}\ dmf\ {\isacharparenleft}Mult\ v\ L{\isacharprime}{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Dynamic programming enumeration procedure%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ pwge{\isacharunderscore}impl\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}pwge{\isacharunderscore}impl\ L\ L{\isacharprime}\ {\isasymlongleftrightarrow}\ list{\isacharunderscore}all\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isasymge}\ y{\isacharparenright}\ {\isacharparenleft}zip\ L\ L{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}impl{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}length\ L\ {\isacharequal}\ length\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}pwge{\isacharunderscore}impl\ L\ L{\isacharprime}\ {\isasymlongleftrightarrow}\ L\ {\isasymsucceq}\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}impl{\isacharunderscore}def\ pwge{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isacharunderscore}iff\ set{\isacharunderscore}zip{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{function}\isamarkupfalse%
\ enum{\isacharunderscore}dp\ \isakeyword{where}\ \isanewline
\ {\isachardoublequoteopen}enum{\isacharunderscore}dp\ val\ res\ k\ L\ g\ stop\ maxL\ {\isacharequal}\ foldl\isanewline
\ \ \ \ \ \ {\isacharparenleft}{\isasymlambda}\ r\ n{\isachardot}\ let\ l\ {\isacharequal}\ inc{\isacharunderscore}nth\ L\ n\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ if\ length\ l\ {\isasymnoteq}\ length\ maxL\ {\isasymor}\ stop\ l\ {\isasymor}\ {\isasymnot}\ pwge{\isacharunderscore}impl\ maxL\ l\ then\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ enum{\isacharunderscore}dp\ {\isacharparenleft}g\ val\ n{\isacharparenright}\ r\ n\ l\ g\ stop\ maxL\isanewline
\ \ \ \ \ \ {\isacharparenright}\isanewline
\ \ \ \ \ \ {\isacharparenleft}val\ {\isacharhash}\ res{\isacharparenright}\isanewline
\ \ \ \ \ \ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}step\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ res\ k\ g\ stop\ maxL\ L\ {\isasymequiv}\ let\ l\ {\isacharequal}\ inc{\isacharunderscore}nth\ L\ k\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ if\ length\ l\ {\isasymnoteq}\ length\ maxL\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ stop\ l\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymnot}\ pwge{\isacharunderscore}impl\ maxL\ l\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ res\ else\ enum{\isacharunderscore}dp\ {\isacharparenleft}g\ val\ k{\isacharparenright}\ res\ k\ l\ g\ stop\ maxL{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ listdiff\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}listdiff\ xs\ ys\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ a\ {\isacharminus}\ b{\isacharparenright}\ {\isacharparenleft}zip\ xs\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}val{\isacharcomma}\ res{\isacharcomma}\ k{\isacharcomma}\ L{\isacharcomma}\ g{\isacharcomma}\ stop{\isacharcomma}\ maxL{\isacharparenright}{\isachardot}\ listdiff\ {\isacharparenleft}map\ {\isacharparenleft}op{\isacharplus}{\isadigit{1}}{\isacharparenright}\ maxL{\isacharparenright}\ L{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ \isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ val\ res\ k\ L\ g\ stop\ maxL\ r\ n\ l\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}l\ {\isacharequal}\ inc{\isacharunderscore}nth\ L\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}n\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{and}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}length\ l\ {\isasymnoteq}\ length\ maxL\ {\isasymor}\ stop\ l\ {\isasymor}\ {\isasymnot}\ pwge{\isacharunderscore}impl\ maxL\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ x{\isachardot}\ x\ {\isacharless}\ length\ maxL\ {\isasymlongrightarrow}\ l\ {\isacharbang}\ x\ {\isasymle}\ maxL\ {\isacharbang}\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ l\ {\isacharequal}\ length\ maxL{\isachardoublequoteclose}\ {\isachardoublequoteopen}n\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharbackquoteopen}n\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}impl{\isacharunderscore}def\ list{\isacharunderscore}all{\isacharunderscore}iff\ set{\isacharunderscore}zip{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}length\ maxL{\isacharbraceright}{\isachardot}\isanewline
\ \ \ \ \ \ \ \ \ \ Suc\ {\isacharparenleft}maxL\ {\isacharbang}\ x{\isacharparenright}\ {\isacharminus}\ inc{\isacharunderscore}nth\ L\ n\ {\isacharbang}\ x\ {\isasymle}\ Suc\ {\isacharparenleft}maxL\ {\isacharbang}\ x{\isacharparenright}\ {\isacharminus}\ L\ {\isacharbang}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isacharless}length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Suc\ {\isacharparenleft}maxL\ {\isacharbang}\ n{\isacharparenright}\ {\isacharminus}\ inc{\isacharunderscore}nth\ L\ n\ {\isacharbang}\ n\ {\isacharless}\ Suc\ {\isacharparenleft}maxL\ {\isacharbang}\ n{\isacharparenright}\ {\isacharminus}\ L\ {\isacharbang}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n\ {\isacharless}length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}l\ {\isacharequal}\ inc{\isacharunderscore}nth\ L\ n{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}list{\isacharunderscore}update\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}listdiff\ {\isacharparenleft}map\ {\isacharparenleft}op{\isacharplus}{\isadigit{1}}{\isacharparenright}\ maxL{\isacharparenright}\ l\ {\isacharless}\ listdiff\ {\isacharparenleft}map\ {\isacharparenleft}op{\isacharplus}{\isadigit{1}}{\isacharparenright}\ maxL{\isacharparenright}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l\ {\isacharequal}\ inc{\isacharunderscore}nth\ L\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ l\ {\isacharequal}\ length\ maxL{\isacharbackquoteclose}\ {\isacharbackquoteopen}n\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ listdiff{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff\ sum{\isacharunderscore}list{\isacharunderscore}sum{\isacharunderscore}nth\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharparenright}\isanewline
\ \ \ \ \ {\isacharparenleft}rule\ sum{\isacharunderscore}strict{\isacharunderscore}mono{\isacharunderscore}ex{\isadigit{1}}{\isacharcomma}\ auto{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}g\ val\ n{\isacharcomma}\ r{\isacharcomma}\ n{\isacharcomma}\ l{\isacharcomma}\ g{\isacharcomma}\ stop{\isacharcomma}\ maxL{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}val{\isacharcomma}\ res{\isacharcomma}\ k{\isacharcomma}\ L{\isacharcomma}\ g{\isacharcomma}\ stop{\isacharcomma}\ maxL{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isasymin}\ measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}val{\isacharcomma}\ res{\isacharcomma}\ k{\isacharcomma}\ L{\isacharcomma}\ g{\isacharcomma}\ stop{\isacharcomma}\ maxL{\isacharparenright}{\isachardot}\ listdiff\ {\isacharparenleft}map\ {\isacharparenleft}op{\isacharplus}{\isadigit{1}}{\isacharparenright}\ maxL{\isacharparenright}\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{declare}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mono{\isacharcolon}\isanewline
\isakeyword{assumes}\ {\isachardoublequoteopen}length\ L\ {\isacharequal}\ length\ maxL{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ \ {\isachardoublequoteopen}set\ {\isacharparenleft}val\ {\isacharhash}\ res{\isacharparenright}\ {\isasymsubseteq}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp\ val\ res\ k\ L\ g\ stop\ maxL{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ val\ res\ k\ L\ g\ stop\ maxL\ rule{\isacharcolon}\ enum{\isacharunderscore}dp{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ val\ res\ k\ L\ g\ stop\ maxL{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ enum{\isacharunderscore}dp{\isachardot}simps{\isacharcomma}\ subst\ foldl{\isacharunderscore}conv{\isacharunderscore}fold{\isacharcomma}\ rule\ fold{\isacharunderscore}invariant{\isacharbrackleft}\isakeyword{where}\ Q{\isacharequal}{\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\ s\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isacharparenleft}val\ {\isacharhash}\ res{\isacharparenright}\ {\isasymsubseteq}\ set\ s{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}val\ {\isacharhash}\ res{\isacharparenright}\ {\isasymsubseteq}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ s\ x\ g\ stop\ maxL\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ x\ {\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ x{\isachardoublequoteclose}\ s{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mono{\isacharprime}{\isacharcolon}\isanewline
\isakeyword{assumes}\ {\isachardoublequoteopen}length\ L\ {\isacharequal}\ length\ maxL{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isachardoublequoteopen}set\ res\ {\isasymsubseteq}\ set\ {\isacharparenleft}foldl\ {\isacharparenleft}{\isasymlambda}\ r\ n{\isachardot}\ enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ r\ n\ g\ stop\ maxL\ L{\isacharparenright}\ res\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ foldl{\isacharunderscore}conv{\isacharunderscore}fold{\isacharcomma}\ rule\ fold{\isacharunderscore}invariant{\isacharbrackleft}\isakeyword{where}\ Q{\isacharequal}{\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ s\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ res\ {\isasymsubseteq}\ set\ s{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ res\ {\isasymsubseteq}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ s\ x\ g\ stop\ maxL\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mono{\isacharbrackleft}\isakeyword{where}\ val\ {\isacharequal}\ {\isachardoublequoteopen}g\ val\ x{\isachardoublequoteclose}\ \isakeyword{and}\ res{\isacharequal}s\ \isakeyword{and}\ k{\isacharequal}x\ \isakeyword{and}\ L{\isacharequal}{\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ x{\isachardoublequoteclose}\ \isakeyword{and}\ g{\isacharequal}g\ \isakeyword{and}\ stop{\isacharequal}stop\ \isakeyword{and}\ maxL{\isacharequal}maxL{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}lemma{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}length\ L\ {\isacharequal}\ length\ maxL{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}\ {\isachargreater}\ k\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isachardoublequoteopen}X\ {\isacharequal}\ {\isacharbraceleft}L{\isacharprime}{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ L\ {\isasymand}\ maxL\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ take\ k\ L{\isacharprime}\ {\isacharequal}\ take\ k\ L\ {\isasymand}\ {\isasymnot}\ {\isacharparenleft}{\isasymexists}\ Ls{\isachardot}\ Ls\ {\isasymsucceq}\ L\ {\isasymand}\ take\ k\ L\ {\isacharequal}\ take\ k\ Ls\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ stop\ Ls{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isachardoublequoteopen}P\ val\ L{\isachardoublequoteclose}\ \isakeyword{and}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}k\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ \isakeyword{and}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}{\isasymAnd}\ val\ L\ k{\isacharprime}{\isachardot}\ {\isasymlbrakk}P\ val\ L{\isacharsemicolon}\ \ k{\isacharprime}\ {\isacharless}\ length\ L{\isacharsemicolon}\ k{\isacharprime}\ {\isacharless}\ length\ maxL{\isacharsemicolon}\ {\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}\ {\isachargreater}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline
\ \ \ \ \ \ \ \ P\ {\isacharparenleft}g\ val\ k{\isacharprime}{\isacharparenright}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ L{\isacharprime}\ {\isasymin}\ X{\isachardot}\ {\isasymexists}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp\ val\ res\ k\ L\ g\ stop\ maxL{\isacharparenright}{\isachardot}\ P\ B\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ val\ res\ k\ L\ g\ stop\ maxL\ arbitrary{\isacharcolon}\ X\ rule{\isacharcolon}\ enum{\isacharunderscore}dp{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ val\ res\ k\ L\ g\ stop\ maxL{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}take\ k\ L{\isacharprime}\ {\isacharequal}\ take\ k\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}\ Ls{\isachardot}\ Ls\ {\isasymsucceq}\ L\ {\isasymand}\ take\ k\ L\ {\isacharequal}\ take\ k\ Ls\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ stop\ Ls{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}B{\isasymin}set\ {\isacharparenleft}enum{\isacharunderscore}dp\ val\ res\ k\ L\ g\ stop\ maxL{\isacharparenright}{\isachardot}\ P\ B\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}L\ {\isacharequal}\ L{\isacharprime}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mono{\isacharbrackleft}of\ L\ maxL\ val\ res\ k\ g\ stop{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ k{\isacharprime}{\isachardot}\ k{\isacharprime}\ {\isasymge}\ k\ {\isasymand}\ k{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymand}\ take\ k{\isacharprime}\ L{\isacharprime}\ {\isacharequal}\ take\ k{\isacharprime}\ L\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}\ {\isachargreater}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}take\ k\ L{\isacharprime}\ {\isacharequal}\ take\ k\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ {\isachardoublequoteopen}length\ L\ {\isacharminus}\ k{\isachardoublequoteclose}\ arbitrary{\isacharcolon}\ k{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Suc\ p{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ inc{\isacharunderscore}nth\ L\ k{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Suc{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ Suc{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}k{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isacharbang}\ k\ {\isacharequal}\ L\ {\isacharbang}\ k{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ L\ {\isacharequal}\ length\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ Suc{\isacharunderscore}diff{\isacharunderscore}Suc\ Suc{\isacharunderscore}leI\ Suc{\isacharunderscore}neq{\isacharunderscore}Zero\ diff{\isacharunderscore}is{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}eq\ linorder{\isacharunderscore}cases\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharunderscore}eq\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharunderscore}neq{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Suc\ k\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymnoteq}\ L{\isacharprime}{\isacharbackquoteclose}\ Suc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ list{\isacharunderscore}eq{\isacharunderscore}iff{\isacharunderscore}nth{\isacharunderscore}eq{\isacharbrackleft}of\ L\ L{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ less{\isacharunderscore}linear\ less{\isacharunderscore}trans{\isacharunderscore}Suc\ nth{\isacharunderscore}take{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}take\ {\isacharparenleft}Suc\ k{\isacharparenright}\ L{\isacharprime}\ {\isacharequal}\ take\ {\isacharparenleft}Suc\ k{\isacharparenright}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ take{\isacharunderscore}Suc{\isacharunderscore}conv{\isacharunderscore}app{\isacharunderscore}nth{\isacharbrackleft}of\ k\ L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ take{\isacharunderscore}Suc{\isacharunderscore}conv{\isacharunderscore}app{\isacharunderscore}nth{\isacharbrackleft}of\ k\ L{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}p\ {\isacharequal}\ length\ L\ {\isacharminus}\ Suc\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharbackquoteopen}Suc\ k\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}{\isachargreater}Suc\ k\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ k{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}k{\isacharprime}\ {\isasymge}\ Suc\ k{\isachardoublequoteclose}\ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}take\ k{\isacharprime}\ L{\isacharprime}\ {\isacharequal}\ take\ k{\isacharprime}\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}\ {\isachargreater}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Suc\ k\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}k{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ k{\isacharprime}\ \isakeyword{where}\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}k{\isacharprime}\ {\isasymge}\ k{\isachardoublequoteclose}\ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}take\ k{\isacharprime}\ L{\isacharprime}\ {\isacharequal}\ take\ k{\isacharprime}\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}\ {\isachargreater}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}l\ {\isacharequal}\ {\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X{\isacharprime}{\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}L{\isacharprime}{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ {\isacharquery}l\ {\isasymand}\ maxL\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ take\ k{\isacharprime}\ L{\isacharprime}\ {\isacharequal}\ take\ k{\isacharprime}\ {\isacharquery}l\ {\isasymand}\ {\isasymnot}\ {\isacharparenleft}{\isasymexists}\ Ls{\isachardot}\ Ls\ {\isasymsucceq}\ {\isacharquery}l\ {\isasymand}\ take\ k{\isacharprime}\ {\isacharquery}l\ {\isacharequal}\ take\ k{\isacharprime}\ Ls\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ stop\ Ls{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}l\ {\isasymsucceq}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}take\ k\ L\ {\isacharequal}\ take\ k\ {\isacharquery}l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L\ {\isacharbackquoteclose}{\isacharbackquoteopen}k\ {\isasymle}\ k{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ stop\ {\isacharquery}l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharbackquoteopen}k{\isacharprime}\ {\isasymge}\ k{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isacharquery}l\ {\isasymsucceq}\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}take\ k\ L\ {\isacharequal}\ take\ k\ {\isacharquery}l{\isacharbackquoteclose}\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymsucceq}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}a\ {\isacharequal}\ {\isachardoublequoteopen}foldl\ {\isacharparenleft}{\isasymlambda}r\ n{\isachardot}\ enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ r\ n\ g\ stop\ maxL\ L{\isacharparenright}\ {\isacharparenleft}val\ {\isacharhash}\ res{\isacharparenright}\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}k{\isacharprime}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp\ {\isacharparenleft}g\ val\ k{\isacharprime}{\isacharparenright}\ {\isacharquery}a\ k{\isacharprime}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ g\ stop\ maxL{\isacharparenright}{\isachardot}\ P\ B\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymin}\ {\isacharquery}X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}Ls{\isachardot}\ Ls\ {\isasymsucceq}\ inc{\isacharunderscore}nth\ L\ k{\isacharprime}\ {\isasymand}\ take\ k{\isacharprime}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ {\isacharequal}\ take\ k{\isacharprime}\ Ls\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ stop\ Ls{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Ls\ \isakeyword{where}\ {\isachardoublequoteopen}Ls\ {\isasymsucceq}\ {\isacharquery}l{\isachardoublequoteclose}\ {\isachardoublequoteopen}take\ k{\isacharprime}\ {\isacharquery}l\ {\isacharequal}\ take\ k{\isacharprime}\ Ls{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ Ls{\isachardoublequoteclose}\ {\isachardoublequoteopen}stop\ Ls{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Ls\ {\isasymsucceq}\ L\ {\isasymand}\ take\ k\ L\ {\isacharequal}\ take\ k\ Ls\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ stop\ Ls{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}l\ {\isasymsucceq}\ L{\isacharbackquoteclose}\ pwge{\isacharunderscore}trans{\isacharbrackleft}of\ Ls\ {\isacharquery}l\ L{\isacharbrackright}\ {\isacharbackquoteopen}k{\isacharprime}\ {\isasymge}\ k{\isacharbackquoteclose}\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ take{\isacharunderscore}prefix{\isacharbrackleft}of\ k\ k{\isacharprime}\ L\ Ls{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}k{\isacharprime}\ {\isasymin}\ set\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}length\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ {\isasymnoteq}\ length\ maxL\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ stop\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymnot}\ pwge{\isacharunderscore}impl\ maxL\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharbackquoteopen}{\isasymnot}\ stop\ {\isacharquery}l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}trans{\isacharbrackleft}of\ maxL\ L{\isacharprime}\ {\isacharquery}l{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}impl{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}P\ {\isacharparenleft}g\ val\ k{\isacharprime}{\isacharparenright}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{7}}{\isacharparenright}\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ L\ {\isacharequal}\ length\ maxL{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ {\isacharequal}\ length\ maxL{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ length\ {\isacharquery}l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ val\ L\ k{\isacharprime}\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}P\ val\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymAnd}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}\ {\isacharless}\ k{\isacharprime}{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymLongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}\ k{\isacharprime}\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ length\ maxL{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}P\ {\isacharparenleft}g\ val\ k{\isacharprime}{\isacharparenright}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{7}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k{\isacharprime}{\isacharprime}\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ k{\isacharprime}{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ k{\isacharprime}\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ {\isacharquery}a\ k{\isacharprime}\ g\ stop\ maxL\ L{\isacharparenright}{\isachardot}\ P\ B\ L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ L\ {\isacharequal}\ length\ maxL{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymnot}\ stop\ {\isacharquery}l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymsucceq}\ {\isacharquery}l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}trans{\isacharbrackleft}of\ maxL\ L{\isacharprime}\ {\isacharquery}l{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def\ pwge{\isacharunderscore}impl{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}k{\isachardot}{\isachardot}{\isacharless}k{\isacharprime}{\isacharbrackright}\ {\isacharat}\ {\isacharparenleft}k{\isacharprime}\ {\isacharhash}\ {\isacharbrackleft}Suc\ k{\isacharprime}{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ upt{\isacharunderscore}add{\isacharunderscore}eq{\isacharunderscore}append{\isacharbrackleft}of\ k\ k{\isacharprime}\ {\isachardoublequoteopen}length\ L\ {\isacharminus}\ k{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ upt{\isacharunderscore}conv{\isacharunderscore}Cons{\isacharbrackleft}of\ k{\isacharprime}\ {\isachardoublequoteopen}length\ L{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymle}\ k{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}dp\ val\ res\ k\ L\ g\ stop\ maxL\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ foldl\ {\isacharparenleft}{\isasymlambda}r\ n{\isachardot}\ enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ r\ n\ g\ stop\ maxL\ L{\isacharparenright}\ {\isacharquery}a\ {\isacharparenleft}k{\isacharprime}\ {\isacharhash}\ {\isacharbrackleft}Suc\ k{\isacharprime}{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ enum{\isacharunderscore}dp{\isachardot}simps{\isacharparenright}simp\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}dp\ val\ res\ k\ L\ g\ stop\ maxL\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ foldl\ {\isacharparenleft}{\isasymlambda}r\ n{\isachardot}\ enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ r\ n\ g\ stop\ maxL\ L{\isacharparenright}\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ {\isacharquery}a\ k{\isacharprime}\ g\ stop\ maxL\ L{\isacharparenright}\ {\isacharbrackleft}Suc\ k{\isacharprime}{\isachardot}{\isachardot}{\isacharless}length\ L{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ foldl{\isachardot}simps{\isacharparenright}\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}\ {\isacharbackquoteopen}length\ L\ {\isacharequal}\ length\ maxL{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mono{\isacharprime}{\isacharbrackleft}\isakeyword{where}\ res{\isacharequal}{\isachardoublequoteopen}enum{\isacharunderscore}dp{\isacharunderscore}step\ val\ {\isacharquery}a\ k{\isacharprime}\ g\ stop\ maxL\ L{\isachardoublequoteclose}\ \isakeyword{and}\ val{\isacharequal}val\ \isakeyword{and}\ g{\isacharequal}g\ \isakeyword{and}\ stop{\isacharequal}stop\ \isakeyword{and}\ maxL{\isacharequal}maxL\ \isakeyword{and}\ k{\isacharequal}{\isachardoublequoteopen}Suc\ k{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ L{\isacharequal}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Incrementally build all generating subsets for L-partitioned lists upto
 the given bounds%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P\ P\ n\ perms\ stops\ maxL\ {\isacharequal}\ \isanewline
\ \ \ enum{\isacharunderscore}dp\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isadigit{0}}\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymlambda}\ FFb\ m{\isachardot}\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ P\ FFb\ n\ m\ perms{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymlambda}\ L{\isachardot}\ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ L{\isacharprime}{\isachardot}\ pwge{\isacharunderscore}impl\ L\ L{\isacharprime}{\isacharparenright}\ stops{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ maxL{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P{\isacharunderscore}correct{\isacharcolon}\isanewline
\isakeyword{assumes}\ \ {\isachardoublequoteopen}{\isasymAnd}\ A\ F{\isachardot}\ {\isasymlbrakk}sd\ A{\isacharsemicolon}\ sdf\ F{\isacharsemicolon}\ dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ Pinc{\isacharprime}\ A\ F\ {\isasymlongleftrightarrow}\ Pinc\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ Pinc\ P{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ Pinc{\isachardoublequoteclose}\isanewline
\isakeyword{assumes}\isanewline
\ \ {\isachardoublequoteopen}X\ {\isacharequal}\ {\isacharbraceleft}L{\isacharprime}{\isachardot}\ maxL\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ {\isasymnot}\ {\isacharparenleft}{\isasymexists}\ S\ {\isasymin}\ set\ stops{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ S{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharunderscore}\ {\isacharequal}\ {\isacharquery}lhs{\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}P\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}length\ maxL\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ S\ {\isasymin}\ set\ stops{\isachardot}\ length\ S\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ \ {\isachardoublequoteopen}{\isasymforall}\ L{\isacharprime}\ {\isasymin}\ X{\isachardot}\ {\isasymexists}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P\ Pinc{\isacharprime}\ n\ perms\ stops\ maxL{\isacharparenright}{\isachardot}\ \isanewline
\ \ \ \ \ \ \ \ \ \ iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ B{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ L{\isacharprime}\ {\isasymin}\ X{\isachardot}\ {\isasymexists}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P\ Pinc{\isacharprime}\ n\ perms\ stops\ maxL{\isacharparenright}{\isachardot}\ \isanewline
\ \ \ \ \ \ \ \ \ \ iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ B{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharprime}{\isacharparenright}\ {\isasymand}\ sdff\ B\ {\isasymand}\ dmf\ B\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}dp{\isacharunderscore}lemma{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ length\ maxL{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ maxL\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}k{\isacharprime}{\isacharprime}{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ k{\isacharprime}{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ \ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharless}\ length\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isasymand}\ sdff\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ {\isasymand}\ dmf\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zeros{\isacharunderscore}replicate{\isacharbrackleft}of\ n\ {\isachardoublequoteopen}n{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharasterisk}{\isacharcomma}\ rule{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}\ {\isasymsubseteq}\ L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}P\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharasterisk}{\isacharparenright}{\isacharplus}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ iso{\isacharunderscore}represents{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ val\ L\ k{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ val{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L{\isacharparenright}\ {\isasymand}\ sdff\ val\ {\isasymand}\ dmf\ val\ n{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}{\isachargreater}k{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}k{\isacharprime}\ {\isacharless}\ length\ maxL{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}take\ {\isacharparenleft}k{\isacharprime}{\isacharplus}{\isadigit{1}}{\isacharparenright}\ L\ {\isacharequal}\ take\ k{\isacharprime}\ L\ {\isacharat}\ {\isacharbrackleft}L\ {\isacharbang}\ k{\isacharprime}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\ take{\isacharunderscore}Suc{\isacharunderscore}conv{\isacharunderscore}app{\isacharunderscore}nth{\isacharbrackleft}of\ k{\isacharprime}\ L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ val{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}take\ k{\isacharprime}\ L\ {\isacharat}\ {\isacharbrackleft}L\ {\isacharbang}\ k{\isacharprime}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zeros{\isacharbrackleft}of\ k{\isacharprime}\ L\ n{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ k{\isacharprime}\ perms{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}take\ k{\isacharprime}\ L\ {\isacharat}\ {\isacharbrackleft}{\isacharparenleft}L\ {\isacharbang}\ k{\isacharprime}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}correctness{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ val{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}take\ k{\isacharprime}\ L\ {\isacharat}\ {\isacharbrackleft}L\ {\isacharbang}\ k{\isacharprime}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ k{\isacharprime}\ perms{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ {\isacharparenleft}length\ {\isacharparenleft}take\ k{\isacharprime}\ L{\isacharparenright}{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ min{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ {\isacharparenleft}take\ k{\isacharprime}\ L{\isacharparenright}\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ maxL\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ maxL{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sdff\ val{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ val\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ Pinc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}take\ {\isacharparenleft}k{\isacharprime}{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}\ {\isacharequal}\ take\ k{\isacharprime}\ L\ {\isacharat}\ {\isacharbrackleft}Suc\ {\isacharparenleft}L\ {\isacharbang}\ k{\isacharprime}{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k{\isacharprime}\ {\isacharless}\ length\ L{\isacharbackquoteclose}\ take{\isacharunderscore}Suc{\isacharunderscore}conv{\isacharunderscore}app{\isacharunderscore}nth{\isacharbrackleft}of\ k{\isacharprime}\ {\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ k{\isacharprime}\ perms{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}take\ {\isacharparenleft}k{\isacharprime}{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ k{\isacharprime}\ perms{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}T{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zeros{\isacharbrackleft}of\ k{\isacharprime}\ {\isachardoublequoteopen}inc{\isacharunderscore}nth\ L\ k{\isacharprime}{\isachardoublequoteclose}\ n{\isacharbrackright}\ {\isacharbackquoteopen}{\isasymforall}\ k{\isacharprime}{\isacharprime}{\isachardot}\ k{\isacharprime}{\isacharprime}{\isachargreater}k{\isacharprime}\ {\isasymand}\ k{\isacharprime}{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ k{\isacharprime}\ perms{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}T{\isadigit{2}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharbrackleft}THEN\ conjunct{\isadigit{2}}{\isacharcomma}\ THEN\ conjunct{\isadigit{1}}{\isacharbrackright}\ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}dmf\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ Pinc{\isacharprime}\ val\ n\ k{\isacharprime}\ perms{\isacharparenright}\ n{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}T{\isadigit{3}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharbrackleft}THEN\ conjunct{\isadigit{2}}{\isacharcomma}\ THEN\ conjunct{\isadigit{2}}{\isacharbrackright}\ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}domain{\isacharparenright}\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}T{\isadigit{1}}\ {\isasymand}\ {\isacharquery}T{\isadigit{2}}\ {\isasymand}\ {\isacharquery}T{\isadigit{3}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isacharequal}\isanewline
\ \ \ \ \ \ {\isacharbraceleft}L{\isacharprime}{\isachardot}\isanewline
\ \ \ \ \ \ \ L{\isacharprime}\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}\ {\isasymand}\ \ maxL\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ take\ {\isadigit{0}}\ L{\isacharprime}\ {\isacharequal}\ take\ {\isadigit{0}}\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isacharparenright}\ {\isasymand}\isanewline
\ \ \ \ \ {\isasymnot}\ {\isacharparenleft}{\isasymexists}Ls{\isachardot}\ Ls\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ take\ {\isadigit{0}}\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ take\ {\isadigit{0}}\ Ls\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ list{\isacharunderscore}ex\ {\isacharparenleft}pwge{\isacharunderscore}impl\ Ls{\isacharparenright}\ stops{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharunderscore}\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ assms{\isacharparenleft}{\isadigit{4}}{\isacharparenright}{\isacharcomma}\ rule{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isasymsubseteq}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L{\isacharprime}\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}S{\isasymin}set\ stops{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ L{\isacharprime}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ maxL\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ pwge{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ L{\isacharprime}\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ pwge{\isacharunderscore}replicate{\isacharunderscore}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}Ls{\isachardot}\ Ls\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}\ {\isasymand}\ take\ {\isadigit{0}}\ {\isacharparenleft}replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ take\ {\isadigit{0}}\ Ls\ {\isasymand}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ list{\isacharunderscore}ex\ {\isacharparenleft}pwge{\isacharunderscore}impl\ Ls{\isacharparenright}\ stops{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Ls\ \isakeyword{where}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ Ls{\isachardoublequoteclose}\ {\isachardoublequoteopen}list{\isacharunderscore}ex\ {\isacharparenleft}pwge{\isacharunderscore}impl\ Ls{\isacharparenright}\ stops{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ Ls\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ L{\isacharprime}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ S\ \isakeyword{where}\ {\isachardoublequoteopen}S\ {\isasymin}\ set\ stops{\isachardoublequoteclose}\ {\isachardoublequoteopen}Ls\ {\isasymsucceq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}impl{\isacharbrackleft}of\ Ls{\isacharbrackright}\ {\isacharbackquoteopen}{\isasymforall}\ S\ {\isasymin}\ set\ stops{\isachardot}\ length\ S\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}S{\isasymin}set\ stops{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ S{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymsucceq}\ Ls{\isacharbackquoteclose}\ pwge{\isacharunderscore}trans{\isacharbrackleft}of\ L{\isacharprime}\ Ls\ S{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}rhs\ {\isasymsubseteq}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L{\isacharprime}\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}Ls{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ Ls\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}\ {\isasymand}\ list{\isacharunderscore}ex\ {\isacharparenleft}pwge{\isacharunderscore}impl\ Ls{\isacharparenright}\ stops{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}S{\isasymin}set\ stops{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ S\ \isakeyword{where}\ {\isachardoublequoteopen}S\ {\isasymin}\ set\ stops{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ L{\isacharprime}\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ S\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ maxL\ {\isacharequal}\ n{\isacharplus}{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ S\ {\isasymand}\ S\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}\ {\isasymand}\ list{\isacharunderscore}ex\ {\isacharparenleft}pwge{\isacharunderscore}impl\ S{\isacharparenright}\ stops{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}refl{\isacharbrackleft}of\ S{\isacharbrackright}\ pwge{\isacharunderscore}impl{\isacharbrackleft}of\ S\ S{\isacharbrackright}\ pwge{\isacharunderscore}replicate{\isacharunderscore}{\isadigit{0}}{\isacharbrackleft}of\ S\ {\isachardoublequoteopen}n{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}Ls{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ Ls\ {\isasymand}\ Ls\ {\isasymsucceq}\ replicate\ {\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}\ {\isasymand}\ list{\isacharunderscore}ex\ {\isacharparenleft}pwge{\isacharunderscore}impl\ Ls{\isacharparenright}\ stops{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}maxL\ {\isasymsucceq}\ L{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
