%
\begin{isabellebody}%
\setisabellecontext{WeightsShares{\isacharunderscore}NotFCFamily}%
%
\isamarkupsection{nonFC families characterization using shares (Poonen's theorem)%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ WeightsShares{\isacharunderscore}NotFCFamily\isanewline
\isakeyword{imports}\ Main\ WeightsShares{\isacharunderscore}FCFamily\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}hypercube{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}S\ {\isacharequal}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}K\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}a\ {\isasymnotin}\ K{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}op\ {\isasymunion}\ K\ {\isacharbackquote}\ F{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ a\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ inj{\isacharcolon}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}op\ {\isasymunion}\ K{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}count\ a\ {\isacharparenleft}op\ {\isasymunion}\ K\ {\isacharbackquote}\ F{\isacharparenright}\ {\isacharequal}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}A\ {\isasymin}\ op\ {\isasymunion}\ K\ {\isacharbackquote}\ F{\isachardot}\ a\ {\isasymin}\ A{\isacharbraceright}\ {\isacharequal}\ op\ {\isasymunion}\ K\ {\isacharbackquote}\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymnotin}\ K{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}S\ {\isacharequal}\ {\isasymUnion}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}K\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ inj\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharasterisk}{\isacharparenright}\ {\isacharparenleft}rule\ card{\isacharunderscore}image{\isacharcomma}\ simp\ add{\isacharcolon}\ inj\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}op\ {\isasymunion}\ K\ {\isacharbackquote}\ F{\isacharparenright}\ {\isacharequal}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ card{\isacharunderscore}image{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ inj{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}op\ {\isasymunion}\ K\ {\isacharbackquote}\ F{\isacharparenright}{\isacharequal}\ frankl{\isacharunderscore}fun\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sum{\isacharunderscore}over{\isacharunderscore}spread{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ d\ c\ {\isacharcolon}{\isacharcolon}\ nat\ \isakeyword{and}\ f\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}d\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ c{\isacharbrackright}{\isachardot}\ f\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ int\ d\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}c{\isacharbrackright}{\isachardot}\ f\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ c{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isadigit{0}}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Suc\ c{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ c{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ upt{\isacharunderscore}add{\isacharunderscore}eq{\isacharunderscore}append{\isacharbrackleft}of\ {\isadigit{0}}\ {\isachardoublequoteopen}d\ {\isacharasterisk}\ c{\isachardoublequoteclose}\ {\isachardoublequoteopen}d\ {\isacharasterisk}\ {\isacharparenleft}Suc\ c{\isacharparenright}\ {\isacharminus}\ d\ {\isacharasterisk}\ c{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ add{\isachardot}commute{\isacharparenright}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardot}\ f\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ c{\isacharbrackright}{\isachardot}\ f\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ \ {\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardot}\ f\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardot}\ f\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ int\ d\ {\isacharasterisk}\ f\ c{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ s\ {\isasymin}\ set\ {\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardot}\ s\ div\ d\ {\isacharequal}\ c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ s\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}s\ {\isasymin}\ set\ {\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}s\ {\isasymge}\ d{\isacharasterisk}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}s\ {\isacharless}\ d{\isacharasterisk}Suc\ c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}s\ div\ d\ {\isacharequal}\ c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ split{\isacharunderscore}div{\isacharunderscore}lemma{\isacharbrackleft}of\ d\ c\ s{\isacharbrackright}\ {\isacharbackquoteopen}d\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardot}\ f\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}s{\isasymleftarrow}{\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardot}\ f\ c{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ interv{\isacharunderscore}sum{\isacharunderscore}list{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharunderscore}nat{\isacharparenright}{\isacharplus}\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}list{\isacharunderscore}triv{\isacharbrackleft}of\ {\isachardoublequoteopen}f\ c{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}d\ {\isacharasterisk}\ c{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ Suc\ c{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ int{\isacharunderscore}distrib{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ archimedean{\isacharunderscore}negative{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ x\ y\ {\isacharcolon}{\isacharcolon}\ int\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}y\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ d{\isachardot}\ x\ {\isacharplus}\ int\ d\ {\isacharasterisk}\ y\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isasymle}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y{\isacharless}{\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ k\ \isakeyword{where}\ {\isachardoublequoteopen}k\ {\isacharequal}\ {\isacharminus}y{\isachardoublequoteclose}\ {\isachardoublequoteopen}k\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharasterisk}\ k\ {\isasymge}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ False\ {\isacharbackquoteopen}k\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ k\ {\isachargreater}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ int{\isacharunderscore}distrib{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharequal}\ {\isacharminus}y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}nat\ {\isacharparenleft}x\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ Fc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}length\ c\ {\isacharequal}\ length\ Fs{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymexists}\ cj\ {\isasymin}\ set\ c{\isachardot}\ cj\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ F\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}let\ Fs{\isacharprime}\ {\isacharequal}\ Fs\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ in\ {\isacharparenleft}{\isasymforall}\ a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ \ int\ x\ {\isacharasterisk}\ y{\isacharparenright}\ {\isacharparenleft}zip\ c\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ Fs{\isacharprime}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}F\ {\isasymin}\ set\ Fs{\isachardot}\ F\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ Pow{\isacharunderscore}iff\ UnionE\ set{\isacharunderscore}mp{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F\ \isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}set\ Fs{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}sum{\isacharunderscore}c\ {\isacharequal}\ {\isachardoublequoteopen}sum{\isacharunderscore}list\ c{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}sum{\isacharunderscore}c\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ wj\ \isakeyword{where}\ {\isachardoublequoteopen}wj\ {\isasymin}\ set\ c{\isachardoublequoteclose}\ {\isachardoublequoteopen}wj\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymexists}\ wj\ {\isasymin}\ set\ c{\isachardot}\ wj\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ n\ \isakeyword{where}\ {\isachardoublequoteopen}n\ {\isacharless}\ length\ c{\isachardoublequoteclose}\ {\isachardoublequoteopen}c\ {\isacharbang}\ n\ {\isacharequal}\ wj{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ in{\isacharunderscore}set{\isacharunderscore}conv{\isacharunderscore}nth{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}mono{\isacharunderscore}single{\isacharunderscore}lt{\isacharunderscore}nat{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}length\ c{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharunderscore}{\isachardot}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isacharbang}\ c{\isachardoublequoteclose}\ n{\isacharbrackright}\ {\isacharbackquoteopen}wj\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}list{\isacharunderscore}sum{\isacharunderscore}nth{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ div{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ s\ div\ d\ {\isacharless}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\ s\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}s\ div\ d\ {\isasymle}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ div{\isacharunderscore}le{\isacharunderscore}mono{\isacharbrackleft}of\ s\ {\isachardoublequoteopen}d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ d\ {\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}s\ div\ d\ {\isacharless}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isacharquery}sum{\isacharunderscore}c\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ Divides{\isachardot}div{\isacharunderscore}mult{\isadigit{2}}{\isacharunderscore}eq\ div{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff\ neq{\isadigit{0}}{\isacharunderscore}conv{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Gs\ {\isacharequal}\ {\isachardoublequoteopen}spread\ c\ Fs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ {\isacharquery}Gs\ {\isacharequal}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ c\ {\isacharequal}\ length\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ length{\isacharunderscore}spread{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ i{\isachardot}\ i\ {\isacharless}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ i\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ i\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isacharless}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Gs\ {\isacharbang}\ i\ {\isasymin}\ set\ {\isacharquery}Gs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ {\isacharquery}Gs\ {\isacharequal}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ div\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Gs\ {\isacharbang}\ i\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}spread{\isacharbrackleft}of\ c\ Fs{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ div\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ i\ A\ B{\isachardot}\ i\ {\isacharless}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymand}\ A\ {\isasymin}\ Fc\ {\isasymand}\ B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ i\ {\isasymlongrightarrow}\ A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\ i\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}i\ {\isacharless}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ j\ \isakeyword{where}\ {\isachardoublequoteopen}j\ {\isacharless}\ length\ Fs{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}Gs\ {\isacharbang}\ i\ {\isacharequal}\ Fs\ {\isacharbang}\ j{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ {\isacharbackquoteopen}{\isasymforall}i{\isacharless}sum{\isacharunderscore}list\ c{\isachardot}\ spread\ c\ Fs\ {\isacharbang}\ i\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\ in{\isacharunderscore}set{\isacharunderscore}conv{\isacharunderscore}nth{\isacharparenright}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Gs\ {\isacharbang}\ i\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}F{\isasymin}set\ Fs{\isachardot}\ F\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ i{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}extensions{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ s\ A\ B{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymand}\ A\ {\isasymin}\ Fc\ {\isasymand}\ B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ div\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ Bd{\isachardot}\ {\isasymforall}\ d{\isachardot}\ finite\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isasymand}\ card\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}\ {\isasymand}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isasyminter}\ {\isacharquery}X\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Bd\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ d{\isachardot}\ {\isacharparenleft}SOME\ B{\isachardot}\ {\isacharparenleft}finite\ B\ {\isasymand}\ card\ B\ {\isacharequal}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}\ {\isasymand}\ B\ {\isasyminter}\ {\isacharquery}X\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}Bd{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule\ allI{\isacharcomma}\ rule\ someI{\isacharunderscore}ex{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}B{\isachardot}\ finite\ B\ {\isasymand}\ card\ B\ {\isacharequal}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}\ {\isasymand}\ B\ {\isasyminter}\ {\isacharquery}X\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}disjoint{\isacharunderscore}set{\isacharbrackleft}of\ {\isacharquery}X\ {\isachardoublequoteopen}d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}finite\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Bd\ \isakeyword{where}\ Bd{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ finite\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isasymand}\ card\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}\ {\isasymand}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isasyminter}\ {\isacharquery}X\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Bds\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ d\ s{\isachardot}\ set{\isacharunderscore}drop{\isacharunderscore}nth\ s\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Bds\ d\ s\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}{\isacharparenleft}rule\ allI{\isacharparenright}{\isacharplus}{\isacharcomma}\ rule\ impI{\isacharcomma}\ erule\ conjE{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\ s\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharless}\ card\ {\isacharparenleft}set{\isacharunderscore}drop{\isacharunderscore}nth\ s\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Bd\ {\isacharbackquoteopen}{\isacharquery}sum{\isacharunderscore}c\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ card{\isacharunderscore}set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharparenright}\ simp{\isacharunderscore}all\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Bds\ d\ s\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Hds\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ d\ s{\isachardot}\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isacharparenright}\ {\isacharbackquote}\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Hdl\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ d{\isachardot}\ {\isacharparenleft}map\ {\isacharparenleft}{\isacharquery}Hds\ d{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Hd\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ d{\isachardot}\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharparenright}\ {\isacharbackquote}\ Pow\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Fd\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ d{\isachardot}\ Fc\ {\isasymunion}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ s\ d{\isachardot}\ s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isacharbang}\ s\ {\isacharequal}\ {\isacharquery}Hds\ d\ s{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ s\ a{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ a\ {\isasymin}\ {\isacharquery}X\ {\isasymand}\ s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ \ \ \ \ \ \ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Hds\ d\ s{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharplus}{\isacharcomma}\ {\isacharparenleft}erule\ conjE{\isacharparenright}{\isacharplus}{\isacharcomma}\ rule\ frankl{\isacharunderscore}fun{\isacharunderscore}hypercube{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\ s\ d\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymnotin}\ set{\isacharunderscore}drop{\isacharunderscore}nth\ s\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}\ s{\isacharbrackright}\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\ s\ a\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}X{\isachardoublequoteclose}\ {\isachardoublequoteopen}s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}d\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}\ s{\isacharbrackright}\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ Fc\ {\isasyminter}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule{\isacharcomma}\ rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ Fc\ {\isasyminter}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ S\ S{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}S\ {\isasymin}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}S{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymin}\ S{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ s\ A\ \isakeyword{where}\ {\isachardoublequoteopen}s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isacharequal}\ A\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ x\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Bds\ d\ s\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}S\ {\isacharequal}\ A\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}S\ {\isasymin}\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isacharbackquoteclose}\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}\ s{\isacharbrackright}\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ Fc\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule{\isacharcomma}\ rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ Fc\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ S\ \isakeyword{where}\ {\isachardoublequoteopen}S\ {\isasymin}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymin}\ op\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharbackquote}\ Pow\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ x\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Bd\ card{\isacharunderscore}gt{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ S{\isacharbackquoteclose}\ {\isacharbackquoteopen}S\ {\isasymin}\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ Bd\ d{\isacharbackquoteclose}\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ \ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule{\isacharcomma}\ rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ S\ S{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}S\ {\isasymin}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymin}\ S{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}S\ {\isasymin}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ s\ B\ \isakeyword{where}\ {\isachardoublequoteopen}s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isacharequal}\ B\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}S{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}S\ {\isasymin}\ S{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymin}\ Bd\ d{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymnotin}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}drops{\isacharbrackleft}of\ s\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}{\isacharbrackright}\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}B\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}set\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}B\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymnotin}\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isacharbackquoteclose}\ {\isacharbackquoteopen}a\ {\isasymin}\ Bd\ d{\isacharbackquoteclose}\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ A\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymnotin}\ B\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ S{\isacharbackquoteclose}\ {\isacharbackquoteopen}S\ {\isacharequal}\ B\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}Bds\ d\ s{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ finite\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ finite\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\isanewline
\ \ \isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Si\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ a{\isachardot}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ s{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ s{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isacharquery}sum{\isacharunderscore}c{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ a{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymand}\ a\ {\isasymin}\ {\isacharquery}X\ {\isasymlongrightarrow}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ d\ {\isacharasterisk}\ {\isacharquery}Si\ a{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ a{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}{\isacharparenleft}rule\ allI{\isacharparenright}{\isacharplus}{\isacharcomma}\ rule\ impI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\ i\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ frankl{\isacharunderscore}fun\ i\ Fc\ {\isacharplus}\ frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ frankl{\isacharunderscore}fun{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharunderscore}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ Fc{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ finite\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ finite\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasyminter}\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ Fc\ {\isasyminter}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ Fc\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ {\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}Pow\ {\isacharquery}X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharplus}{\isacharcomma}\ rule\ frankl{\isacharunderscore}fun{\isacharunderscore}hypercube{\isacharparenright}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Bd\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d{\isachardot}\ {\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}Pow{\isacharbrackleft}of\ {\isacharquery}X{\isacharbrackright}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ a{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharplus}{\isacharcomma}\ rule\ frankl{\isacharunderscore}fun{\isacharunderscore}UN{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\ a\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto\ intro{\isacharbang}{\isacharcolon}\ finite{\isacharunderscore}imageI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ s\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}\ {\isasymsubseteq}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ \ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ d\ a\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ i\ j{\isachardot}\ i\ {\isacharless}\ length\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isasymand}\ j\ {\isacharless}\ length\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}\ {\isasymand}\ i\ {\isasymnoteq}\ j\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharquery}Hdl\ d\ {\isacharbang}\ i\ {\isasyminter}\ {\isacharquery}Hdl\ d\ {\isacharbang}\ j\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ i\ j\ a\ b\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}j\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\ {\isachardoublequoteopen}i\ {\isasymnoteq}\ j{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}j\ div\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isacharquery}Bds\ d\ i\ {\isasymunion}\ a\ {\isacharequal}\ {\isacharquery}Bds\ d\ j\ {\isasymunion}\ b{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Bd\ d\ {\isasyminter}\ {\isacharquery}X\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Bd\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ set\ Fs{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasymin}\ {\isasymUnion}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}j\ div\ d{\isacharparenright}{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}j\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymsubseteq}\ {\isacharquery}X{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasymsubseteq}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasyminter}\ {\isacharquery}Bds\ d\ i\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasyminter}\ {\isacharquery}Bds\ d\ j\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}b\ {\isasyminter}\ {\isacharquery}Bds\ d\ i\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasyminter}\ {\isacharquery}Bds\ d\ j\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset{\isacharbrackleft}OF\ {\isacharbackquoteopen}finite\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Bds\ d\ i\ {\isacharequal}\ {\isacharquery}Bds\ d\ j{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}Bds\ d\ i\ {\isasymunion}\ a\ {\isacharequal}\ {\isacharquery}Bds\ d\ j\ {\isasymunion}\ b{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Un{\isacharunderscore}iff\ {\isacharbackquoteopen}Bd\ d\ {\isasyminter}\ {\isasymUnion}Fc\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ {\isasymsubseteq}\ {\isasymUnion}Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inf{\isacharunderscore}sup{\isacharunderscore}absorb\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fastforce\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isasymnoteq}\ j{\isacharbackquoteclose}\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}inj{\isacharbrackleft}OF\ {\isacharbackquoteopen}finite\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ {\isacharparenleft}Bd\ d{\isacharparenright}\ {\isacharequal}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isacharplus}\ {\isadigit{1}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}j\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ a{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ a\ {\isasymin}\ {\isacharquery}X\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ s{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ d\ s\ a{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ a\ {\isasymin}\ {\isacharquery}X\ {\isasymand}\ s\ {\isacharless}\ d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ \ \ \ \ \ \ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Hds\ d\ s{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ comp{\isacharunderscore}def{\isacharparenright}\ {\isacharparenleft}tactic\ {\isacharverbatimopen}\ cong{\isacharunderscore}tac\ %
\isaantiq
context{}%
\endisaantiq
\ {\isadigit{1}}{\isacharverbatimclose}{\isacharcomma}\ simp{\isacharcomma}\ force{\isacharparenright}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ d\ a{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ s{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d{\isacharasterisk}{\isacharquery}sum{\isacharunderscore}c{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ int\ d\ {\isacharasterisk}\ {\isacharquery}Si\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}over{\isacharunderscore}spread\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ {\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Hd\ d{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ d\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ballI{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlambda}s{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}spread\ c\ Fs\ {\isacharbang}\ s{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ {\isasymcirc}\ {\isacharparenleft}{\isasymlambda}\ s{\isachardot}\ spread\ c\ Fs\ {\isacharbang}\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}{\isasymlambda}s{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ s{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isacharquery}sum{\isacharunderscore}c{\isacharbrackright}\ {\isacharequal}\ \ map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ {\isacharparenleft}spread\ c\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharasterisk}{\isacharcomma}\ subst\ map{\isacharunderscore}map{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\ subst\ {\isacharbackquoteopen}length\ {\isacharparenleft}spread\ c\ Fs{\isacharparenright}\ {\isacharequal}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\ subst\ map{\isacharunderscore}nth{\isacharbrackleft}of\ {\isachardoublequoteopen}spread\ c\ Fs{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}rule\ refl{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}{\isasymlambda}s{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Gs\ {\isacharbang}\ s{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isacharquery}sum{\isacharunderscore}c{\isacharbrackright}\ {\isacharequal}\ spread\ c\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ map{\isacharunderscore}spread{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Si\ a\ {\isacharequal}\ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ int\ x\ {\isacharasterisk}\ y{\isacharparenright}\ {\isacharparenleft}zip\ c\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ Fs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ listsum{\isacharunderscore}spread\ {\isacharbackquoteopen}length\ c\ {\isacharequal}\ length\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}let\ Fs{\isacharprime}\ {\isacharequal}\ Fs\ in\ {\isacharparenleft}{\isasymforall}a{\isasymin}{\isasymUnion}Fc{\isachardot}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymleftarrow}zip\ c\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ Fs{\isacharprime}{\isacharparenright}{\isachardot}\ int\ x\ {\isacharasterisk}\ y{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isasymexists}\ da{\isachardot}\ \ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ da\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ archimedean{\isacharunderscore}negative\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}da\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ a{\isachardot}\ SOME\ da{\isachardot}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ da\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}d\ {\isacharequal}\ {\isachardoublequoteopen}Max\ {\isacharparenleft}{\isacharquery}da\ {\isacharbackquote}\ {\isacharquery}X{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isacharquery}d\ {\isasymge}\ {\isacharquery}da\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymAnd}\ x\ y{\isachardot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isasymle}\ y\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ Max\ {\isacharparenleft}{\isacharquery}da\ {\isacharbackquote}\ {\isacharquery}X{\isacharparenright}\ {\isasymge}\ {\isacharquery}da\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ {\isacharparenleft}{\isacharquery}da\ a{\isacharparenright}\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule\ someI{\isacharunderscore}ex{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isasymexists}\ da{\isachardot}\ \ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ da\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ {\isacharquery}d\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}d\ {\isasymge}\ {\isacharquery}da\ a{\isachardoublequoteclose}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ {\isacharparenleft}{\isacharquery}da\ a{\isacharparenright}\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isacharquery}d\ {\isasymge}\ {\isacharquery}da\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ {\isacharparenleft}{\isacharquery}da\ a{\isacharparenright}\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ {\isacharquery}d\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}\ x\ y\ y{\isacharprime}\ z{\isachardot}\ {\isasymlbrakk}x\ {\isacharplus}\ int\ y\ {\isacharasterisk}\ z\ {\isacharless}\ {\isadigit{0}}{\isacharsemicolon}\ y\ {\isasymle}\ y{\isacharprime}{\isacharsemicolon}\ z\ {\isacharless}\ {\isadigit{0}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharplus}\ int\ y{\isacharprime}\ {\isacharasterisk}\ z\ {\isacharless}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\ y{\isacharprime}\ z\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharplus}\ int\ y\ {\isacharasterisk}\ z\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymle}\ y{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}z\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharplus}\ int\ y\ {\isacharasterisk}\ z\ {\isasymge}\ x\ {\isacharplus}\ int\ y{\isacharprime}\ {\isacharasterisk}\ z{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymle}\ y{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}z\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharplus}\ int\ y{\isacharprime}\ {\isacharasterisk}\ z\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharplus}\ int\ y\ {\isacharasterisk}\ z\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ {\isacharasterisk}{\isacharbrackleft}\isakeyword{where}\ y{\isacharequal}{\isachardoublequoteopen}{\isacharquery}da\ a{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\ fact{\isacharplus}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}d{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ d\ \isakeyword{where}\ {\isachardoublequoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ Fc\ {\isacharplus}\ int\ d\ {\isacharasterisk}\ {\isacharquery}Si\ a\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}F{\isachardot}\ Fc\ {\isasymsubseteq}\ F\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ \ union{\isacharunderscore}closed\ F\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ \ finite\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}a{\isasymin}{\isacharquery}X{\isachardot}\ card\ F\ {\isachargreater}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}Fd\ d{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ intro\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}\ {\isacharless}\ card\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isacharquery}X{\isachardot}\ frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ Hdl\ Hd\ Fd\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}Hdl\ {\isacharequal}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Hd\ {\isacharequal}\ {\isacharquery}Hd\ d{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fd\ {\isacharequal}\ Fc\ {\isasymunion}\ Hdl\ {\isasymunion}\ Hd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ Fc{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ Fc{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ Fc{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ Fc{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ Hdl{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ Hdl{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ i\ a\ \isakeyword{where}\ {\isachardoublequoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}d\ s\ A\ B{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c\ {\isasymand}\ A\ {\isasymin}\ Fc\ {\isasymand}\ B\ {\isasymin}\ spread\ c\ Fs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymunion}\ B\ {\isasymin}\ spread\ c\ Fs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymunion}\ a{\isacharparenright}\ {\isasymunion}\ {\isacharquery}Bds\ d\ i\ {\isasymin}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}i{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharcomma}\ auto{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymunion}\ a{\isacharparenright}\ {\isasymunion}\ {\isacharquery}Bds\ d\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}B\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ \ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ Fc{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ Hd{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ safe\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ Hd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ b\ \isakeyword{where}\ {\isachardoublequoteopen}b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isacharequal}\ b\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Hd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}B\ {\isacharequal}\ b\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ PowI\ Un{\isacharunderscore}assoc\ Un{\isacharunderscore}commute\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ Hdl{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ Hdl{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ safe\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Hdl{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ Hdl{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ i\ j\ a\ b\ \isakeyword{where}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isachardoublequoteclose}\ {\isachardoublequoteopen}j\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}b\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}j\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isacharequal}\ {\isacharquery}Bds\ d\ j\ {\isasymunion}\ b{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ set\ Fs{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasymin}\ {\isasymUnion}\ set\ Fs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isacharless}\ d{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c\ {\isasymlongrightarrow}\ spread\ c\ Fs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymsubseteq}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}F{\isasymin}set\ Fs{\isachardot}\ {\isasymUnion}F\ {\isasymsubseteq}\ {\isasymUnion}Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}i\ {\isacharequal}\ j{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}j\ div\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}F{\isasymin}set\ Fs{\isachardot}\ F\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isacharbackquoteclose}\ div\ {\isacharbackquoteopen}length\ {\isacharquery}Gs\ {\isacharequal}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}F{\isasymin}set\ Fs{\isachardot}\ {\isasymUnion}F\ {\isasymsubseteq}\ {\isasymUnion}Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}extensions{\isacharunderscore}def\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}def\ union{\isacharunderscore}closed{\isacharunderscore}def\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isacharless}\ d{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}i{\isacharless}sum{\isacharunderscore}list\ c{\isachardot}\ spread\ c\ Fs\ {\isacharbang}\ i\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\ {\isacharbackquoteopen}j\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}a\ {\isasymunion}\ b{\isacharparenright}\ {\isasymunion}\ {\isacharquery}Bds\ d\ i\ {\isasymin}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}i{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharcomma}\ auto{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isacharequal}\ {\isacharquery}Bds\ d\ j\ {\isasymunion}\ b{\isacharbackquoteclose}\ {\isacharbackquoteopen}i\ {\isacharequal}\ j{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ Un{\isacharunderscore}assoc\ Un{\isacharunderscore}commute\ sup{\isachardot}right{\isacharunderscore}idem{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Bds\ d\ i\ {\isasymunion}\ {\isacharquery}Bds\ d\ j\ {\isacharequal}\ Bd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\ {\isacharbackquoteopen}j\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}distinct{\isacharbrackleft}of\ i\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}distinct{\isacharbrackleft}of\ j\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ length{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}{\isacharbrackright}\ Bd\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nth{\isacharunderscore}eq{\isacharunderscore}iff{\isacharunderscore}index{\isacharunderscore}eq{\isacharbrackleft}of\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ i\ j{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Hd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isacharequal}\ {\isacharquery}Bds\ d\ j\ {\isasymunion}\ b{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymunion}\ b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ PowI\ Un{\isacharunderscore}assoc\ image{\isacharunderscore}iff\ sup{\isacharunderscore}left{\isacharunderscore}commute{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ Hdl{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ Hd{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ safe\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Hdl{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ Hd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ i\ a\ b\ \isakeyword{where}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}i\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}i\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isacharequal}\ b\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ blast\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymsubseteq}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{0}}\ {\isacharless}\ d{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c\ {\isasymlongrightarrow}\ spread\ c\ Fs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}F{\isasymin}set\ Fs{\isachardot}\ {\isasymUnion}F\ {\isasymsubseteq}\ {\isasymUnion}Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ {\isacharparenleft}mono{\isacharunderscore}tags{\isacharcomma}\ lifting{\isacharparenright}\ Union{\isacharunderscore}upper\ le{\isacharunderscore}supI\ neq{\isadigit{0}}{\isacharunderscore}conv\ subset{\isacharunderscore}trans{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}a\ {\isasymunion}\ b{\isacharparenright}\ {\isasymunion}\ Bd\ d\ {\isasymin}\ {\isacharquery}Hd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Bds\ d\ i\ {\isasymunion}\ Bd\ d\ {\isacharequal}\ Bd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset\ Bd\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Hd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ {\isacharquery}Bds\ d\ i\ {\isasymunion}\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isacharequal}\ b\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ Un{\isacharunderscore}left{\isacharunderscore}commute\ sup{\isacharunderscore}assoc{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ Hd{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ Hd{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ safe\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ Hd{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ Hd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ b\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ a\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isacharequal}\ b\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}Hd\ d{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ a\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isacharequal}\ b\ {\isasymunion}\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ PowI\ Un{\isacharunderscore}commute\ image{\isacharunderscore}iff\ sup{\isachardot}right{\isacharunderscore}idem\ sup{\isacharunderscore}left{\isacharunderscore}commute{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ Fd{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fd\ {\isacharequal}\ Fc\ {\isasymunion}\ Hdl\ {\isasymunion}\ Hd{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ UnE\ Un{\isacharunderscore}commute{\isacharparenright}{\isacharplus}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}{\isacharquery}Fd\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ Bd\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}{\isasymUnion}x{\isasymin}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}d\ {\isacharasterisk}\ sum{\isacharunderscore}list\ c{\isacharbraceright}{\isachardot}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ op\ {\isasymunion}\ {\isacharparenleft}set{\isacharunderscore}drop{\isacharunderscore}nth\ x\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharparenright}\ {\isacharbackquote}\ spread\ c\ Fs\ {\isacharbang}\ {\isacharparenleft}x\ div\ d{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ d{\isachardot}\ d\ {\isachargreater}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ finite\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}{\isacharquery}Hdl\ d{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}set{\isacharunderscore}drop{\isacharunderscore}nth\ a\ {\isacharparenleft}Bd\ d{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Bd\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}Bd\ d{\isachardoublequoteclose}\ a{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\ x\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ spread\ c\ Fs\ {\isacharbang}\ {\isacharparenleft}a\ div\ d{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}set\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ d\ s{\isachardot}\ d\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymand}\ s\ {\isacharless}\ d\ {\isacharasterisk}\ {\isacharquery}sum{\isacharunderscore}c\ {\isasymlongrightarrow}\ {\isacharquery}Gs\ {\isacharbang}\ {\isacharparenleft}s\ div\ d{\isacharparenright}\ {\isasymin}\ set\ Fs{\isacharbackquoteclose}\ {\isacharbackquoteopen}d\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ set\ Fs{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isachardot}\ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharquery}X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ linorder{\isacharunderscore}not{\isacharunderscore}less{\isacharparenright}\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:
