%
\begin{isabellebody}%
\setisabellecontext{IrreducibleFamiliesImpl}%
%
\isamarkupsubsubsection{Implementation by sorted and distinct lists%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ IrreducibleFamiliesImpl\isanewline
\isakeyword{imports}\ IrreducibleFamilies\ UnionClosedImpl\ Combinatorics\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ expressible{\isacharunderscore}l\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}expressible{\isacharunderscore}l\ A\ F\ {\isasymequiv}\ A\ {\isasymin}\ set\ {\isacharparenleft}map\ Union{\isacharunderscore}l\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}soundness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}expressible{\isacharunderscore}l\ A\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}expressible\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\ \isacommand{obtain}\isamarkupfalse%
\ X{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}X{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ Union{\isacharunderscore}l\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ X\ \isakeyword{where}\ {\isachardoublequoteopen}set\ X\ {\isasymsubseteq}\ set\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}\ {\isasymle}\ length\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}lists{\isachardot}Union{\isacharunderscore}set{\isacharbrackleft}of\ X{\isacharprime}{\isacharbrackright}\ all{\isacharunderscore}subs{\isacharunderscore}set{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ X{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}subset{\isacharunderscore}ex{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ F{\isacharprime}{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fl{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}l{\isachardot}\ set\ F{\isacharprime}l\ {\isasymsubseteq}\ set\ Fl\ \ {\isasymand}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}l\ {\isacharequal}\ F{\isacharprime}\ {\isasymand}\ distinct\ F{\isacharprime}l\ {\isasymand}\ length\ F{\isacharprime}l\ {\isasymle}\ length\ Fl{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ Fl\ arbitrary{\isacharcolon}\ F{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ a\ Fl{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fl{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ F{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}set\ a{\isacharbraceright}\ {\isasymsubseteq}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fl{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymnotin}\ set\ Fl{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ a\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}l\ \isakeyword{where}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}set\ F{\isacharprime}l\ {\isasymsubseteq}\ set\ Fl{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isacharprime}l{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}l\ {\isacharequal}\ F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}set\ a{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ F{\isacharprime}l\ {\isasymle}\ length\ Fl{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}set\ a{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymnotin}\ set\ Fl{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ a\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}F{\isacharprime}l\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}completeness{\isacharunderscore}lemma{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fl{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}map\ set\ {\isacharparenleft}map\ Union{\isacharunderscore}l\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ Fl{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}l\ \isakeyword{where}\ {\isachardoublequoteopen}set\ F{\isacharprime}l\ {\isasymsubseteq}\ set\ Fl{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isacharprime}l{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}l\ {\isacharequal}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ F{\isacharprime}l\ {\isasymle}\ length\ Fl{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}subset{\isacharunderscore}ex{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ F{\isacharprime}l\ {\isasymge}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}l\ {\isacharequal}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ not{\isacharunderscore}less{\isacharunderscore}eq{\isacharunderscore}eq{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ F{\isacharprime}l\ {\isasymin}\ set\ {\isacharbrackleft}{\isadigit{1}}{\isachardot}{\isachardot}{\isacharless}length\ Fl\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ F{\isacharprime}l\ {\isasymge}\ {\isadigit{1}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ F{\isacharprime}l\ {\isasymle}\ length\ Fl{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}Union{\isacharunderscore}l\ F{\isacharprime}l{\isacharparenright}\ {\isasymin}\ {\isacharparenleft}set\ {\isasymcirc}\ Union{\isacharunderscore}l{\isacharparenright}\ {\isacharbackquote}\ set\ {\isacharparenleft}Combinatorics{\isachardot}combine\ Fl\ {\isacharparenleft}length\ F{\isacharprime}l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}sublist{\isacharbrackleft}of\ {\isachardoublequoteopen}set\ F{\isacharprime}l{\isachardoublequoteclose}\ Fl{\isacharbrackright}\ {\isacharbackquoteopen}set\ F{\isacharprime}l\ {\isasymsubseteq}\ set\ Fl{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ F{\isacharprime}l{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ F{\isacharprime}l\ {\isasymle}\ length\ Fl{\isacharbackquoteclose}\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ F{\isacharprime}l{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ SetUnionImpl{\isacharunderscore}lists{\isachardot}Union{\isacharunderscore}set{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}l\ {\isacharequal}\ F{\isacharprime}{\isacharbackquoteclose}{\isacharbrackleft}symmetric{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}nonempty{\isacharunderscore}subsets{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ SetUnionImpl{\isacharunderscore}lists{\isachardot}Union{\isacharunderscore}set{\isacharcomma}\ auto{\isacharcomma}\ force{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}completeness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sd\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}expressible\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}expressible{\isacharunderscore}l\ A\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sdff\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}nonempty{\isacharunderscore}subsets{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sdf\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}subset{\isacharbrackleft}of\ {\isacharunderscore}\ F\ {\isacharunderscore}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sdf\ {\isacharparenleft}map\ Union{\isacharunderscore}l\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}lists{\isachardot}Union{\isacharunderscore}inv\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}expressible\ {\isacharparenleft}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A\ {\isacharequal}\ {\isasymUnion}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ A\ {\isasymin}\ set\ {\isacharbackquote}\ set\ {\isacharparenleft}map\ Union{\isacharunderscore}l\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}completeness{\isacharunderscore}lemma{\isacharbrackleft}of\ F{\isacharprime}\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ expressible{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sd\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}sdf\ {\isacharparenleft}map\ Union{\isacharunderscore}l\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetImpl{\isacharunderscore}lists{\isachardot}set{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}map\ Union{\isacharunderscore}l\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F{\isacharparenright}{\isachardoublequoteclose}\ A{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
