%
\begin{isabellebody}%
\setisabellecontext{LPartitioningNonFCsCovered}%
%
\isamarkupsubsection{Generating all families that are not FCs covered by the given collection%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioningNonFCsCovered\isanewline
\isakeyword{imports}\ LPartitioning\ \ Covering\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ n\ L{\isachardot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ L{\isacharunderscore}part\ n\ L{\isacharprime}{\isachardot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharprime}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F\ \isakeyword{where}\ {\isachardoublequoteopen}F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isacharbackquoteclose}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}subset{\isacharbrackleft}of\ L{\isacharprime}\ L\ n\ F{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fc\ \isakeyword{where}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fc\ {\isasymin}\ {\isasymF}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}of\ F{\isacharbrackright}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}mono{\isacharbrackleft}of\ F\ F{\isacharprime}\ Fc{\isacharbrackright}\ {\isacharbackquoteopen}F\ {\isasymsubseteq}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ notFCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}mono\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ notFCs{\isacharunderscore}covered{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}{\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Un{\isacharunderscore}commute{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ iso{\isacharunderscore}sym\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ {\isacharparenleft}{\isasymlambda}\ A\ F{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ notFCs{\isacharunderscore}covered{\isacharunderscore}iso\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}notFCs{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ {\isasymequiv}\ L{\isacharunderscore}part{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ {\isasymequiv}\ mult{\isacharunderscore}all{\isacharunderscore}P\ {\isacharparenleft}{\isasymlambda}\ A\ f{\isachardot}\ {\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}notFC{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}FFb{\isacharprime}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}notFCs{\isacharunderscore}covered\ {\isasymF}\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}length\ L\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb{\isacharprime}\ {\isacharparenleft}L{\isacharunderscore}part{\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}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}\ A\ f{\isachardot}\ {\isasymnot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ {\isacharparenleft}f\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\ FFb\ n\ L\ k{\isacharcomma}\ OF\ notFCs{\isacharunderscore}covered\ inj{\isacharunderscore}preserved{\isacharunderscore}not{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\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:
