%
\begin{isabellebody}%
\setisabellecontext{MoreFun}%
%
\isamarkupsection{Auxiliary lemmas about bijective functions%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ MoreFun\isanewline
\isakeyword{imports}\ Main\ MoreSet\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsubsection{Extending bijective functions%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}extend{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ X\ X{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{and}\ Y\ Y{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}b\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ X\ Y{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}card\ X{\isacharprime}\ {\isacharequal}\ card\ Y{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ X{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ Y{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}X\ {\isasyminter}\ X{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Y\ {\isasyminter}\ Y{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ f{\isacharprime}{\isachardot}\ bij{\isacharunderscore}betw\ f{\isacharprime}\ {\isacharparenleft}X\ {\isasymunion}\ X{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Y\ {\isasymunion}\ Y{\isacharprime}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ X{\isachardot}\ f\ x\ {\isacharequal}\ f{\isacharprime}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ fa\ \isakeyword{where}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ fa\ X{\isacharprime}\ Y{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}same{\isacharunderscore}card{\isacharunderscore}bij{\isacharbrackleft}of\ X{\isacharprime}\ Y{\isacharprime}{\isacharbrackright}\ {\isacharbackquoteopen}finite\ X{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ Y{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ X{\isacharprime}\ {\isacharequal}\ card\ Y{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}f\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ if\ x\ {\isasymin}\ X\ then\ f\ x\ else\ fa\ x{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ {\isacharquery}f\ X\ Y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ f\ X\ Y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ {\isacharquery}f\ X{\isacharprime}\ Y{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ fa\ X{\isacharprime}\ Y{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}X\ {\isasyminter}\ X{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}f{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}combine{\isacharbrackleft}of\ {\isacharquery}f\ X\ Y\ X{\isacharprime}\ Y{\isacharprime}{\isacharbrackright}\ {\isacharbackquoteopen}X\ {\isasyminter}\ X{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}Y\ {\isasyminter}\ Y{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
This should hold for every infinite type --- for our
applications, it suffices to consider only \isa{nat}.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ nat{\isacharunderscore}set{\isacharunderscore}extend{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ X{\isacharprime}{\isacharcolon}{\isacharcolon}nat\ set{\isachardot}\ finite\ X{\isacharprime}\ {\isasymand}\ card\ X{\isacharprime}\ {\isacharequal}\ n\ {\isasymand}\ X\ {\isasyminter}\ X{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}Max\ X{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}\ {\isachardot}{\isachardot}{\isacharless}\ {\isacharparenleft}Max\ X{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharplus}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isasyminter}\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymge}\ Suc\ {\isacharparenleft}Max\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymle}\ Max\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymin}\ X{\isacharbackquoteclose}\ Max{\isacharunderscore}ge{\isacharbrackleft}of\ X\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymge}\ Suc\ {\isacharparenleft}Max\ X{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymle}\ Max\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}X{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}inj{\isacharunderscore}extend{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ X{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}{\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{and}\ Y{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ X\ Y{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ Y{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ X{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ f{\isacharprime}{\isachardot}\ inj{\isacharunderscore}on\ f{\isacharprime}\ {\isacharparenleft}X\ {\isasymunion}\ X{\isacharprime}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ X{\isachardot}\ f{\isacharprime}\ x\ {\isacharequal}\ f\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}X{\isacharprime}\ {\isacharminus}\ X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ Y{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}card\ {\isacharquery}X{\isacharprime}\ {\isacharequal}\ card\ Y{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ Y{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Y\ {\isasyminter}\ Y{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isacharunderscore}set{\isacharunderscore}extend{\isacharbrackleft}of\ Y\ {\isachardoublequoteopen}card\ {\isacharquery}X{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ Y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}extend{\isacharbrackleft}of\ f\ X\ Y\ {\isacharquery}X{\isacharprime}\ Y{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}complement{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}B\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}B{\isacharprime}\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\ \isanewline
\ \ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ B\ B{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ A\ {\isasymle}\ card\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ A{\isacharprime}{\isachardot}\ card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}A{\isacharprime}\ {\isacharminus}\ B{\isacharprime}{\isacharparenright}\ {\isasymand}\ A{\isacharprime}\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ B{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ B{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}B{\isacharprime}\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ B\ {\isacharequal}\ card\ B{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ f\ B\ B{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ card{\isacharunderscore}image{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}X\ {\isacharminus}\ B{\isacharprime}{\isacharparenright}\ {\isacharequal}\ card\ X\ {\isacharminus}\ card\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ B{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}B{\isacharprime}\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Diff{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}B{\isacharprime}{\isachardoublequoteclose}\ X{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}\ {\isacharequal}\ card\ A\ {\isacharminus}\ card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Diff{\isacharunderscore}subset{\isacharunderscore}Int{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}B{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isasyminter}\ B{\isachardoublequoteclose}\ A{\isacharbrackright}\ {\isacharbackquoteopen}finite\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ B\ {\isacharminus}\ card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}B\ {\isacharminus}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Diff{\isacharunderscore}subset{\isacharunderscore}Int{\isacharbrackleft}of\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ A{\isacharbrackright}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isasyminter}\ B{\isachardoublequoteclose}\ A{\isacharbrackright}\ {\isacharbackquoteopen}finite\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Int{\isacharunderscore}commute{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ B\ {\isasymle}\ card\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ X\ {\isachardoublequoteopen}B{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}B\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymle}\ card\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}A\ {\isasyminter}\ B{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}finite\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymle}\ card\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ X\ {\isachardoublequoteopen}A\ {\isasymunion}\ B{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ B\ {\isacharminus}\ card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymle}\ card\ X\ {\isacharminus}\ card\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Un{\isacharunderscore}Int{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}B{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}card\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymle}\ card\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ B{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}F{\isacharprime}{\isasymsubseteq}X\ {\isacharminus}\ B{\isacharprime}{\isachardot}\ card\ F{\isacharprime}\ {\isacharequal}\ card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ subset{\isacharunderscore}eq{\isacharunderscore}card{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}X\ {\isacharminus}\ B{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}X\ {\isacharminus}\ B{\isacharprime}{\isachardoublequoteclose}\ X{\isacharbrackright}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}\ {\isasymle}\ card\ {\isacharparenleft}X\ {\isacharminus}\ B{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ B\ {\isacharminus}\ card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}B\ {\isacharminus}\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ {\isacharparenleft}X\ {\isacharminus}\ B{\isacharprime}{\isacharparenright}\ {\isacharequal}\ card\ X\ {\isacharminus}\ card\ B{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}\ {\isacharequal}\ card\ A\ {\isacharminus}\ card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ B\ {\isasymle}\ card\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymle}\ card\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ B\ {\isacharminus}\ card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymle}\ card\ X\ {\isacharminus}\ card\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ A\ {\isasymle}\ card\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ {\isacharparenleft}X\ {\isacharminus}\ B{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ F{\isacharprime}\ {\isacharequal}\ card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}B{\isacharprime}\ {\isasymunion}\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}B{\isacharprime}\ {\isasymunion}\ F{\isacharprime}\ {\isacharminus}\ B{\isacharprime}\ {\isacharequal}\ F{\isacharprime}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}B{\isacharprime}\ {\isasymsubseteq}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}card\ F{\isacharprime}\ {\isacharequal}\ card\ {\isacharparenleft}A\ {\isacharminus}\ B{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Bijections between the domain of a set family and natural numbers.%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}card{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ h\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ card\ {\isacharparenleft}h\ {\isacharbackquote}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}image{\isacharbrackleft}of\ h\ A{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}card{\isacharunderscore}Int{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ h\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}h\ {\isacharbackquote}\ A\ {\isasyminter}\ h\ {\isacharbackquote}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}image{\isacharunderscore}Int{\isacharbrackleft}of\ h\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ A\ B{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}image{\isacharbrackleft}of\ h\ {\isachardoublequoteopen}A\ {\isasyminter}\ B{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}card{\isacharunderscore}Un{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ h\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isasymUnion}\ A{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ h\ {\isacharbackquote}\ A{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ A{\isacharparenright}\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ h\ {\isacharbackquote}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ h\ {\isacharparenleft}{\isasymUnion}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ h\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackleft}of\ h\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}image{\isacharbrackleft}of\ h\ {\isachardoublequoteopen}{\isasymUnion}\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}card{\isacharunderscore}image{\isacharunderscore}inj{\isacharcolon}\isanewline
\isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ h\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}op\ {\isacharbackquote}\ h{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ballI{\isacharcomma}\ rule\ ballI{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isacharbackquote}\ x\ {\isacharequal}\ h\ {\isacharbackquote}\ y\ {\isasymlongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}Un{\isacharunderscore}image{\isacharunderscore}eq{\isacharunderscore}iff{\isacharbrackleft}of\ h\ x\ y{\isacharbrackright}\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Bijections betwen distinct lists' elements and natural numbers%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ swap\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}swap\ f\ a\ b\ {\isacharequal}\ f\ {\isacharparenleft}a\ {\isacharcolon}{\isacharequal}\ f\ b{\isacharcomma}\ b\ {\isacharcolon}{\isacharequal}\ f\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}swap{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ A\ B{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}a\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}b\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ {\isacharparenleft}swap\ f\ a\ b{\isacharparenright}\ A\ B{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ swap{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}f\ {\isacharequal}\ {\isachardoublequoteopen}swap\ f\ a\ b{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharquery}f\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}f\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ swap{\isacharunderscore}def\ bij{\isacharunderscore}betw{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}swap\ f\ a\ b\ {\isacharbackquote}\ A\ {\isacharequal}\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ swap{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ x\ {\isasymin}\ f{\isacharparenleft}a\ {\isacharcolon}{\isacharequal}\ f\ b{\isacharcomma}\ b\ {\isacharcolon}{\isacharequal}\ f\ a{\isacharparenright}\ {\isacharbackquote}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isacharequal}\ a{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ b{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ {\isasymin}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}a\ {\isasymnoteq}\ b{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isacharequal}\ b{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ a{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ b{\isacharbackquoteclose}\ {\isacharbackquoteopen}a\ {\isasymin}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}a\ {\isasymnoteq}\ b{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ x{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ b{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ex{\isacharunderscore}bij{\isacharunderscore}betw{\isacharunderscore}nat{\isacharunderscore}finite{\isacharunderscore}list{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}set\ l\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ b{\isachardot}\ bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ i\ {\isacharless}\ length\ l\ {\isasymlongrightarrow}\ b\ i\ {\isacharequal}\ l\ {\isacharbang}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\ \isacommand{obtain}\isamarkupfalse%
\ b\ \isakeyword{where}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ ex{\isacharunderscore}bij{\isacharunderscore}betw{\isacharunderscore}nat{\isacharunderscore}finite\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}snoc\ a\ l{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ b\ \isakeyword{where}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}i{\isacharless}length\ l{\isacharprime}{\isachardot}\ b\ i\ {\isacharequal}\ l{\isacharprime}\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ b\ {\isacharbackquote}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isacharbackquoteclose}\ snoc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ k\ \isakeyword{where}\ {\isachardoublequoteopen}k\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ k\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}n\ {\isacharequal}\ {\isachardoublequoteopen}length\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}n\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ snoc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ {\isachardoublequoteopen}l{\isacharprime}\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ X\ {\isachardoublequoteopen}set\ {\isacharparenleft}l{\isacharprime}\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharparenleft}rule\ exI{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}b\ {\isacharequal}\ {\isachardoublequoteopen}swap\ b\ k\ {\isacharquery}n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ {\isacharquery}b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ bij{\isacharunderscore}betw{\isacharunderscore}swap{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isacharquery}n\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ l{\isacharprime}\ {\isasymle}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}i{\isacharless}length\ l{\isacharprime}{\isachardot}\ b\ i\ {\isacharequal}\ l{\isacharprime}\ {\isacharbang}\ i{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ k\ {\isacharequal}\ a{\isacharbackquoteclose}\ snoc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}i{\isacharless}length\ {\isacharparenleft}l{\isacharprime}\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}{\isachardot}\ {\isacharquery}b\ i\ {\isacharequal}\ {\isacharparenleft}l{\isacharprime}\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}i{\isacharless}length\ l{\isacharprime}{\isachardot}\ b\ i\ {\isacharequal}\ l{\isacharprime}\ {\isacharbang}\ i{\isacharbackquoteclose}\ {\isacharbackquoteopen}b\ k\ {\isacharequal}\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymge}\ length\ l{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ swap{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}append{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ex{\isacharunderscore}bij{\isacharunderscore}betw{\isacharunderscore}nat{\isacharunderscore}finite{\isacharunderscore}list{\isacharunderscore}inv{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}set\ l\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ b{\isachardot}\ bij{\isacharunderscore}betw\ b\ X\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ \ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ i\ {\isacharless}\ length\ l\ {\isasymlongrightarrow}\ b\ {\isacharparenleft}l\ {\isacharbang}\ i{\isacharparenright}\ {\isacharequal}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ b\ \isakeyword{where}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}i{\isacharless}length\ l{\isachardot}\ b\ i\ {\isacharequal}\ l\ {\isacharbang}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ ex{\isacharunderscore}bij{\isacharunderscore}betw{\isacharunderscore}nat{\isacharunderscore}finite{\isacharunderscore}list{\isacharbrackleft}of\ l\ X{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}b\ {\isacharequal}\ {\isachardoublequoteopen}inv{\isacharunderscore}into\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ b{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}b{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ {\isacharquery}b\ X\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ bij{\isacharunderscore}betw{\isacharunderscore}inv{\isacharunderscore}into{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ i\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isacharless}\ length\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}l\ {\isacharbang}\ i\ {\isacharequal}\ b\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}i{\isacharless}length\ l{\isachardot}\ b\ i\ {\isacharequal}\ l\ {\isacharbang}\ i{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}i\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ l\ {\isasymle}\ card\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ l{\isacharbrackright}\ card{\isacharunderscore}mono{\isacharbrackleft}of\ X\ {\isachardoublequoteopen}set\ l{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}i\ {\isacharless}\ length\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}b\ {\isacharparenleft}l\ {\isacharbang}\ i{\isacharparenright}\ {\isacharequal}\ i{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}bij{\isacharunderscore}betw\ b\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}card\ X{\isacharbraceright}\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\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:
