%
\begin{isabellebody}%
\setisabellecontext{Covering}%
%
\isamarkupsection{Covering%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Covering\isanewline
\isakeyword{imports}\ UnionClosed\ Frankl\ IsomorphicFamilies\ IrreducibleFamilies\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Definition of Covering%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ FC{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F\ {\isasymequiv}\ {\isasymexists}\ Fc{\isacharprime}{\isachardot}\ iso\ Fc{\isacharprime}\ Fc\ {\isasymand}\ Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ Nc\ F\ {\isasymequiv}\ {\isasymexists}\ Nc{\isacharprime}{\isachardot}\ iso\ Nc\ Nc{\isacharprime}\ {\isasymand}\ closure\ F\ {\isasymsubseteq}\ closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ FCs{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FCs{\isacharunderscore}covered\ {\isasymF}\ F\ {\isasymequiv}\ {\isasymexists}\ Fc\ {\isasymin}\ {\isasymF}{\isachardot}\ FC{\isacharunderscore}covered\ Fc\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered\ {\isasymN}\ F\ {\isasymequiv}\ {\isasymexists}\ Nc\ {\isasymin}\ {\isasymN}{\isachardot}\ nonFC{\isacharunderscore}covered\ Nc\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ covered\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F\ {\isasymequiv}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F\ {\isasymor}\ nonFCs{\isacharunderscore}covered\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}sound{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ Fc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isacharbackquoteclose}\ \isacommand{obtain}\isamarkupfalse%
\ Fc{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}iso\ Fc{\isacharprime}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}FC{\isacharunderscore}family\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}closure{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}mono{\isacharbrackleft}of\ Fc{\isacharprime}\ {\isachardoublequoteopen}closure\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}iso{\isacharbrackleft}of\ {\isacharunderscore}\ Fc{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}sound{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ F\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ F{\isacharprime}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymnot}\ FC{\isacharunderscore}family\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ FC{\isacharunderscore}family\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}nonFC{\isacharunderscore}covered\ F{\isacharprime}\ F{\isacharbackquoteclose}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}closure\ F\ {\isasymsubseteq}\ closure\ F{\isacharprime}{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nonFC{\isacharunderscore}covered{\isacharunderscore}def\ finite{\isacharunderscore}iso{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isachardoublequoteclose}{\isacharbrackright}\ FC{\isacharunderscore}family{\isacharunderscore}empty{\isacharunderscore}set{\isacharunderscore}insert\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}mono{\isacharbrackleft}of\ F\ {\isachardoublequoteopen}closure\ F{\isacharprime}{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}{\isasymnot}\ {\isasymnot}\ FC{\isacharunderscore}family\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ FC{\isacharunderscore}family{\isacharunderscore}closure{\isacharbrackleft}of\ F{\isacharprime}{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ FC{\isacharunderscore}family\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso\ F{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}iso{\isacharbrackleft}of\ {\isacharunderscore}\ F{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}mono{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ {\isasymF}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ closure{\isacharunderscore}mono{\isacharbrackleft}of\ F\ F{\isacharprime}{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}mono{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymsupseteq}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ {\isasymF}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ closure{\isacharunderscore}mono{\isacharbrackleft}of\ F{\isacharprime}\ F{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Covering and empty set%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}remove{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymlongrightarrow}\ FC{\isacharunderscore}covered\ Fc\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}remove{\isacharunderscore}empty{\isacharbrackleft}of\ F{\isacharbrackright}\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}remove{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ Nc\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymlongrightarrow}\ nonFC{\isacharunderscore}covered\ Nc\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}remove{\isacharunderscore}empty{\isacharbrackleft}of\ F{\isacharbrackright}\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ covered{\isacharunderscore}remove{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymlongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}remove{\isacharunderscore}empty{\isacharbrackleft}of\ F{\isacharbrackright}\ nonFC{\isacharunderscore}covered{\isacharunderscore}remove{\isacharunderscore}empty{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Covering and isomorphic families%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ Fc{\isacharprime}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ Fc{\isacharprime}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f\ g\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}Fc{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ g\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}sym{\isacharbrackleft}of\ Fc{\isacharprime}\ Fc{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ g\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ bij{\isacharunderscore}betw{\isacharunderscore}def{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}Fc{\isacharprime}\ {\isasymsubseteq}\ {\isasymUnion}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}mono{\isacharbrackleft}OF\ {\isacharbackquoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ F{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ g\ {\isacharparenleft}{\isasymUnion}Fc{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackleft}of\ {\isacharunderscore}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}{\isacharcomma}\ fact{\isacharplus}{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Fc{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ Fc{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ Fc{\isacharprime}{\isacharprime}{\isachardot}\ iso\ Fc{\isacharprime}{\isacharprime}\ Fc\ {\isasymand}\ Fc{\isacharprime}{\isacharprime}\ {\isasymsubseteq}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}Fc{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ {\isacharquery}Fc{\isacharprime}{\isacharprime}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ Fc{\isacharprime}\ {\isacharquery}Fc{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}g\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ g\ {\isacharparenleft}{\isasymUnion}Fc{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ bij{\isacharunderscore}betw{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ {\isacharquery}Fc{\isacharprime}{\isacharprime}\ Fc{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ iso{\isacharunderscore}sym{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso\ Fc{\isacharprime}\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ iso{\isacharunderscore}trans{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ Fc{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}g\ {\isacharbackquote}\ x\ {\isasymin}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ closure{\isacharunderscore}iso\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ F\ F{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ Nc\ F{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ Nc\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ Nc{\isacharprime}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ Nc\ Nc{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}closure\ F\ {\isasymsubseteq}\ closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f\ g\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}Nc{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Nc{\isachardoublequoteclose}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ g\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}sym{\isacharbrackleft}of\ Nc{\isacharprime}\ Nc{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ bij{\isacharunderscore}betw{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ {\isasymUnion}\ Nc{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}mono{\isacharbrackleft}OF\ {\isacharbackquoteopen}closure\ F\ {\isasymsubseteq}\ closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ g{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ g{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardot}\ g{\isacharprime}\ x\ {\isacharequal}\ g\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ g\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}inj{\isacharunderscore}extend{\isacharbrackleft}of\ g\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Nc{\isacharprime}\ {\isacharminus}\ {\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ Nc{\isacharprime}\ {\isacharminus}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Nc{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharcomma}\ metis\ sup{\isacharunderscore}absorb{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Nc{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ Nc{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}Nc{\isacharprime}{\isachardot}\ iso\ Nc\ Nc{\isacharprime}\ {\isasymand}\ closure\ F{\isacharprime}\ {\isasymsubseteq}\ closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}Nc{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ Nc\ {\isacharquery}Nc{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ Nc{\isacharprime}\ {\isacharquery}Nc{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ g{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}g{\isacharprime}\ \isakeyword{in}\ exI{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ bij{\isacharunderscore}betw{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso\ Nc\ Nc{\isacharprime}{\isacharbackquoteclose}iso{\isacharunderscore}trans\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}closure\ F{\isacharprime}\ {\isasymsubseteq}\ closure\ {\isacharparenleft}op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ Nc{\isacharprime}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ closure{\isacharunderscore}iso{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ closure\ F\ {\isacharequal}\ op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardot}\ g{\isacharprime}\ x\ {\isacharequal}\ g\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ map{\isacharunderscore}fam{\isacharunderscore}cong{\isacharbrackleft}of\ {\isachardoublequoteopen}closure\ F{\isachardoublequoteclose}\ g{\isacharprime}\ g{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ closure\ F\ {\isasymsubseteq}\ op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ {\isacharparenleft}closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}closure\ F\ {\isasymsubseteq}\ closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ {\isacharparenleft}closure\ Nc{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ closure\ {\isacharparenleft}op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ Nc{\isacharprime}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}iso{\isacharbrackleft}of\ g{\isacharprime}\ Nc{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ {\isacharparenleft}op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ Nc{\isacharprime}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ covered{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ F\ F{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ Fc\ {\isasymin}\ {\isasymF}{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ Nc\ {\isasymin}\ {\isasymN}{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ Nc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F\ {\isasymLongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharbrackleft}of\ F\ F{\isacharprime}{\isacharbrackright}\ nonFC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharbrackleft}of\ F\ F{\isacharprime}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}FCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ FF\ FFb\ {\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ set\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso{\isacharunderscore}represents\ FFb\ FF{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ FFb{\isachardot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ FF{\isachardot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ FF{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso{\isacharunderscore}represents\ FFb\ FF{\isacharbackquoteclose}\ iso{\isacharunderscore}sym\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fc\ \isakeyword{where}\ {\isachardoublequoteopen}Fc\ {\isasymin}\ {\isasymF}{\isachardoublequoteclose}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ FFb{\isachardot}\ FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ Fc\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ FF{\isacharbackquoteclose}\ FC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharbrackleft}of\ F{\isacharprime}\ F\ Fc{\isacharbrackright}\ {\isacharbackquoteopen}iso\ F{\isacharprime}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}FCs{\isacharunderscore}covered\ {\isasymF}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymin}\ {\isasymF}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}nonFCs{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ FF\ FFb\ {\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ set\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ FF{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ {\isasymN}{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso{\isacharunderscore}represents\ FFb\ FF{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ FFb{\isachardot}\ nonFCs{\isacharunderscore}covered\ {\isasymN}\ F{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ FF{\isachardot}\ nonFCs{\isacharunderscore}covered\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ FF{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso{\isacharunderscore}represents\ FFb\ FF{\isacharbackquoteclose}\ iso{\isacharunderscore}sym\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ N\ \isakeyword{where}\ {\isachardoublequoteopen}N\ {\isasymin}\ {\isasymN}{\isachardoublequoteclose}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ N\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ FFb{\isachardot}\ nonFCs{\isacharunderscore}covered\ {\isasymN}\ F{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ N\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ FF{\isacharbackquoteclose}\ nonFC{\isacharunderscore}covered{\isacharunderscore}iso{\isacharbrackleft}of\ F{\isacharprime}\ F\ N{\isacharbrackright}\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ FF{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ {\isasymN}{\isachardot}\ finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}iso\ F{\isacharprime}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}N\ {\isasymin}\ {\isasymN}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Covering, closure and irreducible families%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F\ {\isasymlongleftrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ covered{\isacharunderscore}def\ FC{\isacharunderscore}covered{\isacharunderscore}def\ nonFC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ex{\isacharunderscore}irreducible{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ F\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardot}\ irreducible\ F{\isacharprime}\ {\isasymand}\ {\isacharparenleft}covered\ {\isasymF}\ {\isasymN}\ F\ {\isasymlongleftrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardot}\ irreducible\ F{\isacharprime}\ {\isasymand}\ {\isacharparenleft}closure\ F\ {\isacharequal}\ closure\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ ex{\isacharunderscore}irreducible{\isacharunderscore}closure{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}covered\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ all{\isacharunderscore}irreducible{\isacharunderscore}covered{\isacharunderscore}all{\isacharunderscore}covered{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ F{\isachardot}\ irreducible\ F\ {\isasymand}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}\ {\isasymlongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isasymlongrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\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}n{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}{\isasymsubseteq}F{\isachardoublequoteclose}\ {\isachardoublequoteopen}irreducible\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F\ {\isasymlongleftrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ ex{\isacharunderscore}irreducible{\isacharunderscore}covered{\isacharbrackleft}of\ F\ {\isasymF}\ {\isasymN}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}irreducible\ F{\isacharprime}\ {\isasymand}\ {\isasymUnion}F{\isacharprime}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F{\isacharprime}{\isasymsubseteq}F{\isacharbackquoteclose}\ {\isacharbackquoteopen}irreducible\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ assms{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}covered\ {\isasymF}\ {\isasymN}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}covered\ {\isasymF}\ {\isasymN}\ F\ {\isasymlongleftrightarrow}\ covered\ {\isasymF}\ {\isasymN}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
