%
\begin{isabellebody}%
\setisabellecontext{IrreducibleFamilies}%
%
\isamarkupsection{Expressible sets and irrreducible families%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ IrreducibleFamilies\isanewline
\isakeyword{imports}\ UnionClosed\ \isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ expressible\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}expressible\ A\ F\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ F{\isacharprime}{\isachardot}\ F{\isacharprime}\ {\isasymsubseteq}\ F\ {\isasymand}\ F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymand}\ A\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}expressible\ A\ F\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardot}\ F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isachardot}\ A{\isacharprime}\ {\isasymsubseteq}\ A{\isacharparenright}\ {\isasymand}\ {\isasymUnion}\ F{\isacharprime}\ {\isacharequal}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ expressible{\isacharunderscore}closure{\isadigit{1}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}expressible\ A\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\ closure{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ expressible{\isacharunderscore}closure{\isadigit{2}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}expressible\ A\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}op\ {\isasymunion}\ A{\isacharparenright}\ {\isacharbackquote}\ {\isacharparenleft}closure\ F{\isacharparenright}\ {\isasymsubseteq}\ closure\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}expressible\ A\ F{\isacharbackquoteclose}\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ Pow\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expressible{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isasymunion}\ F{\isacharprime}\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymin}\ Pow\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}F{\isacharprime}{\isacharprime}\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ x\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}F{\isacharprime}{\isacharprime}\ {\isasymunion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ x\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ image{\isacharunderscore}iff{\isacharparenright}\ \isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ expressible{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}expressible\ A\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ closure\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}insert{\isacharbrackleft}of\ F\ A{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ expressible{\isacharunderscore}closure{\isadigit{1}}{\isacharbrackleft}of\ A\ F{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ expressible{\isacharunderscore}closure{\isadigit{2}}{\isacharbrackleft}of\ A\ F{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Irreducible families%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ reducible\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}reducible\ F\ {\isasymlongleftrightarrow}\isanewline
\ \ \ {\isacharparenleft}{\isasymexists}\ A\ F{\isacharprime}{\isachardot}\ A\ {\isasymin}\ F\ {\isasymand}\ F{\isacharprime}\ {\isasymsubseteq}\ F\ {\isasymand}\ F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymand}\ A\ {\isasymnotin}\ F{\isacharprime}\ {\isasymand}\ A\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ irreducible\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}irreducible\ F\ {\isasymequiv}\ {\isasymnot}\ reducible\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}reducible\ F\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ A\ {\isasymin}\ F{\isachardot}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ reducible{\isacharunderscore}def\ expressible{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Removing all expressible sets%
}
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ {\isacharparenleft}domintros{\isacharparenright}\ remove{\isacharunderscore}expressible\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible\ F\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ {\isacharparenleft}{\isasymexists}\ A\ {\isasymin}\ F{\isachardot}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}\ then\ \isanewline
\ \ \ \ \ \ \ let\ A\ {\isacharequal}\ SOME\ A{\isachardot}\ A\ {\isasymin}\ F\ {\isasymand}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ in\ remove{\isacharunderscore}expressible\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ else\isanewline
\ \ \ \ \ \ \ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ remove{\isacharunderscore}expressible{\isacharunderscore}dom{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ wf{\isacharunderscore}induct{\isacharbrackleft}of\ {\isachardoublequoteopen}measure\ card{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ card{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}{\isacharprime}a\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ measure\ card\ {\isasymlongrightarrow}\ finite\ y\ {\isasymlongrightarrow}\ remove{\isacharunderscore}expressible{\isacharunderscore}dom\ y{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ x{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ remove{\isacharunderscore}expressible{\isachardot}domintros{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymin}\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}expressible\ A\ {\isacharparenleft}x\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}A\ {\isacharequal}\ {\isachardoublequoteopen}SOME\ A{\isachardot}\ A\ {\isasymin}\ x\ {\isasymand}\ expressible\ A\ {\isacharparenleft}x\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}y\ {\isacharequal}\ {\isachardoublequoteopen}x\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ {\isacharquery}y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ {\isacharasterisk}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ measure\ card{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharcomma}\ rule\ card{\isacharunderscore}Diff{\isadigit{1}}{\isacharunderscore}less{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}A\ {\isasymin}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharplus}{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ {\isacharparenleft}lifting{\isacharparenright}\ someI{\isacharunderscore}ex{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}x\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ x{\isacharbackquoteclose}\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%
\ remove{\isacharunderscore}expressible{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible\ F\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ remove{\isacharunderscore}expressible{\isacharunderscore}dom{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ remove{\isacharunderscore}expressible{\isachardot}pinduct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ F{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}{\isasymexists}\ A\ {\isasymin}\ F{\isachardot}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isacharbackquoteclose}\ remove{\isacharunderscore}expressible{\isachardot}psimps{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isacharbackquoteclose}\ remove{\isacharunderscore}expressible{\isachardot}psimps{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ remove{\isacharunderscore}expressible{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ closure\ {\isacharparenleft}remove{\isacharunderscore}expressible\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ remove{\isacharunderscore}expressible{\isacharunderscore}dom{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ remove{\isacharunderscore}expressible{\isachardot}pinduct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ F{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}{\isasymexists}\ A\ {\isasymin}\ F{\isachardot}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isacharbackquoteclose}\ remove{\isacharunderscore}expressible{\isachardot}psimps{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}A\ {\isacharequal}\ {\isachardoublequoteopen}SOME\ A{\isachardot}\ A\ {\isasymin}\ F\ {\isasymand}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}closure\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ closure\ {\isacharparenleft}remove{\isacharunderscore}expressible\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ {\isacharquery}A{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ closure\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}SOME\ A{\isachardot}\ A\ {\isasymin}\ F\ {\isasymand}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}A\ {\isasymin}\ F\ {\isasymand}\ expressible\ {\isacharquery}A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ {\isacharparenleft}lifting{\isacharparenright}\ someI{\isacharunderscore}ex{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ expressible{\isacharunderscore}closure{\isacharbrackleft}of\ {\isacharquery}A\ {\isachardoublequoteopen}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharquery}A{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\ {\isacharparenleft}metis\ {\isacharparenleft}lifting{\isacharparenright}\ insert{\isacharunderscore}absorb{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isacharbackquoteclose}\ remove{\isacharunderscore}expressible{\isachardot}psimps{\isacharbrackleft}of\ F{\isacharbrackright}\ True\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ remove{\isacharunderscore}expressible{\isacharunderscore}irreducible{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}irreducible\ {\isacharparenleft}remove{\isacharunderscore}expressible\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}let\ F{\isacharprime}\ {\isacharequal}\ remove{\isacharunderscore}expressible\ F\ in\isanewline
\ \ \ \ \ \ \ \ \ {\isasymnot}\ {\isacharparenleft}{\isasymexists}\ A\ {\isasymin}\ F{\isacharprime}{\isachardot}\ expressible\ A\ {\isacharparenleft}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ remove{\isacharunderscore}expressible{\isacharunderscore}dom{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ remove{\isacharunderscore}expressible{\isachardot}pinduct{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ F{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}{\isasymexists}\ A\ {\isasymin}\ F{\isachardot}\ expressible\ A\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isacharbackquoteclose}\ remove{\isacharunderscore}expressible{\isachardot}psimps{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}remove{\isacharunderscore}expressible{\isacharunderscore}dom\ F{\isacharbackquoteclose}\ remove{\isacharunderscore}expressible{\isachardot}psimps{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\ reducible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ex{\isacharunderscore}irreducible{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ F\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardot}\ irreducible\ F{\isacharprime}\ {\isasymand}\ closure\ F{\isacharprime}\ {\isacharequal}\ closure\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ remove{\isacharunderscore}expressible{\isacharunderscore}closure{\isacharbrackleft}OF\ assms{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ remove{\isacharunderscore}expressible{\isacharunderscore}subset{\isacharbrackleft}OF\ assms{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ remove{\isacharunderscore}expressible{\isacharunderscore}irreducible{\isacharbrackleft}OF\ assms{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Uniqueness of irreducible subfamily for the given closure%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ irreducible{\isacharunderscore}closure{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}irreducible\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\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%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymnotin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}closure\ F\ {\isacharequal}\ closure\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fa\ \isakeyword{where}\ {\isachardoublequoteopen}Fa\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fa\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Fa\ {\isacharequal}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}Fa\ {\isacharminus}\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharquery}F{\isadigit{2}}\ {\isacharequal}\ {\isachardoublequoteopen}Fa\ {\isasyminter}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}F{\isadigit{1}}\ {\isasymsubseteq}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fa\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardot}\ A{\isacharprime}\ {\isasymin}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}closure\ F\ {\isacharequal}\ closure\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fa\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}f\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardot}\ F{\isacharprime}{\isacharprime}\ {\isasymsubseteq}\ F{\isacharprime}\ {\isasymand}\ F{\isacharprime}{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymand}\ A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardot}\ {\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isasymin}\ Pow\ F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}\ A{\isacharprime}\ {\isacharequal}\ Union\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardot}\ A{\isacharprime}\ {\isasymin}\ closure\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ image{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}fs\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ A{\isacharprime}{\isachardot}\ SOME\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharquery}F{\isadigit{2}}\ {\isasymunion}\ {\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}\ {\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}F{\isacharprime}{\isacharprime}\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\ A{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ Fa{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymnotin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}fs\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ someI{\isacharunderscore}ex{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharquery}f\ A{\isacharprime}{\isachardoublequoteclose}{\isacharcomma}\ OF\ {\isacharbackquoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isasymUnion}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}\ {\isasymsubseteq}\ {\isasymUnion}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharquery}fs\ A{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ someI{\isacharunderscore}ex{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharquery}f\ A{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharquery}F{\isadigit{1}}\ {\isasymsubseteq}\ {\isasymUnion}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}\ {\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ A{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ someI{\isacharunderscore}ex{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharquery}f\ A{\isacharprime}{\isachardoublequoteclose}{\isacharcomma}\ OF\ {\isacharbackquoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharquery}F{\isacharprime}{\isacharprime}\ {\isacharequal}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymUnion}\ Fa\ {\isacharequal}\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymnotin}\ {\isacharquery}F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fa\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}fs\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymsubseteq}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymUnion}\ Fa\ {\isacharequal}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ {\isacharquery}fs\ A{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ someI{\isacharunderscore}ex{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharquery}f\ A{\isacharprime}{\isachardoublequoteclose}{\isacharcomma}\ OF\ {\isacharbackquoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fa\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}F{\isacharprime}{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}Fa\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ Fa{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ Fa{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ Fa\ {\isacharminus}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ Fa{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}fs\ {\isacharbackquote}\ {\isacharquery}F{\isadigit{1}}{\isacharparenright}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ someI{\isacharunderscore}ex{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharquery}f\ A{\isacharprime}{\isachardoublequoteclose}{\isacharcomma}\ OF\ {\isacharbackquoteopen}{\isasymexists}\ F{\isacharprime}{\isacharprime}{\isachardot}\ {\isacharquery}f\ A{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbackquoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ Fa\ {\isacharminus}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}expressible\ A\ {\isacharparenleft}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}irreducible\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ reducible{\isacharunderscore}def\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ irreducible{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}irreducible\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}irreducible\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}F\ {\isacharequal}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ irreducible{\isacharunderscore}closure{\isacharprime}\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:
