%
\begin{isabellebody}%
\setisabellecontext{FC{\isadigit{6}}}%
%
\isamarkupsection{Proof that all families are covered%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ FC{\isadigit{6}}\isanewline
\isakeyword{imports}\ FC{\isadigit{6}}{\isacharunderscore}Data\ LPartitioningIrreducibleNonFCsCoveredImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ FC{\isadigit{6}}{\isacharunderscore}perms\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FC{\isadigit{6}}{\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}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ FC{\isadigit{6}}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ nonFC{\isadigit{6}}{\isacharunderscore}perms\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nonFC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ Nc{\isachardot}\ map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ close{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ nonFC{\isadigit{6}}{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}{\isadigit{6}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ n{\isadigit{0}}\ n{\isadigit{1}}\ n{\isadigit{2}}\ n{\isadigit{3}}\ n{\isadigit{4}}\ n{\isadigit{5}}\ n{\isadigit{6}}{\isachardot}\ \isanewline
\ \ \ \ is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}n{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}\ F\ {\isasymand}\ \isanewline
\ \ \ \ n{\isadigit{0}}\ {\isasymle}\ {\isadigit{1}}\ {\isasymand}\ n{\isadigit{1}}\ {\isasymle}\ {\isadigit{6}}\ {\isasymand}\ n{\isadigit{2}}\ {\isasymle}\ {\isadigit{1}}{\isadigit{5}}\ {\isasymand}\ n{\isadigit{3}}\ {\isasymle}\ {\isadigit{2}}{\isadigit{0}}\ {\isasymand}\ n{\isadigit{4}}\ {\isasymle}\ {\isadigit{1}}{\isadigit{5}}\ {\isasymand}\ n{\isadigit{5}}\ {\isasymle}\ {\isadigit{6}}\ {\isasymand}\ n{\isadigit{6}}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A\ {\isasymle}\ card\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ A{\isacharbrackright}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ assms\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ Union{\isacharunderscore}upper\ card{\isacharunderscore}atLeastLessThan\ card{\isacharunderscore}mono\ finite{\isacharunderscore}atLeastLessThan{\isacharparenright}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A\ {\isacharless}\ {\isadigit{7}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ card{\isacharunderscore}mono{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{6}}\ choose\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isadigit{5}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{6}}\ choose\ {\isadigit{3}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{6}}\ choose\ {\isadigit{4}}\ {\isacharequal}\ {\isadigit{1}}{\isadigit{5}}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}{\isadigit{6}}\ choose\ {\isadigit{5}}\ {\isacharequal}\ {\isadigit{6}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval{\isacharplus}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{1}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{3}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{4}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{5}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ {\isadigit{6}}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ metis\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{1}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{2}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{3}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{4}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{5}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{6}}{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{0}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{1}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{2}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{3}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{4}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{5}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isadigit{6}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymnotin}\ set\ FC{\isadigit{6}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ FC{\isadigit{6}}\ {\isadigit{6}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdff\ FC{\isadigit{6}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval{\isacharplus}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharbrackleft}of\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isadigit{6}}\ FC{\isadigit{6}}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isadigit{6}}{\isacharunderscore}perms{\isacharunderscore}def\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{5}}{\isadigit{6}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{7}}{\isadigit{0}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{1}}{\isadigit{6}}{\isadigit{5}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{2}}{\isadigit{0}}{\isadigit{6}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{3}}{\isadigit{0}}{\isadigit{4}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{3}}{\isadigit{2}}{\isadigit{3}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{3}}{\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{4}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}enum{\isacharunderscore}rec{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ all{\isacharunderscore}FC{\isacharunderscore}partitions\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}all{\isacharunderscore}FC{\isacharunderscore}partitions\ {\isacharequal}\ \isanewline
{\isacharbrackleft}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\ \isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isacharcomma}\isanewline
\ \ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}\ \isanewline
{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}notAllFC{\isacharunderscore}partitions\ {\isacharequal}\ {\isacharbraceleft}L{\isacharprime}{\isachardot}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{2}}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ {\isasymnot}\ {\isacharparenleft}{\isasymexists}\ S\ {\isasymin}\ set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ S{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions{\isacharunderscore}remove{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}\ {\isasymin}\ notAllFC{\isacharunderscore}partitions{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymin}\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}\ {\isasymin}\ \ notAllFC{\isacharunderscore}partitions{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}L{\isacharprime}\ {\isasymin}\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions{\isacharunderscore}def\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}Cons\ pwge{\isacharunderscore}Nil{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ L\ F{\isachardot}\ L\ {\isasymin}\ notAllFC{\isacharunderscore}partitions\ {\isasymand}\ hd\ L\ {\isacharequal}\ {\isadigit{0}}\ {\isasymand}\ F\ {\isasymin}\ L{\isacharunderscore}part{\isacharunderscore}irreducible\ {\isadigit{6}}\ L\ {\isasymlongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymF}\ {\isacharequal}\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}\ {\isasymlongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharparenleft}rule\ all{\isacharunderscore}irreducible{\isacharunderscore}covered{\isacharunderscore}all{\isacharunderscore}covered{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ F{\isachardot}\ irreducible\ F\ {\isasymand}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}\ {\isasymlongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}irreducible\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ n{\isadigit{0}}\ n{\isadigit{1}}\ n{\isadigit{2}}\ n{\isadigit{3}}\ n{\isadigit{4}}\ n{\isadigit{5}}\ n{\isadigit{6}}\ \isakeyword{where}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharbrackleft}n{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharasterisk}{\isacharcolon}\ \ {\isachardoublequoteopen}n{\isadigit{0}}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n{\isadigit{1}}\ {\isasymle}\ {\isadigit{6}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n{\isadigit{2}}\ {\isasymle}\ {\isadigit{1}}{\isadigit{5}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n{\isadigit{3}}\ {\isasymle}\ {\isadigit{2}}{\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n{\isadigit{4}}\ {\isasymle}\ {\isadigit{1}}{\isadigit{5}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n{\isadigit{5}}\ {\isasymle}\ {\isadigit{6}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n{\isadigit{6}}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}{\isadigit{6}}{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbrackleft}n{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{2}}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}\ {\isasymsucceq}\ {\isacharbrackleft}n{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ pwge{\isacharunderscore}Cons{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}{\isasymexists}\ L{\isacharprime}\ {\isasymin}\ set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardot}\ {\isacharquery}L\ {\isasymsucceq}\ L{\isacharprime}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n{\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ {\isacharquery}L\ F{\isacharbrackright}\ {\isacharbackquoteopen}irreducible\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}\ L{\isacharprime}\ {\isasymin}\ set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardot}\ {\isacharquery}L\ {\isasymsucceq}\ L{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}n{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n{\isadigit{0}}\ {\isasymle}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ covered{\isacharunderscore}remove{\isacharunderscore}empty{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ n{\isadigit{1}}{\isacharcomma}\ n{\isadigit{2}}{\isacharcomma}\ n{\isadigit{3}}{\isacharcomma}\ n{\isadigit{4}}{\isacharcomma}\ n{\isadigit{5}}{\isacharcomma}\ n{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymin}\ notAllFC{\isacharunderscore}partitions{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}\ \ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymexists}\ L{\isacharprime}\ {\isasymin}\ set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardot}\ {\isacharquery}L\ {\isasymsucceq}\ L{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}n{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L{\isacharprime}\ {\isasymin}\ notAllFC{\isacharunderscore}partitions{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}n{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isacharbackquoteclose}{\isacharparenright}\ {\isacharparenleft}rule\ notAllFC{\isacharunderscore}partitions{\isacharunderscore}remove{\isacharunderscore}empty{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}hd\ {\isacharquery}L{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L{\isacharprime}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}remove{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ F\ {\isadigit{6}}\ {\isacharquery}L{\isacharbrackright}\ {\isacharbackquoteopen}n{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}empty{\isacharunderscore}mem{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}irreducible\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}irreducible\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ reducible{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ {\isacharquery}L{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ L\ \isakeyword{where}\ {\isachardoublequoteopen}L\ {\isasymin}\ set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{5}}{\isadigit{6}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{7}}{\isadigit{0}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{1}}{\isadigit{6}}{\isadigit{5}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{2}}{\isadigit{0}}{\isadigit{6}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{3}}{\isadigit{0}}{\isadigit{4}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{3}}{\isadigit{2}}{\isadigit{3}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{3}}{\isadigit{3}}{\isadigit{0}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{4}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}L\ {\isasymsucceq}\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ {\isacharquery}L\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}{\isadigit{0}}{\isadigit{0}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isadigit{6}}\ {\isacharunderscore}\ {\isasymF}\ {\isacharquery}L{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymin}\ set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isacharquery}L\ {\isasymsucceq}\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{theorem}\isamarkupfalse%
\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}\ {\isasymlongrightarrow}\ covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ nonFC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ notAllFC{\isacharunderscore}partitions{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}L\ F{\isachardot}\ L\ {\isasymin}\ notAllFC{\isacharunderscore}partitions\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ hd\ L\ {\isacharequal}\ {\isadigit{0}}\ {\isasymand}\ F\ {\isasymin}\ L{\isacharunderscore}part{\isacharunderscore}irreducible\ {\isadigit{6}}\ L\ {\isasymlongrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ \ covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ nonFC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L\ \isakeyword{and}\ F{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isasymin}\ notAllFC{\isacharunderscore}partitions{\isachardoublequoteclose}\ {\isachardoublequoteopen}hd\ L\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}irreducible\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ L\ F{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}maxL\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{2}}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}stops\ {\isacharequal}\ {\isachardoublequoteopen}all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}L{\isacharprime}{\isachardot}\ {\isacharquery}maxL\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ {\isasymnot}\ {\isacharparenleft}{\isasymexists}\ S\ {\isasymin}\ set\ {\isacharquery}stops{\isachardot}\ L{\isacharprime}\ {\isasymsucceq}\ S{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}perms\ {\isacharequal}\ {\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymin}\ notAllFC{\isacharunderscore}partitions{\isacharbackquoteclose}\ {\isacharbackquoteopen}hd\ L\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isasymin}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ notAllFC{\isacharunderscore}partitions{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ L{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pwge{\isacharunderscore}def{\isacharcomma}\ auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}Cons{\isacharparenright}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}S{\isasymin}set\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isachardot}\ length\ S\ {\isacharequal}\ {\isadigit{7}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymnotin}\ set\ FC{\isadigit{6}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}dmf\ FC{\isadigit{6}}\ {\isadigit{6}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdff\ FC{\isadigit{6}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}FC{\isacharunderscore}partitions{\isacharunderscore}def\ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval{\isacharplus}\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ B\ \isakeyword{where}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isadigit{6}}\ {\isacharquery}perms\ {\isacharquery}stops\ {\isacharquery}maxL{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}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\ FC{\isadigit{6}}{\isacharparenright}\ {\isadigit{6}}\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subsets{\isacharbrackleft}of\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\ FC{\isadigit{6}}\ {\isacharquery}X\ {\isacharquery}maxL\ {\isacharquery}stops\ {\isadigit{6}}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ FC{\isadigit{6}}{\isacharunderscore}perms{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharparenright}\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ nonFC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ iso{\isacharunderscore}represents{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ L{\isacharunderscore}part{\isacharunderscore}irreducible\ {\isadigit{6}}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ {\isadigit{6}}\ L\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}irreducible\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ N\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}N\ {\isasymin}\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ nonFC{\isadigit{6}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}N{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}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\ FC{\isadigit{6}}{\isacharparenright}\ {\isadigit{6}}\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ all{\isacharunderscore}FC{\isacharunderscore}partitions\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{2}}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isachardot}\ {\isasymforall}\ F\ {\isasymin}\ set\ B{\isachardot}\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ nonFC{\isadigit{6}}{\isacharunderscore}perms\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}dmf\ nonFC{\isadigit{6}}\ {\isadigit{6}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ eval\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isadigit{6}}\ {\isacharparenleft}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ all{\isacharunderscore}FC{\isacharunderscore}partitions\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{2}}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isachardot}\ {\isasymforall}\ F\ {\isasymin}\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ B{\isachardot}\ nonFCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ nonFC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}soundness{\isacharbrackleft}of\ {\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\ {\isadigit{6}}\ {\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharbrackleft}of\ nonFC{\isadigit{6}}{\isacharunderscore}perms\ {\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharbrackright}{\isachardoublequoteclose}\ nonFC{\isadigit{6}}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff\ isPermutation{\isacharunderscore}permute\ nonFC{\isadigit{6}}{\isacharunderscore}perms{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\ \isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ nonFC{\isadigit{6}}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}B\ {\isasymin}\ set\ {\isacharparenleft}enum{\isacharunderscore}dp{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}l\ FC{\isadigit{6}}{\isacharunderscore}perms\ {\isadigit{6}}\ {\isacharquery}perms\ {\isacharquery}stops\ {\isacharquery}maxL{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ all{\isacharunderscore}nonFC{\isacharunderscore}partitions\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}all{\isacharunderscore}nonFC{\isacharunderscore}partitions\ {\isacharequal}\ \isanewline
{\isacharbrackleft}\isanewline
\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharcomma}\isanewline
\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharcomma}\isanewline
\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharcomma}\isanewline
\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharcomma}\isanewline
\ {\isacharbrackleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}\isanewline
{\isacharbrackright}{\isachardoublequoteclose}\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
