%
\begin{isabellebody}%
\setisabellecontext{LPartitioningIrreducibleNonFCsCoveredImpl}%
%
\isamarkupsubsubsection{Implementation%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioningIrreducibleNonFCsCoveredImpl\isanewline
\isakeyword{imports}\ LPartitioningIrreducibleNonFCsCovered\ IrreducibleFamiliesImpl\ CoveringImpl\ LPartitioningNonFCsCoveredImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ irreducible{\isacharunderscore}expressible{\isacharunderscore}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}\isanewline
\ \ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}dm\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ expressible{\isacharunderscore}l\ A\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ perms\ {\isasymlongleftrightarrow}\ {\isasymnot}\ expressible\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}\ {\isasymand}\ {\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%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}soundness{\isacharbrackleft}of\ A\ F{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}completeness{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{4}}{\isacharminus}{\isadigit{5}}{\isacharparenright}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharminus}{\isadigit{3}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{6}}{\isacharparenright}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}irreducible{\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\ {\isasymand}\ {\isasymnot}\ expressible{\isacharunderscore}l\ A\ 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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms\ {\isacharequal}\ \isanewline
\ \ \ \ \ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ mult{\isacharunderscore}irreducible{\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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms\ {\isacharequal}\isanewline
\ \ \ \ \ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ perms\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ n\ m\ perms\ {\isacharequal}\isanewline
\ \ \ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible{\isacharunderscore}l\ A\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ perms{\isacharparenright}\ F\ n\ m\ perms{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}P{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ filter{\isacharunderscore}map\ Let{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ mult{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}irreducible{\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\ {\isasymand}\ {\isasymnot}\ expressible{\isacharunderscore}l\ A\ 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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m\ {\isacharequal}\ \isanewline
\ \ \ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ mult{\isacharunderscore}irreducible{\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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m\ perms\ {\isacharequal}\isanewline
\ \ \ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ perms\ {\isacharparenleft}mult{\isacharunderscore}all{\isacharunderscore}irreducible{\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}irreducible{\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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ F\ n\ m\ perms\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\ mult{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ mult{\isacharunderscore}irreducible{\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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}irreducible{\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}irreducible{\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{abbreviation}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}{\isacharunderscore}perms\ n\ perms\ stops\ maxL\ {\isasymequiv}\ \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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymF}{\isacharunderscore}perms\ 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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\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}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}{\isacharunderscore}perms\ n\ perms\ stops\ maxL\ {\isacharequal}\ \isanewline
\ \ \ \ \ enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible{\isacharunderscore}l\ A\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ perms{\isacharparenright}\ n\ perms\ stops\ maxL{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}opt{\isacharbrackleft}OF\ assms{\isacharbrackright}{\isacharcomma}\ subst\ mult{\isacharunderscore}all{\isacharunderscore}base{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharcomma}\ simp{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subsets{\isacharcolon}\isanewline
\isakeyword{assumes}\isanewline
\ \ {\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
\ \ {\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}\isanewline
\ \ {\isachardoublequoteopen}length\ maxL\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ S\ {\isasymin}\ set\ stops{\isachardot}\ length\ S\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymnotin}\ set\ {\isasymF}{\isachardoublequoteclose}\ {\isachardoublequoteopen}perms\ {\isacharequal}\ permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ {\isasymF}\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdff\ {\isasymF}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ \ {\isachardoublequoteopen}{\isasymforall}\ L{\isacharprime}\ {\isasymin}\ X{\isachardot}\ {\isasymexists}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}{\isacharunderscore}perms\ 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}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isasymF}{\isacharparenright}\ n\ L{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}irreducible\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isasymF}{\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\ reducible{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ {\isacharparenleft}rule\ enum{\isacharunderscore}dp{\isacharunderscore}mult{\isacharunderscore}P{\isacharunderscore}correct\ {\isacharbrackleft}\isakeyword{where}\ Pinc{\isacharprime}{\isacharequal}{\isachardoublequoteopen}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible{\isacharunderscore}l\ A\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ {\isacharparenleft}A\ {\isacharhash}\ F{\isacharparenright}\ perms{\isachardoublequoteclose}{\isacharcomma}\ OF\ irreducible{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{7}}{\isacharparenright}{\isacharbrackright}\ irreducible{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharbrackright}{\isacharcomma}\ auto\ simp\ add{\isacharcolon}\ isPermutation{\isacharunderscore}permute{\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:
