%
\begin{isabellebody}%
\setisabellecontext{LPartitioningIrreducibleNonFCsCovered}%
%
\isamarkupsubsection{Generating all irreducible families that are not FCs covered by the given collection%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioningIrreducibleNonFCsCovered\isanewline
\isakeyword{imports}\ LPartitioningIrreducible\ LPartitioningNonFCsCovered\ IrreducibleFamilies\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ irreducible{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ irreducible\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ irreducible{\isacharunderscore}expressible\isanewline
\isacommand{using}\isamarkupfalse%
\ notFCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isasymF}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ metis%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ irreducible{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharunderscore}iso{\isacharcolon}\isanewline
\isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ expressible\ A\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\ {\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}\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ not{\isacharunderscore}expressible{\isacharunderscore}iso{\isacharbrackleft}of\ A\ F\ f{\isacharbrackright}\ notFCs{\isacharunderscore}covered{\isacharunderscore}iso{\isacharbrackleft}of\ {\isasymF}\ F\ A\ f{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ expressible\ A\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}expressible\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}FCs{\isacharunderscore}covered\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ {\isasymequiv}\ L{\isacharunderscore}part{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ irreducible\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ {\isasymequiv}\ mult{\isacharunderscore}all{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ A\ f{\isachardot}\ {\isasymnot}\ expressible\ A\ f\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}f\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharunderscore}irreducible{\isacharunderscore}notFC{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}length\ L\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}FFb{\isacharprime}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb{\isacharprime}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}\ F{\isachardot}\ irreducible\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}\ A\ f{\isachardot}\ {\isasymnot}\ expressible\ A\ f\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}f\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\ FFb{\isacharcomma}\ OF\ irreducible{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}expressible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ {\isasymF}\ {\isasymN}\ FFb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}irreducible{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ n\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ FFb{\isachardot}\ nonFCs{\isacharunderscore}covered\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ N\ {\isasymin}\ {\isasymN}{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ N{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part{\isacharunderscore}irreducible\ n\ L{\isachardot}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}nonFCs{\isacharunderscore}covered{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}F\ {\isasymin}\ L{\isacharunderscore}part\ n\ L{\isachardot}\ irreducible\ F\ {\isasymand}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharbraceright}{\isachardoublequoteclose}\ {\isasymN}\ FFb{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}finite{\isacharbrackleft}of\ n\ L{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
