%
\begin{isabellebody}%
\setisabellecontext{LPartitioning}%
%
\isamarkupsection{L-partitioned families%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ LPartitioning\isanewline
\isakeyword{imports}\ Main\ More{\isachardot}MoreSet\ IsomorphicFamilies\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ \ {\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharcolon}{\isacharcolon}nat{\isacharbraceright}\ {\isasymand}\isanewline
\ \ \ \ \ {\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharless}\ length\ L{\isacharparenright}\ {\isasymand}\isanewline
\ \ \ \ \ {\isacharparenleft}{\isasymforall}\ n\ {\isacharless}\ length\ L{\isachardot}\ card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ n{\isacharbraceright}\ {\isacharequal}\ L\ {\isacharbang}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ L{\isacharunderscore}part\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}L{\isacharunderscore}part\ n\ L\ {\isasymequiv}\ {\isacharbraceleft}F{\isachardot}\ is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}finite{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ finite\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zero{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F\ {\isasymlongleftrightarrow}\ is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharless}\ length\ L{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharless}\ length\ L\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\ card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ length\ L{\isacharbraceright}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\ fastforce\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}append\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}na\ {\isacharequal}\ length\ L{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharplus}{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zeros{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ k{\isacharprime}{\isachardot}\ k{\isacharprime}\ {\isachargreater}\ k\ {\isasymand}\ k{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F\ {\isasymlongleftrightarrow}\ is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}take\ {\isacharparenleft}k{\isacharplus}{\isadigit{1}}{\isacharparenright}\ L{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharless}\ length\ L{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ L\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}snoc\ a\ L{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ length\ L{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isacharless}\ length\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}k{\isacharprime}{\isachardot}\ k\ {\isacharless}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}\ {\isacharless}\ length\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}\ {\isacharbang}\ k{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ {\isachardoublequoteopen}length\ L{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}k{\isacharprime}{\isachardot}\ k\ {\isacharless}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L\ {\isacharbang}\ k{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}k{\isacharprime}{\isachardot}\ k\ {\isacharless}\ k{\isacharprime}\ {\isasymand}\ k{\isacharprime}\ {\isacharless}\ length\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}\ {\isacharbang}\ k{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}append{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zero{\isacharbrackleft}of\ n\ L\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zeros{\isacharunderscore}replicate{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}replicate\ k\ {\isadigit{0}}{\isacharparenright}\ F\ {\isasymlongleftrightarrow}\ \ is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharbrackleft}{\isacharbrackright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ k{\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\ k{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ replicate{\isacharunderscore}add{\isacharbrackleft}of\ k\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}{\isacharbrackright}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}zero{\isacharbrackleft}of\ n\ {\isachardoublequoteopen}replicate\ k\ {\isadigit{0}}{\isachardoublequoteclose}\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}mem{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ A\ {\isacharless}\ length\ L\ {\isasymand}\ L\ {\isacharbang}\ card\ A\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ card\ A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}X\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharquery}X\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isacharquery}X\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ {\isacharquery}X{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A\ {\isacharless}\ length\ L\ {\isasymand}\ L\ {\isacharbang}\ card\ A\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}empty{\isacharunderscore}mem{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}hd\ L\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ L\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}A{\isadigit{0}}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isacharbraceright}\ {\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharquery}A{\isadigit{0}}\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ hd{\isacharunderscore}conv{\isacharunderscore}nth{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}gt{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}remove{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L{\isacharbrackleft}card\ A\ {\isacharcolon}{\isacharequal}\ {\isacharparenleft}L\ {\isacharbang}\ card\ A{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ card\ A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}XA\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharquery}X\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}L{\isacharbrackleft}card\ A\ {\isacharcolon}{\isacharequal}\ {\isacharparenleft}L\ {\isacharbang}\ card\ A{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ n{\isachardot}\ n\ {\isasymnoteq}\ card\ A\ {\isasymlongrightarrow}\ {\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ n{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ card\ A{\isacharbraceright}\ {\isacharequal}\ {\isacharquery}XA{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}L\ {\isacharbang}\ card\ A\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}mem{\isacharbrackleft}of\ n\ L\ F\ A{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharquery}X\ {\isacharequal}\ L\ {\isacharbang}\ card\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}card\ A\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isacharbang}\ card\ A\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isacharparenleft}L\ {\isacharbang}\ card\ A{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}mem{\isacharbrackleft}of\ n\ L\ F\ A{\isacharbrackright}\ {\isacharbackquoteopen}L\ {\isacharbang}\ card\ A\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharquery}XA\ {\isacharequal}\ {\isacharparenleft}L\ {\isacharbang}\ card\ A{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ {\isacharquery}X\ {\isacharequal}\ L\ {\isacharbang}\ card\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Suc{\isacharprime}{\isacharbrackleft}of\ {\isacharquery}X\ {\isachardoublequoteopen}{\isacharparenleft}L\ {\isacharbang}\ card\ A{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ A{\isacharbrackright}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharquery}F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A{\isacharprime}\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymforall}n\ {\isacharless}\ length\ {\isacharquery}L{\isacharprime}{\isachardot}\ card\ {\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ n{\isacharbraceright}\ {\isacharequal}\ {\isacharquery}L{\isacharprime}\ {\isacharbang}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}n{\isacharprime}\ {\isacharless}\ length\ {\isacharquery}L{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharbraceleft}A{\isacharprime}\ {\isasymin}\ {\isacharquery}F{\isachardot}\ card\ A{\isacharprime}\ {\isacharequal}\ n{\isacharprime}{\isacharbraceright}\ {\isacharequal}\ {\isacharquery}L{\isacharprime}\ {\isacharbang}\ n{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n{\isacharprime}\ {\isasymnoteq}\ card\ A{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}n{\isacharprime}\ {\isacharless}\ length\ {\isacharquery}L{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharbackquoteopen}card\ {\isacharquery}XA\ {\isacharequal}\ {\isacharparenleft}L\ {\isacharbang}\ card\ A{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ A\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}remove{\isacharunderscore}last{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ F{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ \ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}remove{\isacharbrackleft}of\ A\ F\ n\ {\isachardoublequoteopen}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}insert{\isacharunderscore}last{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymnotin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}finite{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ n\ {\isacharless}\ length\ L{\isachardot}\ {\isacharbraceleft}X\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardot}\ card\ X\ {\isacharequal}\ n{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}X\ {\isasymin}\ F{\isachardot}\ card\ X\ {\isacharequal}\ n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}X\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardot}\ card\ X\ {\isacharequal}\ length\ L{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}X\ {\isasymin}\ F{\isachardot}\ card\ X\ {\isacharequal}\ length\ L{\isacharbraceright}\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}{\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}X{\isasymin}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardot}\ card\ X\ {\isacharless}\ length\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}n{\isacharprime}\ {\isacharless}\ length\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharbraceleft}X\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardot}\ card\ X\ {\isacharequal}\ n{\isacharprime}{\isacharbraceright}\ {\isacharequal}\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ {\isacharbang}\ n{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n{\isacharprime}\ {\isacharless}\ length\ L{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ nth{\isacharunderscore}append{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}n{\isacharprime}\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}n{\isacharprime}\ {\isacharless}\ length\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}insert{\isacharunderscore}disjoint{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ length\ L{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ nth{\isacharunderscore}append\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Ordering of L-partitions%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ pwge\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsucceq}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ L\ {\isasymlongleftrightarrow}\ {\isacharparenleft}length\ L{\isacharprime}\ {\isacharequal}\ length\ L{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ i\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ L{\isacharprime}\ {\isacharbang}\ i\ {\isasymge}\ L\ {\isacharbang}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}Cons{\isacharcolon}\isanewline
\ {\isachardoublequoteopen}{\isacharparenleft}a\ {\isacharhash}\ L{\isacharparenright}\ {\isasymsucceq}\ {\isacharparenleft}b\ {\isacharhash}\ L{\isacharprime}{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}a\ {\isasymge}\ b\ {\isasymand}\ L\ {\isasymsucceq}\ L{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}Cons{\isacharparenright}\ {\isacharparenleft}metis\ Suc{\isacharunderscore}eq{\isacharunderscore}plus{\isadigit{1}}{\isacharunderscore}left\ diff{\isacharunderscore}is{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}eq\ le{\isacharunderscore}add{\isacharunderscore}diff{\isacharunderscore}inverse\ le{\isacharunderscore}cases\ less{\isacharunderscore}antisym\ less{\isacharunderscore}imp{\isacharunderscore}diff{\isacharunderscore}less\ nth{\isacharunderscore}Cons\ nth{\isacharunderscore}Cons{\isacharprime}{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\ \isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}Nil{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymsucceq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}refl{\isacharcolon}\isanewline
\isakeyword{fixes}\ L{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}linorder\ list{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}L\ {\isasymsucceq}\ L{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}trans\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ L{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}linorder\ list{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}L\ {\isasymsucceq}\ L{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}L\ {\isasymsucceq}\ L{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ L\ arbitrary{\isacharcolon}\ L{\isacharprime}\ L{\isacharprime}{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ a\ l{\isacharparenright}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ b\ l{\isacharprime}\ c\ l{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isacharequal}\ b\ {\isacharhash}\ l{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}L{\isacharprime}{\isacharprime}\ {\isacharequal}\ c\ {\isacharhash}\ l{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharparenleft}a\ {\isacharhash}\ l{\isacharparenright}\ {\isasymsucceq}\ L{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isacharprime}{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ Suc{\isacharunderscore}length{\isacharunderscore}conv{\isacharparenright}\ \isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}Cons{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}replicate{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}length\ X\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}X\ {\isasymsucceq}\ replicate\ n\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ n\ arbitrary{\isacharcolon}\ X{\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\ n{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ X{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}Cons{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ pwge{\isacharunderscore}list{\isacharunderscore}update{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ L{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ list{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}n\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}nk\ {\isasymle}\ L\ {\isacharbang}\ n{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}L\ {\isasymsucceq}\ L\ {\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ nk{\isacharbrackright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}list{\isacharunderscore}update{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}L{\isacharprime}\ {\isasymsucceq}\ L{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ F{\isachardot}\ F\ {\isasymsubseteq}\ F{\isacharprime}\ {\isasymand}\ \ is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isacharprime}k\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ k{\isachardot}\ {\isacharbraceleft}A{\isachardot}\ A\ {\isasymin}\ F{\isacharprime}\ {\isasymand}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Fk\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ k{\isachardot}\ SOME\ S{\isachardot}\ S\ {\isasymsubseteq}\ {\isacharquery}F{\isacharprime}k\ k\ {\isasymand}\ card\ S\ {\isacharequal}\ L\ {\isacharbang}\ k{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ k{\isachardot}\ k\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ S{\isachardot}\ S\ {\isasymsubseteq}\ {\isacharquery}F{\isacharprime}k\ k\ {\isasymand}\ card\ S\ {\isacharequal}\ L\ {\isacharbang}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ S{\isachardot}\ S\ {\isasymsubseteq}\ {\isacharquery}F{\isacharprime}k\ k\ {\isasymand}\ card\ S\ {\isacharequal}\ L\ {\isacharbang}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ card{\isacharunderscore}le{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}L\ {\isacharbang}\ k\ {\isasymle}\ L{\isacharprime}\ {\isacharbang}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}k\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isacharquery}F{\isacharprime}k\ k{\isacharparenright}\ {\isacharequal}\ L{\isacharprime}\ {\isacharbang}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}k\ {\isacharless}\ length\ L{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ pwge{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ k\ {\isacharless}\ length\ L{\isachardot}\ {\isacharquery}Fk\ k\ {\isasymsubseteq}\ {\isacharquery}F{\isacharprime}k\ k\ {\isasymand}\ card\ {\isacharparenleft}{\isacharquery}Fk\ k{\isacharparenright}\ {\isacharequal}\ L\ {\isacharbang}\ k\ {\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isacharless}\ length\ L{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}Fk\ k\ {\isasymLongrightarrow}\ x\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}Fk\ k\ {\isasymLongrightarrow}\ card\ x\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isacharquery}Fk\ k{\isacharparenright}\ {\isacharequal}\ L\ {\isacharbang}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ k{\isachardot}\ k\ {\isacharless}\ length\ L\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ S{\isachardot}\ S\ {\isasymsubseteq}\ {\isacharquery}F{\isacharprime}k\ k\ {\isasymand}\ card\ S\ {\isacharequal}\ L\ {\isacharbang}\ k{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ tfl{\isacharunderscore}some{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ \isakeyword{where}\ P{\isacharequal}{\isachardoublequoteopen}{\isasymlambda}\ S{\isachardot}\ S\ {\isasymsubseteq}\ {\isacharbraceleft}A\ {\isasymin}\ F{\isacharprime}{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}\ {\isasymand}\ card\ S\ {\isacharequal}\ L\ {\isacharbang}\ k{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharbraceleft}{\isacharquery}Fk\ k\ {\isacharbar}\ k\ {\isachardot}\ k\ {\isacharless}\ length\ L{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}F{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharquery}F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}{\isacharquery}F{\isachardot}\ card\ A\ {\isacharless}\ length\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}k{\isacharless}length\ L{\isachardot}\ {\isacharbraceleft}A\ {\isasymin}\ {\isacharquery}F{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}\ {\isacharequal}\ {\isacharquery}Fk\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}k{\isacharless}length\ L{\isachardot}\ card\ {\isacharbraceleft}A\ {\isasymin}\ {\isacharquery}F{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}\ {\isacharequal}\ L\ {\isacharbang}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}subset{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ L{\isacharprime}{\isachardot}\ L\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ \ is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}F\ {\isacharminus}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\ \ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isacharminus}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isachardoublequoteclose}{\isacharbrackright}\ finiteUn{\isacharunderscore}iff{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ {\isachardoublequoteopen}F\ {\isacharminus}\ F{\isacharprime}{\isachardoublequoteclose}\ arbitrary{\isacharcolon}\ F\ F{\isacharprime}\ L\ rule{\isacharcolon}\ finite{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ empty\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isacharequal}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}L{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ pwge{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}insert\ X\ Y{\isacharparenright}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}insert\ X\ Y\ {\isacharequal}\ F\ {\isacharminus}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ L{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}L\ {\isasymsucceq}\ L{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}{\isacharprime}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}X{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}remove{\isacharbrackleft}of\ X\ F\ n\ L{\isacharbrackright}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}list{\isacharunderscore}update{\isacharbrackleft}of\ {\isachardoublequoteopen}card\ X{\isachardoublequoteclose}\ L\ {\isachardoublequoteopen}{\isacharparenleft}L\ {\isacharbang}\ card\ X{\isacharparenright}\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}mem\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ L{\isacharprime}{\isachardot}\ L{\isacharprime}{\isacharprime}\ {\isasymsucceq}\ L{\isacharprime}\ {\isasymand}\ is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ insert{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Y\ {\isacharequal}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}X{\isacharbraceright}{\isacharparenright}\ {\isacharminus}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}insert\ X\ Y\ {\isacharequal}\ F\ {\isacharminus}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}X\ {\isasymnotin}\ Y{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F\ {\isacharminus}\ {\isacharbraceleft}X{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}insert\ X\ Y\ {\isacharequal}\ F\ {\isacharminus}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ L{\isacharprime}{\isacharprime}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}X{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}L\ {\isasymsucceq}\ L{\isacharprime}{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pwge{\isacharunderscore}trans{\isacharbrackleft}of\ L\ L{\isacharprime}{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsection{Generating all L-partitioned families with some given properties%
}
\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}P\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ L\ {\isasymequiv}\ {\isacharbraceleft}F\ {\isasymin}\ L{\isacharunderscore}part\ n\ L{\isachardot}\ P\ F{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ mult{\isacharunderscore}P\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}mult{\isacharunderscore}P\ P\ F\ A\ {\isasymequiv}\ {\isacharbraceleft}f\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}\ {\isacharbar}\ f{\isachardot}\ f\ {\isasymin}\ F\ {\isasymand}\ A\ {\isasymnotin}\ f\ {\isasymand}\ P\ A\ f{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\isanewline
\ {\isachardoublequoteopen}mult{\isacharunderscore}all{\isacharunderscore}P\ P\ F\ n\ m\ {\isasymequiv}\ {\isasymUnion}\ {\isacharbraceleft}mult{\isacharunderscore}P\ P\ F\ A\ {\isacharbar}\ A{\isachardot}\ card\ A\ {\isacharequal}\ m\ {\isasymand}\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ incrementally{\isacharunderscore}checks\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ Pinc\ P\ {\isasymequiv}\isanewline
\ \ \ \ \ \ {\isacharparenleft}{\isasymforall}\ A\ F{\isachardot}\ {\isacharparenleft}finite\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isasymge}\ card\ A{\isacharprime}{\isacharparenright}\ {\isasymand}\ A\ {\isasymnotin}\ F{\isacharparenright}\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}P\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isasymlongleftrightarrow}\ P\ F\ {\isasymand}\ Pinc\ A\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}P{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ Pinc\ P{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}P\ Pinc\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isasymsubseteq}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}P\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isacharprime}{\isachardot}\ card\ A\ {\isacharequal}\ length\ L{\isacharbraceright}\ {\isacharequal}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}A\ {\isasymin}\ F{\isacharprime}{\isachardot}\ card\ A\ {\isacharequal}\ length\ L{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ {\isacharbraceleft}f\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}\ {\isacharbar}f{\isachardot}\isanewline
\ \ \ \ \ \ \ \ \ \ f\ {\isasymin}\ L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ P\ f\ {\isasymand}\ A\ {\isasymnotin}\ f\ {\isasymand}\ Pinc\ A\ f{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharcomma}\ rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}F{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ {\isacharquery}F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}remove{\isacharunderscore}last\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}{\isacharparenleft}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharparenleft}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\ finiteUn{\isacharunderscore}iff{\isacharbrackleft}of\ F{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymforall}A{\isacharprime}{\isasymin}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardot}\ card\ A{\isacharprime}\ {\isasymle}\ card\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Pinc\ A\ {\isacharquery}F{\isachardoublequoteclose}\ {\isachardoublequoteopen}P\ {\isacharparenleft}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}P\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}absorb{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}rhs\ {\isasymsubseteq}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ mult{\isacharunderscore}P\ Pinc\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F\ \isakeyword{where}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}P\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymnotin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}Pinc\ A\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}insert{\isacharunderscore}last\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}P\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F{\isacharprime}\ {\isacharequal}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}Pinc\ A\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}P\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ F\ A{\isacharbrackright}\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isasymunion}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ inj{\isacharunderscore}preserved\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ P\ {\isasymequiv}\ {\isasymforall}\ A\ F\ f{\isachardot}\ {\isacharparenleft}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}\ {\isasymand}\ P\ A\ F{\isacharparenright}\ {\isasymlongrightarrow}\ P\ {\isacharparenleft}f\ {\isacharbackquote}\ A{\isacharparenright}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}incrementally{\isacharunderscore}checks\ Pinc\ P{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}preserved\ Pinc{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharunderscore}\ {\isacharquery}FFk{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ {\isachardoublequoteopen}length\ L\ {\isasymle}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}FFb{\isacharprime}\ {\isacharequal}\ mult{\isacharunderscore}all{\isacharunderscore}P\ Pinc\ FFb\ n\ {\isacharparenleft}length\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FFb{\isacharprime}\ {\isacharparenleft}L{\isacharunderscore}part{\isacharunderscore}P\ P\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharquery}FFb{\isacharprime}\ {\isacharquery}FFk{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}FFb\ {\isasymsubseteq}\ {\isacharquery}FFk{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}FFb{\isacharprime}\ {\isasymsubseteq}\ {\isacharquery}FFk{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}P{\isacharbrackleft}of\ P\ Pinc{\isacharcomma}\ OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}represents\ FFb\ {\isacharquery}FFk{\isachardoublequoteclose}\ {\isachardoublequoteopen}FFb\ {\isasymsubseteq}\ {\isacharquery}FFk{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}represents\ {\isacharquery}FFb{\isacharprime}\ {\isacharquery}FFk{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ {\isacharquery}FFk{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A\ \isakeyword{where}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ mult{\isacharunderscore}P\ Pinc\ {\isacharquery}FFk\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ L{\isacharunderscore}part{\isacharunderscore}mult{\isacharunderscore}P{\isacharbrackleft}of\ P\ Pinc\ n\ L\ k{\isacharcomma}\ OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F\ \isakeyword{where}\ {\isachardoublequoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}P\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymnotin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}Pinc\ A\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fb\ \isakeyword{where}\ {\isachardoublequoteopen}Fb\ {\isasymin}\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ F\ Fb{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso{\isacharunderscore}represents\ FFb\ {\isacharquery}FFk{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ metis\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}Fb\ {\isacharequal}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}Fb{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Fb\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}is{\isacharunderscore}L{\isacharunderscore}part\ n\ {\isacharparenleft}L\ {\isacharat}\ {\isacharbrackleft}k{\isacharbrackright}{\isacharparenright}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fb\ {\isasymin}\ FFb{\isacharbackquoteclose}\ {\isacharbackquoteopen}FFb\ {\isasymsubseteq}\ {\isacharquery}FFk{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ is{\isacharunderscore}L{\isacharunderscore}part{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast{\isacharplus}\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ f{\isacharprime}{\isachardot}\ inj{\isacharunderscore}on\ f{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}\ {\isasymand}\ f{\isacharprime}\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isasymin}{\isasymUnion}F{\isachardot}\ f\ x\ {\isacharequal}\ f{\isacharprime}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{obtain}\isamarkupfalse%
\ Bb\ \isakeyword{where}\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isacharminus}\ {\isasymUnion}\ F{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}Bb\ {\isacharminus}\ {\isasymUnion}\ Fb{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Bb\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}complement{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Fb{\isachardoublequoteclose}\ A\ f{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymUnion}\ Fb\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ \ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}Fb{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ L\ {\isasymle}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}extend{\isacharbrackleft}of\ f\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ Fb{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharminus}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}Bb\ {\isacharminus}\ {\isasymUnion}\ Fb{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ Fb{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}Bb\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymUnion}\ Fb\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset\ bij{\isacharunderscore}betw{\isacharunderscore}def{\isacharparenright}\ {\isacharparenleft}metis\ Un{\isacharunderscore}least{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f{\isacharprime}\ \isakeyword{where}\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharprime}\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ F\ {\isasymunion}\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}Fb\ {\isacharequal}\ op\ {\isacharbackquote}\ f{\isacharprime}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ {\isacharparenleft}lifting{\isacharparenright}\ image{\isacharunderscore}cong{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ Fb{\isacharprime}\ {\isasymin}\ {\isacharquery}FFb{\isacharprime}{\isachardot}\ iso\ F{\isacharprime}\ Fb{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ {\isacharparenleft}Fb\ {\isasymunion}\ {\isacharbraceleft}f{\isacharprime}\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}insert{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ f{\isacharprime}\ F\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isacharbackquoteopen}F{\isacharprime}\ {\isacharequal}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}Fb\ {\isasymunion}\ {\isacharbraceleft}f{\isacharprime}\ {\isacharbackquote}\ A{\isacharbraceright}\ {\isasymin}\ {\isacharquery}FFb{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Pinc\ {\isacharparenleft}f{\isacharprime}\ {\isacharbackquote}\ A{\isacharparenright}\ Fb{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}{\isacharasterisk}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Pinc\ A\ F{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ f{\isacharprime}\ F\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Fb\ {\isasymin}\ FFb{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharprime}\ {\isacharbackquote}\ A\ {\isasymnotin}\ Fb\ {\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ {\isacharparenleft}f{\isacharprime}\ {\isacharbackquote}\ A{\isacharparenright}\ {\isacharequal}\ length\ L{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}f{\isacharprime}\ {\isacharbackquote}\ A\ {\isasymsubseteq}\ \ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}insert{\isacharbrackleft}of\ f{\isacharprime}\ F\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ length\ L{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fb\ {\isasymin}\ FFb{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\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:
