%
\begin{isabellebody}%
\setisabellecontext{LPartitioningIrreducible}%
%
\isamarkupsubsection{Generating all irreducible families%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioningIrreducible\isanewline
\isakeyword{imports}\ LPartitioning\ IrreducibleFamilies\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ irreducible{\isacharunderscore}expressible{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F{\isacharparenright}\ irreducible{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{and}\ \ F\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ expressible\ A\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}irreducible\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isasymge}\ card\ A{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}reducible\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ Fb\ \isakeyword{where}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fb\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fb\ {\isasymsubseteq}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymnotin}\ Fb{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ Fb{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}reducible\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ reducible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ False\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}A{\isacharprime}\ {\isacharequal}\ A{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ expressible\ A\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ Fb{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fb\ {\isasymsubseteq}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymnotin}\ Fb{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fb\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Fb{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fb\ {\isasymsubseteq}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymnotin}\ Fb{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ Fb{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fb\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}irreducible\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ reducible{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ Fb{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A{\isacharprime}\ {\isachargreater}\ card\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymnoteq}\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ A{\isacharprime}\ A{\isacharbrackright}\ card{\isacharunderscore}seteq{\isacharbrackleft}of\ A{\isacharprime}\ A{\isacharbrackright}\ \ {\isacharbackquoteopen}finite\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isasymge}\ card\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ reducible{\isacharunderscore}def\ expressible{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ not{\isacharunderscore}expressible{\isacharunderscore}iso{\isacharcolon}\isanewline
\isakeyword{assumes}\ \ {\isachardoublequoteopen}{\isasymnot}\ expressible\ A\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ expressible\ {\isacharparenleft}f\ {\isacharbackquote}\ A{\isacharparenright}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fb{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}Fb{\isacharprime}\ {\isasymsubseteq}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isacharequal}\ {\isasymUnion}Fb{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fb{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharplus}{\isacharplus}{\isacharcolon}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharprime}\ {\isacharequal}\ Fb{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ {\isacharparenleft}no{\isacharunderscore}types{\isacharparenright}\ subset{\isacharunderscore}image{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}y\ {\isasymin}\ Fb{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ x\ {\isasymin}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}image\ f\ A\ {\isacharequal}\ {\isasymUnion}Fb{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ x{\isacharprime}\ y{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}y{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ {\isasymin}\ y{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymin}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}y{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymin}\ y{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymsubseteq}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ x\ {\isasymin}\ f\ {\isacharbackquote}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}image\ f\ A\ {\isacharequal}\ {\isasymUnion}Fb{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ x{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}x{\isacharprime}\ {\isasymin}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ f\ x{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ {\isasymUnion}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}\ {\isacharbackquoteopen}Fb{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ expressible\ A\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}expressible{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ not{\isacharunderscore}expressible{\isacharunderscore}iso\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}irreducible\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}irreducible\ {\isasymequiv}\ L{\isacharunderscore}part{\isacharunderscore}P\ irreducible{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ mult{\isacharunderscore}irreducible\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}irreducible\ {\isasymequiv}\ mult{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}irreducible\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}irreducible\ {\isasymequiv}\ mult{\isacharunderscore}all{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}mult{\isacharunderscore}irreducible{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}irreducible\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharplus}{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}irreducible\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}irreducible\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}P{\isacharbrackleft}of\ irreducible\ {\isachardoublequoteopen}{\isasymlambda}\ A\ f{\isachardot}\ {\isasymnot}\ expressible\ A\ f{\isachardoublequoteclose}\ n\ L\ k{\isacharcomma}\ OF\ irreducible{\isacharunderscore}expressible{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemmas}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}mult{\isacharunderscore}irreducible{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharequal}\isanewline
\ \ \ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharbrackleft}of\ irreducible\ {\isachardoublequoteopen}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F{\isachardoublequoteclose}{\isacharcomma}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ OF\ irreducible{\isacharunderscore}expressible\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}expressible{\isacharbrackright}\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
