%
\begin{isabellebody}%
\setisabellecontext{WeightsShares{\isacharunderscore}FCFamily}%
%
\isamarkupsection{FC families characterization using shares (Poonen's theorem)%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ WeightsShares{\isacharunderscore}FCFamily\isanewline
\isakeyword{imports}\ WeightsShares{\isacharunderscore}Frankl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{HyperCube projection%
}
\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ hypercube{\isacharunderscore}prj\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}hypercube{\isacharunderscore}prj\ K\ S\ F\ {\isasymequiv}\ {\isacharparenleft}{\isasymlambda}S{\isachardot}\ S\ {\isacharminus}\ K{\isacharparenright}\ {\isacharbackquote}\ {\isacharparenleft}F\ {\isasyminter}\ op\ {\isasymunion}\ K\ {\isacharbackquote}\ Pow\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{syntax}\isamarkupfalse%
\isanewline
\ \ {\isachardoublequoteopen}{\isacharunderscore}hypercube{\isacharunderscore}prj{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymlangle}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isasymrangle}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{translations}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlangle}K{\isacharcomma}\ S{\isacharcomma}\ F{\isasymrangle}{\isachardoublequoteclose}\ {\isacharequal}{\isacharequal}\ {\isachardoublequoteopen}CONST\ hypercube{\isacharunderscore}prj\ K\ S\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ hypercube{\isacharunderscore}prj{\isacharunderscore}union{\isacharunderscore}closed{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isasymlangle}K{\isacharcomma}\ S{\isacharcomma}\ F{\isasymrangle}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}{\isacharparenleft}rule\ allI{\isacharparenright}{\isacharplus}{\isacharcomma}\ rule\ impI{\isacharcomma}\ erule\ conjE{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}hypercube{\isacharunderscore}prj\ K\ S\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}HC\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isasymunion}\ K\ {\isacharbackquote}\ Pow\ S{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}F{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ b\ \isakeyword{where}\ \isanewline
\ \ \ \ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isacharquery}HC{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ a\ {\isacharminus}\ K{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ Pow\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ {\isachardoublequoteopen}b\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isasymin}\ {\isacharquery}HC{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isacharequal}\ b\ {\isacharminus}\ K{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ Pow\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ {\isachardoublequoteopen}a\ {\isasymunion}\ b{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ \ \ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymin}\ F\ {\isasyminter}\ {\isacharquery}HC{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymunion}\ b\ {\isasymin}\ {\isacharquery}HC{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isasymunion}\ B{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isacharequal}\ a\ {\isasymunion}\ b\ {\isacharminus}\ K{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ hypercube{\isacharunderscore}prj{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}S\ {\isacharequal}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}K\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ {\isasymlangle}K{\isacharcomma}\ S{\isacharcomma}\ F{\isasymrangle}\ Fc{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlangle}K{\isacharcomma}\ S{\isacharcomma}\ F{\isasymrangle}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ hypercube{\isacharunderscore}prj{\isacharunderscore}union{\isacharunderscore}closed{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardot}\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}{\isacharparenright}\ {\isacharbackquote}\ Fc\ {\isasymsubseteq}\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ballI{\isacharcomma}\ rule\ subsetI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A{\isacharprime}\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isasymunion}\ A{\isacharprime}\ {\isacharbackquote}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y\ {\isasymunion}\ A{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}S\ {\isacharequal}\ {\isasymUnion}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ {\isachardoublequoteopen}K\ {\isasymunion}\ x{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ K\ {\isasymunion}\ x\ {\isacharminus}\ K{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}K\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymsubseteq}\ S{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasymunion}\ x\ {\isasymin}\ F\ {\isasyminter}\ op\ {\isasymunion}\ K\ {\isacharbackquote}\ Pow\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasymunion}\ x\ {\isasymin}\ op\ {\isasymunion}\ K\ {\isacharbackquote}\ Pow\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymsubseteq}\ S{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}y\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasymunion}\ A{\isacharprime}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasymunion}\ A{\isacharprime}\ {\isasymunion}\ y\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasymunion}\ x\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}x\ {\isacharequal}\ y\ {\isasymunion}\ A{\isacharprime}{\isacharbackquoteclose}{\isacharparenright}\ {\isacharparenleft}subst\ Un{\isacharunderscore}commute{\isacharbrackleft}of\ y\ A{\isacharprime}{\isacharbrackright}{\isacharcomma}\ subst\ Un{\isacharunderscore}assoc{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}w{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ K{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}K\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ K{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}S{\isacharprime}\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}K\ {\isasymunion}\ S{\isacharprime}{\isacharparenright}\ {\isacharequal}\ w\ {\isasymrhd}\isactrlsub s\ S{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ sum{\isachardot}union{\isacharunderscore}disjoint{\isacharbrackleft}of\ K\ {\isachardoublequoteopen}S{\isacharprime}{\isachardoublequoteclose}\ w{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ hypercube{\isacharunderscore}prj{\isacharunderscore}hyper{\isacharunderscore}share{\isacharunderscore}w{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ K{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ K{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ S\ F\ X{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ {\isasymlangle}K{\isacharcomma}\ S{\isacharcomma}\ F{\isasymrangle}\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ hyper{\isacharunderscore}share{\isacharunderscore}def\ family{\isacharunderscore}share{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}HCF\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}\ {\isasyminter}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}HCF{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}F\ {\isasyminter}\ op\ {\isasymunion}\ K\ {\isacharbackquote}\ Pow\ S{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}mK\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ S{\isachardot}\ S\ {\isacharminus}\ K{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}s\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}S{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharquery}mK\ {\isacharquery}HCF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}L{\isasymin}{\isacharquery}HCF{\isachardot}\ {\isacharquery}s\ L{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}L{\isasymin}{\isacharquery}HCF{\isacharprime}{\isachardot}\ {\isacharparenleft}{\isacharquery}s\ {\isasymcirc}\ {\isacharquery}mK{\isacharparenright}\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}HCF\ {\isacharequal}\ {\isacharquery}HCF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ hypercube{\isacharunderscore}Pow{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ L\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isasymin}\ {\isacharquery}HCF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}s\ L\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}s\ {\isasymcirc}\ {\isacharquery}mK{\isacharparenright}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}share{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ S{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}K\ {\isasymunion}\ x{\isacharparenright}\ {\isacharequal}\ w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}K\ {\isasymunion}\ x\ {\isacharminus}\ K{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}w{\isadigit{0}}{\isacharbrackleft}of\ K\ {\isachardoublequoteopen}K\ {\isasymunion}\ x\ {\isacharminus}\ K{\isachardoublequoteclose}\ w\ {\isachardoublequoteopen}K\ {\isasymunion}\ x\ {\isacharminus}\ K{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ K{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ K{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{All shares non-negative%
}
\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ w\ {\isasymequiv}\ {\isasymforall}\ F{\isacharprime}\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ frankl{\isacharunderscore}uce{\isacharunderscore}shares{\isacharunderscore}nonneg{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ w{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ frankl{\isacharunderscore}element\ a\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ a{\isachardot}\ frankl{\isacharunderscore}element\ a\ F\ {\isasymand}\ w\ a\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ frankl{\isacharunderscore}hyper{\isacharunderscore}share{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ K{\isasymin}Pow\ {\isacharparenleft}{\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc{\isacharparenright}{\isachardot}\ \ {\isacharparenleft}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ K\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasymin}\ Pow\ {\isacharparenleft}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ {\isacharparenleft}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ hypercube{\isacharunderscore}prj{\isacharunderscore}hyper{\isacharunderscore}share{\isacharunderscore}w{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ K{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}K\ {\isasymin}\ Pow\ {\isacharparenleft}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ K{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}K\ {\isasymin}\ Pow\ {\isacharparenleft}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}x{\isasymin}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ {\isasymlangle}K{\isacharcomma}\ {\isasymUnion}Fc{\isacharcomma}\ F{\isasymrangle}\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}P\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlangle}K{\isacharcomma}\ {\isasymUnion}Fc{\isacharcomma}\ F{\isasymrangle}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ {\isacharquery}P\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}{\isasymforall}\ F{\isacharprime}\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}P\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}P\ {\isasymsubseteq}\ Pow\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}K\ {\isasyminter}\ {\isasymUnion}\ Fc\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}K\ {\isasymin}\ Pow\ {\isacharparenleft}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ {\isacharquery}P\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ hypercube{\isacharunderscore}prj{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharbrackleft}of\ F\ Fc\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\ K{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}K\ {\isasymin}\ Pow\ {\isacharparenleft}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}\ {\isacharequal}\ w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc\ {\isasymunion}\ {\isasymUnion}\ Fc\ {\isacharequal}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}w{\isadigit{0}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\ w\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardot}\ w\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\ set{\isacharunderscore}share{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc\ {\isasymunion}\ {\isasymUnion}Fc\ {\isacharequal}\ {\isasymUnion}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ assms{\isacharparenright}\isanewline
\isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ \ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}w\ a\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{moreover}\isamarkupfalse%
\isanewline
\isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ Fc\ {\isasymor}\ a\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymnotin}\ {\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc{\isachardot}\ w\ a\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}w\ a\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{ultimately}\isamarkupfalse%
\isanewline
\isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}uce{\isacharunderscore}shares{\isacharunderscore}nonneg{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ w{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ w{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}w{\isacharprime}\ \ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ a{\isachardot}\ if\ a\ {\isasymin}\ {\isasymUnion}\ Fc\ then\ w\ a\ else\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}a{\isasymin}{\isasymUnion}Fc{\isachardot}\ frankl{\isacharunderscore}element\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ frankl{\isacharunderscore}uce{\isacharunderscore}shares{\isacharunderscore}nonneg{\isacharparenright}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ Fc\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ {\isacharquery}w{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ weight{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ \isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}{\isasymUnion}F\ {\isacharminus}\ {\isasymUnion}Fc{\isachardot}\ {\isacharquery}w{\isacharprime}\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ {\isacharquery}w{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharprime}\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymsubseteq}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharquery}w{\isacharprime}\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}cong{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\ w\ {\isacharquery}w{\isacharprime}\ F{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ {\isacharparenleft}{\isacharquery}w{\isacharprime}\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ w{\isacharbackquoteclose}\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymin}\ {\isasymlbrace}Fc{\isasymrbrace}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ weight{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F\ {\isasymge}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\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:
