%
\begin{isabellebody}%
\setisabellecontext{LPartitioningNonFCsCoveredImpl}%
%
\isamarkupsubsubsection{Implementation%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioningNonFCsCoveredImpl\isanewline
\isakeyword{imports}\ LPartitioningNonFCsCovered\ CoveringImpl\ LPartitioningImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}perms\ {\isacharequal}\ permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ {\isasymF}\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdff\ {\isasymF}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ \isanewline
\ \ \ \ \ {\isachardoublequoteopen}{\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ perms\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ \ \ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isasymF}{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F\ {\isasymunion}\ {\isacharbraceleft}set\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ \ \ \ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}soundness{\isacharbrackleft}of\ perms\ n\ {\isacharunderscore}\ {\isachardoublequoteopen}A\ {\isacharhash}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}completeness{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isacharhash}\ F{\isachardoublequoteclose}\ {\isacharunderscore}\ n\ perms{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff\ isPermutation{\isacharunderscore}permute{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ A\ perms\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ {\isacharparenleft}let\ F{\isacharprime}\ {\isacharequal}\ filter\ {\isacharparenleft}{\isasymlambda}\ f{\isachardot}\ A\ {\isasymnotin}\ set\ f{\isacharparenright}\ F{\isacharsemicolon}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ F{\isacharprime}{\isacharprime}\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ A\ {\isacharhash}\ x{\isacharparenright}\ F{\isacharprime}\ \isanewline
\ \ \ \ \ \ \ \ in\ filter\ {\isacharparenleft}{\isasymlambda}\ X{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ X\ perms{\isacharparenright}\ F{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms\ {\isacharequal}\ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ A\ perms{\isacharparenright}\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms\ {\isacharequal}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ perms\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ perms{\isacharparenright}\ F\ n\ m\ perms{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ filter{\isacharunderscore}map{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ list\ list\ {\isasymRightarrow}\ nat\ list\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ Fc{\isacharunderscore}perms\ F\ {\isasymlongleftrightarrow}\ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Fc{\isacharprime}{\isachardot}\ set\ Fc{\isacharprime}\ {\isasymsubseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isacharparenright}\ Fc{\isacharunderscore}perms{\isachardoublequoteclose}\isanewline
\isacommand{definition}\isamarkupfalse%
\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ {\isasymlongleftrightarrow}\ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Fc{\isachardot}\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ Fc\ F{\isacharparenright}\ {\isasymF}{\isacharunderscore}perms{\isachardoublequoteclose}\isanewline
\ \ \isanewline
\isacommand{definition}\isamarkupfalse%
\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharprime}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharprime}\ {\isasymF}{\isacharunderscore}perms\ F\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ \ \ {\isacharparenleft}let\ clF\ {\isacharequal}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ in\ list{\isacharunderscore}ex\ {\isacharparenleft}list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Fc{\isacharprime}{\isachardot}\ set\ Fc{\isacharprime}\ {\isasymsubseteq}\ clF{\isacharparenright}{\isacharparenright}\ {\isasymF}{\isacharunderscore}perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharprime}\ {\isacharequal}\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ ext{\isacharparenright}{\isacharplus}\ {\isacharparenleft}simp\ add{\isacharcolon}\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharprime}{\isacharunderscore}def\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ A\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ {\isacharparenleft}let\ F{\isacharprime}\ {\isacharequal}\ filter\ {\isacharparenleft}{\isasymlambda}\ f{\isachardot}\ A\ {\isasymnotin}\ set\ f{\isacharparenright}\ F{\isacharsemicolon}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ F{\isacharprime}{\isacharprime}\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ A\ {\isacharhash}\ x{\isacharparenright}\ F{\isacharprime}\ \isanewline
\ \ \ \ \ \ \ \ in\ filter\ {\isacharparenleft}{\isasymlambda}\ X{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharprime}\ {\isasymF}{\isacharunderscore}perms\ X{\isacharparenright}\ F{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m\ {\isacharequal}\ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ A{\isacharparenright}\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m\ perms\ {\isacharequal}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ perms\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}opt{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymF}{\isacharunderscore}perms\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ permute{\isacharunderscore}family{\isacharunderscore}l\ p\ F{\isacharparenright}\ perms{\isacharparenright}\ {\isasymF}{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m\ perms\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ FCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ \ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}{\isacharunderscore}perms\ L\ n\ perms\ {\isasymequiv}\ \isanewline
\ \ enum{\isacharunderscore}rec\ L\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ {\isacharparenleft}{\isasymlambda}\ F\ L{\isachardot}\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ {\isacharparenleft}length\ L\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymF}{\isacharunderscore}perms\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ permute{\isacharunderscore}family{\isacharunderscore}l\ p\ F{\isacharparenright}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isasymF}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymnotin}\ set\ {\isasymF}{\isachardoublequoteclose}\ \isanewline
\ \ {\isachardoublequoteopen}dmf\ {\isasymF}\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdff\ {\isasymF}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ L\ {\isacharminus}\ {\isadigit{1}}\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}{\isacharunderscore}perms\ L\ n\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isasymF}{\isacharparenright}\ n\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}Fc{\isasymin}set\ {\isasymF}{\isachardot}\ {\isasymnot}\ FC{\isacharunderscore}covered\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymnotin}\ set\ {\isasymF}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ \ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sdff\ {\isasymF}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}opt{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}{\isacharplus}\isanewline
\ \ \ \ \ \ \ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharbrackleft}\isakeyword{where}\ n{\isacharequal}{\isachardoublequoteopen}n{\isachardoublequoteclose}\ \isakeyword{and}\ perms{\isacharequal}{\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}{\isacharcomma}\ OF\ notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharbrackleft}of\ {\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}{\isacharcomma}\ OF\ {\isacharunderscore}\ assms{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isacharbrackright}\ notFCs{\isacharunderscore}covered\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}FCs{\isacharunderscore}covered\ {\isacharunderscore}\ {\isacharbackquoteopen}length\ L\ {\isacharminus}\ {\isadigit{1}}\ {\isasymle}\ n{\isacharbackquoteclose}{\isacharbrackright}{\isacharcomma}\ simp{\isacharunderscore}all\ add{\isacharcolon}\ isPermutation{\isacharunderscore}permute\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
