\documentclass[runningheads]{llncs}
\usepackage{amssymb,url,alltt}
\usepackage[all]{xy}
\raggedbottom

\def\mizerror#1{\strut\rlap{\hspace\hsize\ \texttt{*#1}}}
\def\xverb#1{\underbar{\tt{#1}}}
\def\xsemi{\xverb{;}}

\begin{document}

\title{Ten Formal Proof Sketches}
\author{Freek Wiedijk}
\institute{Radboud University Nijmegen}
\maketitle

\begin{abstract}
This note collects the formal proof sketches that I have done.
\end{abstract}


\section{Algebra: Irrationality of $\sqrt{2}$}

\subsection{Source}

G.H.~Hardy and E.M.~Wright,
{\em An Introduction to the Theory of Numbers.}
4th edition, Clarendon Press, Oxford, 1960.
Pages 39--40.

\subsection{Informal Proof}

{\sc Theorem 43 (Pythagoras' theorem).} {\em $\sqrt{2}$ is irrational.}

\medskip\noindent
The traditional proof ascribed to Pythagoras runs
as follows.  If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{(4.3.1)}$$
is soluble in integers $a$, $b$ with $(a,b) = 1$.  Hence $a^2$ is even, and there%-
fore $a$ is even.  If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even,
contrary to the hypothesis that $(a,b) = 1$.

\subsection{Formal Proof Sketch: Informal Layout}

{\sc theorem} Th43:$\,$ {\it $\mathop{\mbox{\rm sqrt}} 2$ is irrational\/} $\,$:: {\sc Pythagoras' theorem}

\medskip\noindent
{\sc proof}$\,$ assume $\mathop{\mbox{\rm sqrt}} 2$
is rational; consider $a,b$ such that
$$\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}\leqno{\mbox{4\_3\_1:}}$$
and $a,b$ are\_relative\_prime; $a\mathbin{\hat{}}2$ is even;
$a$ is even; consider $c$ such that $a = 2\mathbin{*}c$; $4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$; $2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$; $b$ is
even; thus contradiction; $\,${\sc end};

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|theorem Th43: sqrt 2 is irrational|\\
\verb|proof|\\
\verb| assume sqrt 2 is rational;|\\
\verb| consider a,b such that|\\
\verb|4_3_1: a^2 = 2*b^2 and|\\
\mizerror{4}\verb|  a,b are_relative_prime;|\\
\mizerror{4}\verb| a^2 is even;|\\
\mizerror{4}\verb| a is even;|\\
\mizerror{4}\verb| consider c such that a = 2*c;|\\
\mizerror{4}\verb| 4*c^2 = 2*b^2;|\\
\mizerror{4}\verb| 2*c^2 = b^2;|\\
\mizerror{4}\verb| b is even;|\\
\mizerror{1}\verb| thus contradiction;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{theorem Th43: sqrt 2 is irrational}\\
\xverb{proof}\\
\verb| |\xverb{assume sqrt 2 is rational;}\\
\verb| then |\xverb{consider a,b such that}\\
\verb|A1: b <> 0 and|\\
\verb|A2: sqrt 2 = a/b and|\\
\verb|A3: |\xverb{a,b are\char`_relative\char`_prime}\verb| by Def1;|\\
\verb|A4: b^2 <> 0 by A1,SQUARE_1:73;|\\
\verb| 2 = (a/b)^2 by A2,SQUARE_1:def 4|\\
\verb|  .= a^2/b^2 by SQUARE_1:69;|\\
\verb| then|\\
\xverb{4\char`_3\char`_1: a\^{}2 = 2*b\^{}2}\verb| by A4,REAL_1:43|\xsemi\\
\verb| |\xverb{a\^{}2 is even}\verb| by 4_3_1,ABIAN:def 1|\xsemi\\
\verb| then|\\
\verb|A5: |\xverb{a is even}\verb| by PYTHTRIP:2|\xsemi\\
\verb| then |\xverb{consider c such that}\\
\verb|A6: |\xverb{a = 2*c}\verb| by ABIAN:def 1|\xsemi\\
\verb|A7: |\xverb{4*c\^{}2 =}\verb| (2*2)*c^2|\\
\verb|  .= 2^2*c^2 by SQUARE_1:def 3|\\
\verb|  .= |\xverb{2*b\^{}2}\verb| by A6,4_3_1,SQUARE_1:68|\xsemi\\
\verb| 2*(2*c^2) = (2*2)*c^2 by AXIOMS:16|\\
\verb|  .= 2*b^2 by A7;|\\
\verb| then |\xverb{2*c\^{}2 = b\^{}2}\verb| by REAL_1:9|\xsemi\\
\verb| then b^2 is even by ABIAN:def 1;|\\
\verb| then |\xverb{b is even}\verb| by PYTHTRIP:2|\xsemi\\
\verb| then 2 divides a & 2 divides b by A5,Def2;|\\
\verb| then|\\
\verb|A8: 2 divides a gcd b by INT_2:33;|\\
\verb| a gcd b = 1 by A3,INT_2:def 4;|\\
\verb| |\xverb{hence contradiction}\verb| by A8,INT_2:17|\xsemi\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.1.11 -- 3.33.722


\section{Algebra: Infinity of Primes}

\subsection{Source}

The slides of a talk by Herman Geuvers,
{\em Formalizing an intuitionistic proof of the Fundamental
Theorem of Algebra.}

\subsection{Informal Proof}

{\sc Theorem}$\,$ There are infinitely many primes:\\
for every number $n$ there exists a prime $p> n$ \medskip

\medskip\noindent
\textsc{Proof} [after Euclid]\\
Given $n$. Consider $k=n!+1$, where $n!=1\cdot 2\cdot 3\cdot \ldots\cdot n$.\\
Let $p$ be a prime that divides $k$.\\
For this number $p$ we have $p> n$: otherwise $p\leq n$;\\
but then $p$ divides $n!$,\\
so $p$ cannot divide $k=n!+1$,\\
contradicting the choice of $p$. QED

\subsection{Formal Proof Sketch: Informal Layout}

{\sc theorem}$\,$ $\{n: n\mbox{\rm\ is prime}\}$ is infinite $\,${\sc proof}\\
for $n$ ex $p$ st $p$ is prime \& $p > n$

\medskip\noindent
{\sc proof} :: [after Euclid]\\
let $n$; set $k = n! + 1$;\\
consider $p$ such that $p$ is prime \& $p$ divides $k$;\\
take $p$; thus $p$ is prime; thus $p > n$ $\,${\sc proof}$\,$ assume $p <= n$;\\
$p$ divides $n!$;\\
not $p$ divides $n! + 1$;\\
thus contradiction; $\,${\sc end; end;} thus thesis; {\sc end;}

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|theorem {n: n is prime} is infinite|\\
\verb|proof|\\
\verb| for n ex p st p is prime & p > n|\\
\verb| proof|\\
\verb|  let n;|\\
\verb|  set k = n! + 1;|\\
\mizerror{4}\verb|  consider p such that p is prime & p divides k;|\\
\verb|  take p;|\\
\mizerror{4}\verb|  thus p is prime;|\\
\verb|  thus p > n|\\
\verb|  proof|\\
\verb|   assume p <= n;|\\
\mizerror{4}\verb|   p divides n!;|\\
\mizerror{4}\verb|   not p divides n! + 1;|\\
\mizerror{1}\verb|   thus contradiction;|\\
\verb|  end;|\\
\verb| end;|\\
\mizerror{4}\verb| thus thesis;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{theorem {\char`\{}p: p is prime{\char`\}} is infinite}\\
\xverb{proof}\\
\verb|A1: |\xverb{for n ex p st p is prime \& p > n}\\
\verb| |\xverb{proof}\\
\verb|  |\xverb{let n;}\\
\verb|  |\xverb{set k = n! + 1;}\\
\verb|  n! > 0 by NEWTON:23;|\\
\verb|  then n! >= 0 + 1 by NAT_1:38;|\\
\verb|  then k >= 1 + 1 by REAL_1:55;|\\
\verb|  then |\xverb{consider p such that}\\
\verb|A2: |\xverb{p is prime \& p divides k}\verb| by INT_2:48|\xsemi\\
\verb|  |\xverb{take p;}\\
\verb|  |\xverb{thus p is prime}\verb| by A2|\xsemi\\
\verb|  |\xverb{assume}\\
\verb|A3: |\xverb{p <= n;}\\
\verb|  p <> 0 by A2,INT_2:def 5;|\\
\verb|  then|\\
\verb|A4: |\xverb{p divides n!}\verb| by A3,NAT_LAT:16|\xsemi\\
\verb|  p > 1 by A2,INT_2:def 5;|\\
\verb|  then not p divides 1 by NAT_1:54;|\\
\verb|  |\xverb{hence contradiction}\verb| by A2,A4,NAT_1:57|\xsemi\\
\verb| |\xverb{end;}\\
\verb| |\xverb{thus thesis}\verb| from Unbounded(A1)|\xsemi\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.1.11 -- 3.33.722


\section{Algebra: Image of Left Unit Element}

\subsection{Source}

Rob Nederpelt, {\em Weak Type Theory: A formal language for mathematics.}
Computer Science Report 02-05, Eindhoven University of Technology,
Department of Math.~and Comp.~Sc., May 2002.
Page 42.

\subsection{Informal Proof}

{\sc Theorem.}  Let $G$ be a set with a binary operation $\cdot$ and left unit element
$e$.  Let $H$ be a set with binary operation $*$ and assume that $\phi$ is a homo%-
morphism of $G$ onto $H$.  Then $H$ has a left unit element as well.

\medskip\noindent
{\sc Proof.}  Take $e' = \phi(e)$.  Let $h\in H$.  There is $g\in G$ such that $\phi(g) = h$.
Then $$e' * h = \phi(e) * \phi(g) = \phi(e\cdot g) = \phi(g) = h,$$
hence $e'$ is left unit element of $H$.\hfill$\Box$

\subsection{Formal Proof Sketch: Informal Layout}

\quad
 let $G,H$ be non empty HGrStr;
 let $e$ be Element of $G$ such that $e$ is\_left\_unit\_of $G$;
 let {\it phi\/} be map of $G,H$ such that
  {\it phi\/} is\_homomorphism $G,H$ and {\it phi\/} is onto;
 thus ex $e'$ being Element of $H$ st $e'$ is\_left\_unit\_of $H$\medskip\\
{\sc proof}$\,$
 take $e' = \mbox{\it phi\/}.e$;
 now
  let $h$ be Element of $H$;
  consider $g$ being Element of $G$ such that $\mbox{\it phi\/}.g = h$;
  thus
$$\mbox{$e' * h = \mbox{\it phi\/}.e * \mbox{\it phi\/}.g \mathrel{\mbox{.=}} \mbox{\it phi\/}.(e * g) \mathrel{\mbox{.=}} \mbox{\it phi\/}.g \mathrel{\mbox{.=}} h$;}$$
 end;
 hence $e'$ is\_left\_unit\_of $H$;
\hfill {\sc end;}

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb| let G,H be non empty HGrStr;|\\
\verb| let e be Element of G such that e is_left_unit_of G;|\\
\verb| let phi be map of G,H such that|\\
\verb|  phi is_homomorphism G,H and phi is onto;|\\
\verb| thus ex e' being Element of H st e' is_left_unit_of H|\\
\verb|proof|\\
\verb| take e' = phi.e;|\\
\verb| now|\\
\verb|  let h be Element of H;|\\
\mizerror{4}\verb|  consider g being Element of G such that phi.g = h;|\\
\mizerror{4$\;$*4$\;$*4$\;$*4}\verb|  thus e' * h = phi.e * phi.g .= phi.(e * g) .= phi.g .= h;|\\
\verb| end;|\\
\mizerror{4}\verb| hence e' is_left_unit_of H;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\verb| |\xverb{let G,H be non empty HGrStr;}\\
\verb| |\xverb{let e be Element of G such that}\\
\verb|H1: |\xverb{e is\char`_left\char`_unit\char`_of G;}\\
\verb| |\xverb{let phi be map of G,H such that}\\
\verb|H2: |\xverb{phi is\char`_homomorphism G,H and}\\
\verb|H3: |\xverb{phi is onto;}\\
\verb| |\xverb{thus ex e' being Element of H st e' is\char`_left\char`_unit\char`_of H}\\
\xverb{proof}\\
\verb| |\xverb{take e' = phi.e;}\\
\verb| |\xverb{now}\\
\verb|  |\xverb{let h be Element of H;}\\
\verb|  |\xverb{consider g being Element of G such that}\\
\verb|A1: |\xverb{phi.g = h}\verb| by H3,Th1|\xverb{;}\\
\verb|  |\xverb{thus e' * h = phi.(e * g)}\verb| by A1,H2,Def2|\\
\verb|   |\xverb{.= h}\verb| by A1,H1,Def1|\xverb{;}\\
\verb| |\xverb{end;}\\
\verb| |\xverb{hence e' is\char`_left\char`_unit\char`_of H}\verb| by Def1|\xverb{;}\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.1.11 -- 3.33.722


\section{Algebra: Lagrange's Theorem}

\subsection{Source}

B.L. van der Waerden, \emph{Algebra}. 5th edition, Springer-Verlag, Berlin, 1966.
Page 26.

\subsection{Informal Proof}

\strut\hspace{\parindent}%
Zwei Nebenklassen $a\mathfrak{g}$, $b\mathfrak{g}$ k\"onnen sehr wohl gleich sein, ohne da{\ss}
$a = b$ ist.  Immer dann n\"amlich, wenn $a^{-1}b$ in $\mathfrak{g}$ liegt, gilt
$$b\mathfrak{g} = aa^{-1}b\mathfrak{g} = a(a^{-1}b\mathfrak{g}) = a\mathfrak{g}.$$

Zwei {\it verschiedene} Nebenklassen haben kein Element gemeinsam.
Denn wenn die Nebenklassen $a\mathfrak{g}$ und $b\mathfrak{g}$ ein Element gemein haben, etwa
$$ag_1 = bg_2,$$
so folgt
$$g_1g_2^{-1} = a^{-1}b.$$
so da{\ss} $a^{-1}b$ in $\mathfrak{g}$ liegt; nach dem Vorigen sind also $a\mathfrak{g}$ und $b\mathfrak{g}$ identisch.

Jedes Element $a$ geh\"ort einer Nebenklasse an, n\"amlich der Neben\-%
klasse $a\mathfrak{g}$.  Diese enth\"alt ja sicher das Element $ae = a$.  Nach dem eben
Bewiesenen geh\"ort das Element $a$ auch {\it nur} einer Nebenklasse an.  Wir
k\"onnen demnach jedes Element $a$ als {\it Repr\"asentanten} der $a$ enthaltenden
Nebenklass $a\mathfrak{g}$ ansehen.

Nach dem vorhergehenden bilden die Nebenklassen eine {\it Klassen\-%
einteilung} der Gruppe $\mathfrak{G}$.  Jedes Element geh\"ort einer und nur einer
Klasse an.

Je zwei Nebenklassen sind gleichm\"achtig.  Denn durch $a\mathfrak{g} \to b\mathfrak{g}$ ist
eine eineindeutige Abbildung von $a\mathfrak{g}$ auf $b\mathfrak{g}$ definiert.

Die Nebenklassen sind, mit Ausnahme von $\mathfrak{g}$ selbst, {\it keine} Gruppen;
denn eine Gruppe m\"u{\ss}te das Einselelement enthalten.

Die Anzahl der verschiedenen Nebenklassen einer Untergruppe $\mathfrak{g}$
in $\mathfrak{G}$ hei{\ss}t der {\it Index} von $\mathfrak{g}$ in $\mathfrak{G}$.  Der Index kann endlich oder un\-%
endlich sein.

Ist $N$ die als (endlich angenommene) Ordnung von $\mathfrak{G}$, $n$ die von $\mathfrak{g}$,
$j$~der Index, so gilt die Relation
$$N = jn;\leqno{(2)}$$
denn $\mathfrak{G}$ ist ja in $j$ Klassen eingeteilt, deren jede $n$ Elemente enth\"alt.

Man kann f\"ur endliche Gruppen aus (2) den Index $j$ berechnen:
$$j = {N\over n}$$

Folge.  {\it Die Ordnung einer Untergruppe einer endlichen Gruppe ist
ein Teiler der Ordnung der Gesamtgruppe.}

\subsection{Formal Proof Sketch: Informal Layout}

\strut\hspace{\parindent}%
now let a,b; assume $a\mbox{\char`\^$^{-1}$}*b$ in $G$; thus
$$b*G = a*a\mbox{\char`\^$^{-1}$}*b*G .= a*(a\mbox{\char`\^$^{-1}$}*b*G) .= a*G; \eqno{\mbox{\it end;}}$$

for $a,b$ st $a*G <> b*G$ holds $(a*G) \mathbin{/\backslash} (b*G) = \{\}$

\noindent
proof
let a,b;
now
assume $(a*G) \mathbin{/\backslash} (b*G) <> \{\}$;
consider $g_1,g_2$ such that
$$a*g_1 = b*g_2\mbox{;}$$
$$g_1*g_2\mbox{\char`\^$^{-1}$} = a\mbox{\char`\^$^{-1}$}*b;\smallskip$$
$a\mbox{\char`\^$^{-1}$}*b$ in $G$;
thus $a*G = b*G$;
end;
thus thesis;
end;

for $a$ holds $a$ in $a*G$
proof
let $a$;
$a*e(G) = a$;
thus thesis;
end;

$\{a*G : a\mbox{ in }H\}\mbox{ is a\char`\_partition of }H$;

for $a,b$ holds $\mbox{card}(a*G) = \mbox{card}(b*G)$
proof
let $a,b$;
consider $f$ being Function of $a*G,b*G$ such that
for $g$ holds $f.(a*g) = b*g$;
$f$ is bijective;
thus thesis;
end;

set $\mbox{'Index'} = \mbox{card} \{a*G : a\mbox{ in }H\}$;

now
let $N$ such that $N = \mbox{card }H$;
let $n$ such that $n = \mbox{card }G$;
let $j$ such that $j = \mbox{'Index'}$;
thus
\begin{center}
'2':\hfill $N = j*n$;\hfill{\it end;}
\end{center}

thus {\it card $G$ divides card $H$};

\subsection{Formal Proof Sketch: Formal Layout}

\begingroup
\def\\{\char`\\}
\def\{{\char`\{}
\def\}{\char`\}}
\let\semi=\;
\def\;{$\semi$}
\begin{alltt}\footnotesize
now
 let a,b;
 assume a^-1*b in G;
\mizerror{4\;*4\;*4} thus b*G = a*a^-1*b*G .= a*(a^-1*b*G) .= a*G;
end;
for a,b st a*G <> b*G holds (a*G) /\\ (b*G) = \{\}
proof
 let a,b;
 now
  assume (a*G) /\\ (b*G) <> \{\};
\mizerror{4}  consider g1,g2 such that a*g1 = b*g2;
\mizerror{4}  g1*g2^-1 = a^-1*b;
\mizerror{4}  a^-1*b in G;
\mizerror{4}  thus a*G = b*G;
 end;
\mizerror{4} thus thesis;
end;
for a holds a in a*G
proof
 let a;
\mizerror{4} a*e(G) = a;
\mizerror{4} thus thesis;
end;
\mizerror{4}\{a*G : a in H\} is a_partition of H;
for a,b holds card(a*G) = card(b*G)
proof
 let a,b;
 consider f being Function of a*G,b*G such that
\mizerror{4}  for g holds f.(a*g) = b*g;
\mizerror{4} f is bijective;
\mizerror{4} thus thesis;
end;
set 'Index' = card \{a*G : a in H\};
now
 let N such that N = card H;
 let n such that n = card G;
 let j such that j = 'Index';
 thus
\mizerror{4}'2': N = j*n;
end;
\mizerror{4}thus card G divides card H;
\end{alltt}
\endgroup

\subsection{Formal Proof}

\begingroup
\def\\{\char`\\}
\def\{{\char`\{}
\def\}{\char`\}}
\def\'{\char`\'}
\def\x#1{\underbar{#1}}
\begin{alltt}\footnotesize
A1: \x{now}
 \x{let a,b;}
 \x{assume}
A2: \x{a^-1*b in G;}
 \x{thus b*G =} e(H)*b*G by GROUP_1:def 5
  .= \x{a*a^-1*b*G} by GROUP_1:def 6
  .= a*(a^-1*b)*G by GROUP_1:def 4
  \x{.= a*(a^-1*b*G)} by GROUP_2:127
  .= a*(carr G) by A2,GROUP_2:136
  \x{.= a*G} by GROUP_2:def 13\x{;}
\x{end;}
A3: \x{for a,b st a*G <> b*G holds (a*G) /\\ (b*G) = \{\}}
\x{proof}
 \x{let a,b;}
 \x{now}
  \x{assume (a*G) /\\ (b*G) <> \{\};}
  then consider x such that
A4: x in (a*G) /\\ (b*G) by XBOOLE_0:7;
A5: x in a*G & x in b*G by A4,XBOOLE_0:def 4;
  \x{consider g1} such that
A6: x = a*g1 by A5,Th5;
  consider \x{g2 such that}
A7: x = b*g2 by A5,Th5;
  set g1G = g1;
  set g2G = g2;
  reconsider g1 as Element of H by GROUP_2:51;
  reconsider g2 as Element of H by GROUP_2:51;
A8: \x{a*g1 =} a*g1G by Th2
   .= \x{b*g2} by A6,A7,Th2\x{;}
  g1G*g2G^-1 = g1*g2G^-1 by Th3
   .= \x{g1*g2^-1} by Th2,GROUP_2:57
   .= e(H)*g1*g2^-1 by GROUP_1:def 5
   .= a^-1*a*g1*g2^-1 by GROUP_1:def 6
   .= a^-1*(a*g1)*g2^-1 by GROUP_1:def 4
   .= a^-1*(b*g2*g2^-1) by A8,GROUP_1:def 4
   .= a^-1*(b*(g2*g2^-1)) by GROUP_1:def 4
   .= a^-1*(b*e(H)) by GROUP_1:def 6
   .\x{= a^-1*b} by GROUP_1:def 5\x{;}
  then \x{a^-1*b in G} by STRUCT_0:def 5\x{;}
  \x{hence a*G = b*G} by A1\x{;}
 \x{end;}
 \x{hence thesis;}
\x{end;}
A9: \x{for a holds a in a*G}
\x{proof}
 \x{let a;}
 \x{a*e(G) =} a*e(H) by Th2,GROUP_2:53
  .= \x{a} by GROUP_1:def 5\x{;}
 \x{hence thesis;}
\x{end;}
set X = \{a*G : a in H\};
X c= bool the carrier of H
proof
 let A;
 assume A in X;
 then consider a such that
A10: A = a*G & a in H;
 thus A in bool the carrier of H by A10,ZFMISC_1:def 1;
end;
then reconsider X as Subset-Family of H;
A11: X is a_partition of the carrier of H
proof
 thus union X = the carrier of H
 proof
  thus union X c= the carrier of H;
  let x;
  assume
A12: x in the carrier of H;
  then reconsider a = x as Element of H;
  x in H by A12,STRUCT_0:def 5;
  then a in a*G & a*G in X by A9;
  hence x in union X by TARSKI:def 4;
 end;
 let A be Subset of the carrier of H;
 assume A in X;
 then consider a such that
A13: A = a*G & a in H;
 thus A <> \{\} by A13;
 let B be Subset of the carrier of H;
 assume B in X;
 then consider b such that
A14: B = b*G & b in H;
 assume A <> B;
 then A /\\ B = \{\} by A3,A13,A14;
 hence A misses B by XBOOLE_0:def 7;
end;
then reconsider X as a_partition of H;
\x{\{a*G : a in H\} is a_partition of H} by A11\x{;}
A15: \x{for a,b holds card(a*G) = card(b*G)}
\x{proof}
 \x{let a,b;}
 defpred P[Element of a*G,Element of b*G] means
  for g st $1 = a*g holds $2 = b*g;
A16: now
  let x be Element of a*G;
  consider g such that
A17: x = a*g by Th5;
  reconsider y = b*g as Element of b*G;
  take y;
  thus P[x,y] by A17,Th4;
 end;
 \x{consider f being Function of a*G,b*G such that}
A18: for x being Element of a*G holds P[x,f.x qua Element of b*G]
   from FUNCT_2:sch 3(A16);
 \x{for g holds f.(a*g) = b*g} by A18\x{;}
 \x{f is bijective}
 proof
  hereby
   let x,x' be Element of a*G;
   consider g such that
A19: x = a*g by Th5;
   consider g' such that
A20: x' = a*g' by Th5;
A21: f.x = b*g & f.x' = b*g' by A19,A20,A18;
   assume f.x = f.x';
   hence x = x' by A19,A20,A21,Th4;
  end;
  let y be Element of b*G;
  consider g such that
A22: y = b*g by Th5;
  take a*g;
  thus thesis by A18,A22;
 end\x{;}
 \x{hence thesis} by EUCLID_7:3\x{;}
\x{end;}
\x{set \'Index\' = card \{a*G : a in H\};}
'Index' = card X;
then reconsider 'Index' as natural number;
\x{now}
 \x{let N such that}
A23: \x{N = card H;}
 \x{let n such that}
A24: \x{n = card G;}
 \x{let j such that}
A25: \x{j = \'Index\';}
A26: card H = card the carrier of H by STRUCT_0:def 17;
 now
  let A;
  assume A in X;
  then consider a such that
A27: A = a*G & a in H;
  e(H)*G = carr(G) by GROUP_2:132
   .= the carrier of G by GROUP_2:def 9;
  then card(e(H)*G) = card G by STRUCT_0:def 17;
  hence card A = n by A15,A24,A27;
 end;
 \x{hence N = j*n} by A23,A25,A26,Th1\x{;}
\x{end;}
then card H = 'Index'*card G;
\x{hence card G divides card H} by INT_1:def 9\x{;}
\end{alltt}
\endgroup

\subsection{Mizar Version}

7.11.01 -- 4.117.1046


\section{Analysis: successor has no fixed point}

\subsection{Source}

Fairouz Kamareddine, Manuel Maarek and J.B.~Wells, {\em MathLang: experience-driven development of a new mathematical language,} draft.
Page 11.

Quoted from: Edmund Landau, {\em Foundations of Analysis.}
Translated by F. Steinhardt,
Chelsea, 1951.

\subsection{Informal Proof}

\textbf{Theorem 2}
$$x' \ne x$$

\medskip\noindent
\textbf{Proof} \ Let $\mathfrak{M}$ be the set of all $x$ for which
this holds true.
\begin{enumerate}
\item[I)] By Axiom 1 and Axiom 3,
$$1' \ne 1;$$
therefore 1 belongs to $\mathfrak{M}$.

\medskip
\item[II)] If $x$ belongs to $\mathfrak{M}$, then
$$x' \ne x,$$
and hence by Theorem 1,
$$(x')' \ne x',$$
so that $x'$ belongs to $\mathfrak{M}$.

\end{enumerate}
By Axiom 5, $\mathfrak{M}$ therefore contains all the
natural numbers, i.e.~we have for each $x$
that
$$x' \ne x.$$

\subsection{Formal Proof Sketch: Informal Layout}

\textbf{Theorem}\_2: $$x\;' \mathrel{<>} x$$

\medskip\noindent
\textbf{proof}
\ set $\mathfrak{M} = \{y : y\;' \mathrel{<>} y\}$;
\begin{enumerate}
\item[I:] now
  $$1\;' \mathrel{<>} 1$$ by Axiom\_1, Axiom\_3;
  hence $1$ in $\mathfrak{M}$;
 \hfill\emph{end;}

\medskip
\item[II:] now let $x$;
  assume $x$ in $\mathfrak{M}$;
  then $$x\;' \mathrel{<>} x;$$
  then $$(x\;')' \mathrel{<>} x\;'$$ by Theorem\_1;
  hence $x\;'$ in $\mathfrak{M}$;
 \hfill\emph{end;}

\end{enumerate}
 for $x$ holds $x$ in $\mathfrak{M}$ by Axiom\_5;
 hence $$x\;' \mathrel{<>} x;
\eqno{\mbox{\emph{end;}}}$$

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|Theorem_2: x ' <> x|\\
\verb|proof|\\
\verb| set M = {y : y ' <> y};|\\
\verb|I: now|\\
\verb|  1 ' <> 1 by Axiom_1, Axiom_3;|\\
\mizerror{4}\verb|  hence 1 in M;|\\
\verb| end;|\\
\verb|II: now let x;|\\
\verb|  assume x in M;|\\
\mizerror{4}\verb|  then x ' <> x;|\\
\verb|  then (x ')' <> x ' by Theorem_1;|\\
\verb|  hence x ' in M;|\\
\verb| end;|\\
\mizerror{4}\verb| for x holds x in M by Axiom_5;|\\
\mizerror{4}\verb| hence x ' <> x;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{Theorem\char`\_2: x ' <> x}\\
\xverb{proof}\\
\verb| |\xverb{set M = \char`\{y : y ' <> y\char`\};}\\
\xverb{I: now}\\
\verb|  |\xverb{1 ' <> 1 by Axiom\char`\_3;}\\
\verb|  |\xverb{hence 1 in M by Axiom\char`\_1;}\\
\verb| |\xverb{end;}\\
\verb| |\xverb{now let x;}\\
\verb|  |\xverb{assume x in M;}\\
\verb|  |\xverb{then}\verb| ex y st x = y & |\xverb{y ' <> y;}\\
\verb|  |\xverb{then (x ')' <> x '}\verb| by Axiom_4|\xsemi\\
\verb|  |\xverb{hence x ' in M;}\\
\verb| |\xverb{end;}\\
\verb| then |\xverb{x in M by }\verb|I,|\xverb{Axiom\char`\_5;}\\
\verb| then ex y st x = y & y ' <> y;|\\
\verb| |\xverb{hence x ' <> x;}\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.4.01 -- 3.60.795


\section{Analysis: successor has no fixed point}

\subsection{Source}

A message \emph{Formal verification} on the FOM mailing list by Lasse Rempe-Gillen
$\langle$\verb|L.Rempe@liverpool|\penalty100\verb|.ac.uk|$\rangle$,
dated 21 October 2014 and with Message-ID\break
$\langle${\verb|675123965B518F43B235C5FCB5D565DCBF14577E@CHEXMBX1.livad.liv.ac.uk|}$\rangle$.$\hspace{-1cm}$

\subsection{Informal Proof}

\emph{Let $f$ be a real-valued function on the real line, such that $f(x)>x$ for all $x$.
Let $x_0$ be a real number, and define the sequence $(x_n)$ recursively by $x_{n+1}
:= f(x_n)$. Then $x_n$ diverges to infinity.}

\medskip\noindent
A standard proof might go along the following steps: 1) By assumption, the
sequence is strictly increasing; 2) hence the sequence either diverges to
infinity or has a finite limit; 3) by continuity, any finite limit would have
to be a fixed point of $f$, hence the latter cannot occur.

\subsection{Formal Proof Sketch: Informal Layout}

\emph{now let $f$ be continuous Function of {\small REAL},{\small REAL}; assume for $x$ holds $f.(x) > x$;
let $x_0$ be Element of {\small REAL}; set $x$ = \emph{recursively\_iterate}($f$,$x_0$); $x_{.(n + 1)} = f.(x_{.n})$;
thus $x$ is divergent\_to+infty}

\medskip\noindent
proof$\enskip$ $x$ is increasing; $x$ is divergent\_to+infty or $x$ is convergent;
$x$ is convergent implies $f.(\lim x) = \lim x$; $x$ is not convergent;
$\enskip$thus thesis; end; \emph{end;}

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|now     |\\
\verb|  let f be continuous Function of REAL,REAL;|\\
\verb|  assume for x holds f.(x) > x;|\\
\verb|  let x0 be Element of REAL; |\\
\verb|  set x = recursively_iterate(f,x0);|\\
\mizerror{4}\verb|  x.(n + 1) = f.(x.n);|\\
\verb|  thus x is divergent_to+infty|\\
\verb|  proof|\\
\mizerror{4}\verb|    x is increasing;|\\
\mizerror{4}\verb|    x is divergent_to+infty or x is convergent;|\\
\mizerror{4}\verb|    x is convergent implies f.(lim x) = lim x;|\\
\mizerror{4}\verb|    x is not convergent;|\\
\mizerror{4}\verb|    thus thesis;|\\
\verb|  end;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{now}\\
\verb|  |\xverb{let f be continuous Function of REAL,REAL;}\\
\verb|  |\xverb{assume}\\
\verb|A1: |\xverb{for x holds f.(x) > x;}\\
\verb|  |\xverb{let x0 be Element of REAL;}\\
\verb|  |\xverb{set x = recursively\char`\_iterate(f,x0);}\\
\verb|A2: |\xverb{x.(n + 1) = f.(x.n)}\verb| by Def1|\xverb{;}\\
\verb|  |\xverb{thus x is divergent\char`\_to+infty}\\
\verb|  |\xverb{proof}\\
\verb|    now let n;|\\
\verb|      x.(n + 1) = f.(x.n) by A2;|\\
\verb|      hence x.(n + 1) > x.n by A1;|\\
\verb|    end;|\\
\verb|    then|\\
\verb|A3:   |\xverb{x is increasing}\verb| by SEQM_3:def 6|\xverb{;}\\
\verb|    then x is bounded_above implies x is convergent;|\\
\verb|    then|\\
\verb|A4:   |\xverb{x is divergent\char`\_to+infty or x is convergent}\verb| by A3,LIMFUNC1:31|\xverb{;}\\
\verb|    |\xverb{x is convergent implies f.(lim x) = lim x}\\
\verb|    proof|\\
\verb|      assume|\\
\verb|A5:     x is convergent;|\\
\verb|A6:   dom f = REAL by PARTFUN1:def 2;|\\
\verb|A7:   rng x c= dom f by A6,RELAT_1:def 19;|\\
\verb|A8:   now let n;|\\
\verb|        reconsider m = n as Element of NAT by ORDINAL1:def 12;|\\
\verb|        x.(m + 1) = f.(x.m) by A2|\\
\verb|          .= (f /* x).m by A7,FUNCT_2:108;|\\
\verb|        hence x.(n + 1) = (f /* x).n;|\\
\verb|      end;|\\
\verb|      f is_continuous_in lim x by A6,XREAL_0:def 1,FCONT_1:def 2;|\\
\verb|      hence f.(lim x) = lim (f /* x) by A5,A7,FCONT_1:def 1|\\
\verb|        .= lim (x ^\ 1) by A8,NAT_1:def 3|\\
\verb|        .= lim x by A5,SEQ_4:22;|\\
\verb|    end|\xverb{;}\\
\verb|    then |\xverb{x is not convergent}\verb| by A1|\xverb{;}\\
\verb|    |\xverb{hence thesis}\verb| by A4|\xverb{;}\\
\verb|  |\xverb{end;}\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

8.1.02 -- 5.22.1191 


\section{Linear Algebra: Linear Independence}

\subsection{Source}

Jean Gallier, {\em Basics of Algebra and Analysis For Computer Science.}
Published at \url{<http://www.cis.upenn.edu/~jean/gbook.html>},
University of Pennsylvania, 2001.
Page 16.

\subsection{Informal Proof}

{\bf Lemma 2.1.}
{\em
Given a linearly independent family $(u_i)_{i\in I}$ of elements of a vector space $E$, if
$v\in E$ is not a linear combination of $(u_i)_{i\in I}$, then the family $(u_i)_{i\in I}\cup_k (v)$ obtained by adding
$v$ to the family $(u_i)_{i\in I}$ is linearly independent (where $k\not\in I$).}

\medskip\noindent
{\em Proof.}
Assume that $\mu v + \sum_{i\in I} \lambda_i u_i = 0$, for any family $(\lambda_i)_{i\in I}$ of scalars in $K$.  If $\mu\ne 0$,
then $\mu$ has an inverse (because $K$ is a field), and thus we have $v = -\sum_{i\in I} (\mu^{-1}\lambda_i) u_i$, showing
that $v$ is a linear combination of $(u_i)_{i\in I}$ and contradicting the hypothesis.  Thus, $\mu = 0$.  But
then, we have $\sum_{i\in I} \lambda_i u_i = 0$, and since the family $(u_i)_{i\in I}$ is linearly independent, we have
$\lambda_i = 0$ for all $i\in I$.
$\hfill\Box$

\subsection{Formal Proof Sketch: Informal Layout}

{\bf theorem Lem21:}
{\em $u$ is linearly-independent\/} \& {\em not $v$ in $\mbox{\rm Lin}(u)$ implies
$u \mathbin{\backslash/} \{v\}$ is linearly-independent}

\medskip\noindent
{\em proof\/}
assume $u$ is linearly-independent \& not $v$ in $\mbox{\rm Lin}(u)$;
assume $u \mathbin{\backslash/} \{v\}$ is linearly-dependent;
consider $m$ being Element of $K$,
$l$ being Linear\_Combination of $u$ such that
$m*v + \mbox{\rm Sum}(l) = 0.E$;
now
assume $m \mathrel{<>} 0.K$;
$v = -m"*\mbox{\rm Sum}(l)$;
$v$ in $\mbox{\rm Lin}(u)$;
thus contradiction;
end;
$m = 0.K$;
$\mbox{\rm Sum}(l) = 0.E$;
$\mbox{\rm Carrier}(l) = \{\}$;
thus contradiction;
{\em end;}

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|theorem Lem21:|\\
\verb| u is linearly-independent & not v in Lin(u) implies|\\
\verb|  u \/ {v} is linearly-independent|\\
\verb|proof|\\
\verb| assume u is linearly-independent & not v in Lin(u);|\\
\verb| assume u \/ {v} is linearly-dependent;|\\
\verb| consider m being Element of K,|\\
\verb|  l being Linear_Combination of u such that|\\
\mizerror{4}\verb|   m*v + Sum(l) = 0.E;|\\
\verb| now|\\
\verb|  assume m <> 0.K;|\\
\mizerror{4}\verb|  v = -m"*Sum(l);|\\
\mizerror{4}\verb|  v in Lin(u);|\\
\mizerror{1}\verb|  thus contradiction;|\\
\verb| end;|\\
\mizerror{4}\verb| m = 0.K;|\\
\mizerror{4}\verb| Sum(l) = 0.E;|\\
\mizerror{4}\verb| Carrier(l) = {};|\\
\mizerror{1}\verb| thus contradiction;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{theorem Lem21:}\\
\verb| |\xverb{u is linearly-independent \& not v in Lin(u) implies}\\
\verb|  |\xverb{u \char`\\/ {\char`\{}v{\char`\}} is linearly-independent}\\
\xverb{proof}\\
\verb| |\xverb{assume}\\
\verb|A1: |\xverb{u is linearly-independent \& not v in Lin(u);}\\
\verb| given l' being Linear_Combination of u \/ {v} such that|\\
\verb|A2: Sum(l') = 0.E & Carrier(l') <> {};|\\
\verb| |\xverb{consider}\verb| m' being Linear_Combination of {v},|\\
\verb|  |\xverb{l being Linear\char`_Combination of u such that}\\
\verb|A3: l' = m' + l by Th2;|\\
\verb| set m = m'.v;|\\
\verb|A4: |\xverb{m*v + Sum(l) =}\verb| Sum(m') + Sum(l) by VECTSP_6:43|\\
\verb|  .= |\xverb{0.E}\verb| by A2,A3,VECTSP_6:77|\xsemi\\
\verb|A5: |\xverb{now}\\
\verb|  |\xverb{assume}\\
\verb|A6: |\xverb{m <> 0.K;}\\
\verb|  m*v = -Sum(l) by A4,RLVECT_1:def 10;|\\
\verb|  then |\xverb{v =}\verb| m"*(-Sum(l)) by A6,VECTSP_1:67|\\
\verb|   .= |\xverb{-m"*Sum(l)}\verb| by VECTSP_1:69|\xsemi\\
\verb|  then|\\
\verb|A7: v = (-m")*Sum(l) by VECTSP_1:68;|\\
\verb|  Sum(l) in Lin(u) by VECTSP_7:12;|\\
\verb|  |\xverb{hence contradiction}\verb| by A1,A7,VECTSP_4:29|\xsemi\\
\verb| |\xverb{end;}\\
\verb| |\xverb{Sum(l) =}\verb| 0.E + Sum(l) by VECTSP_1:7|\\
\verb|  .= |\xverb{0.E}\verb| by A4,A5,VECTSP_1:59|\xsemi\\
\verb| then|\\
\verb|A8: |\xverb{Carrier(l) = {\char`\{}{\char`\}}}\verb| by A1,VECTSP_7:def 1|\xsemi\\
\verb| now|\\
\verb|  let x be set;|\\
\verb|A9: Carrier(m') c= {v} by VECTSP_6:def 7;|\\
\verb|  not v in Carrier(m') by A5,VECTSP_6:20;|\\
\verb|  hence not x in Carrier(m') by A9,TARSKI:def 1;|\\
\verb| end;|\\
\verb| then Carrier(m') = {} by BOOLE:def 1;|\\
\verb| then Carrier(l) \/ Carrier(m') = {} by A8;|\\
\verb| then Carrier(l') c= {} by A3,VECTSP_6:51;|\\
\verb| |\xverb{hence contradiction}\verb| by A2,BOOLE:30|\xsemi\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.1.11 -- 3.33.722


\section{Mathematical Logic: Newman's Lemma}

\subsection{Source}

Henk Barendregt, 
{\em The Lambda Calculus: Its Syntax and Semantics.}
North Holland, 1984.
Page 58.

\subsection{Informal Proof}

3.1.25. {\sc Proposition.} {\em For notions of reduction one has
$$\mbox{\rm SN}\land\mbox{\rm WCR}\Rightarrow\mbox{\rm CR}$$}%
{\sc Proof.}  By SN each term $R$-reduces to an $R$-nf.  It suffices to show that this
$R$-nf is unique.  Call $M$ {\em ambiguous\/} if $M$ $R$-reduces to two distinct $R$-nf's.
For such $M$ one has $M\to_R M'$ with $M'$ ambiguous (use WCR, see figure
3.3).  Hence by SN ambiguous terms do not exist.
\medskip
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] &&&&
& M\ar[d] &\\
& M'\ar@{->>}[ddl]\ar@{->>}[dr] && \ar@{->>}[dl]\ar@{->>}[ddr] &&\mbox{ or }&
& M'\ar@{->>}[d] &\\
&& \ar@{->>}[d] &&&&
& \ar@{->>}[dl]\ar@{->>}[dr] &\\
M_1 && M_3 && M_2 &&
M_1 && M_2}
$$
\begin{center}
{\sc fig.}~3.3.
\end{center}

\subsection{Formal Proof Sketch: Informal Layout}

\begingroup
\def\rewritearrow{\mathrel{\mbox{\rm {-}{-}{-}$>$}}}
\def\doublerewritearrow{\mathrel{\mbox{\rm {-}{-}$>\!>$}}}
{\sc theorem 3\_1\_25:}
$$\mbox{$R$ is SN \& $R$ is WCR implies $R$ is CR}$$
{\sc proof}$\,$
assume that $R$ is SN and $R$ is WCR;
for $M$ ex $M_1$ st $M$ reduces\_to $M_1$;
(for $M,M_1,M_2$ st $M$ reduces\_to $M_1$ \& $M$ reduces\_to $M_2$ holds $M_1 = M_2$)
implies $R$ is CR;
defpred ambiguous[Term of $R$] means
ex $M_1,M_2$ st $\$1$ reduces\_to $M_1$ \& $\$1$ reduces\_to $M_2$ \& $M_1 \mathrel{<>} M_2$;
now
now
let $M$ such that ambiguous[$M$];
thus ex $M'$ st $M \rewritearrow M'$ \& ambiguous[$M'$]
\begin{quote}
{\sc proof}
consider $M_1,M_2$ such that $M \doublerewritearrow M_1$ \& $M \doublerewritearrow M_2$ \& $M_1 <> M_2$;
per cases;
suppose not ex $M'$ st $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$ \& $M' \doublerewritearrow M_2$;
consider $M'$ such that $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$;
consider $M''$ such that $M \rewritearrow M''$ \& $M'' \doublerewritearrow M_2$;
consider $M'''$ such that $M' \doublerewritearrow M'''$ \& $M'' \doublerewritearrow M'''$;
consider $M_3$ such that $M''' \doublerewritearrow M_3$;
take $M'$;
thus thesis;
suppose ex $M'$ st $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$ \& $M' \doublerewritearrow M_2$;
consider $M'$ such that $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$ \& $M' \doublerewritearrow M_2$;
take $M'$;
thus thesis;
{\sc end;}
\end{quote}
{\sc end;}
thus not ex $M$ st ambiguous[$M$];
{\sc end;}
thus thesis;
{\sc end;}
\endgroup

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|theorem 3_1_25:|\\
\verb| R is SN & R is WCR implies R is CR|\\
\verb|proof|\\
\verb| assume that R is SN and R is WCR;|\\
\mizerror{4}\verb| for M ex M1 st M reduces_to M1;|\\
\verb| (for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2)|\\
\mizerror{4}\verb|  implies R is CR;|\\
\verb| defpred ambiguous[Term of R] means|\\
\verb|  ex M1,M2 st $1 reduces_to M1 & $1 reduces_to M2 & M1 <> M2;|\\
\verb| now|\\
\verb|  now|\\
\verb|   let M such that ambiguous[M];|\\
\verb|   thus ex M' st M ---> M' & ambiguous[M']|\\
\verb|   proof :: begin fig 3.3|\\
\mizerror{4}\verb|    consider M1,M2 such that M -->> M1 & M -->> M2 & M1 <> M2;|\\
\verb|    per cases;|\\
\verb|    suppose not ex M' st M ---> M' & M' -->> M1 & M' -->> M2;|\\
\mizerror{4}\verb|     consider M' such that M ---> M' & M' -->> M1;|\\
\mizerror{4}\verb|     consider M'' such that M ---> M'' & M'' -->> M2;|\\
\mizerror{4}\verb|     consider M''' such that M' -->> M''' & M'' -->> M''';|\\
\mizerror{4}\verb|     consider M3 such that M''' -->> M3;|\\
\verb|     take M';|\\
\mizerror{4,4}\verb|     thus thesis;|\\
\verb|    suppose ex M' st M ---> M' & M' -->> M1 & M' -->> M2;|\\
\mizerror{4}\verb|     consider M' such that M ---> M' & M' -->> M1 & M' -->> M2;|\\
\verb|     take M';|\\
\mizerror{4,4}\verb|     thus thesis;|\\
\verb|   end; :: end fig 3.3|\\
\verb|  end;|\\
\mizerror{4}\verb|  thus not ex M st ambiguous[M];|\\
\verb| end;|\\
\mizerror{4}\verb| thus thesis;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{theorem 3\char`_1\char`_25:}\\
\verb| |\xverb{R is SN \& R is WCR implies R is CR}\\
\xverb{proof}\\
\verb| |\xverb{assume that}\\
\verb|A1: |\xverb{R is SN and}\\
\verb|A2: |\xverb{R is WCR;}\\
\verb|A3: R is WN by A1,Th9;|\\
\verb| then |\xverb{for M ex M1 st M reduces\char`_to M1}\verb| by Def10;|\\
\verb|A4: |\xverb{(for M,M1,M2 st M reduces\char`_to M1 \& M reduces\char`_to M2 holds M1 = M2)}\\
\verb|  |\xverb{implies R is CR}\\
\verb| proof|\\
\verb|  assume|\\
\verb|A5: for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2;|\\
\verb|  let M,M',M'';|\\
\verb|  assume|\\
\verb|A6: M -->> M' & M -->> M'';|\\
\verb|  consider M1 such that|\\
\verb|A7: M' -->> M1 by A3,Def10;|\\
\verb|  consider M2 such that|\\
\verb|A8: M'' -->> M2 by A3,Def10;|\\
\verb|  M -->> M1 & M -->> M2 by A6,A7,A8,Th6;|\\
\verb|  then M' -->> M1 & M'' -->> M1 by A5,A7,A8;|\\
\verb|  hence thesis;|\\
\verb| end|\xsemi\\
\verb| |\xverb{defpred ambiguous[Term of R] means}\\
\verb|  |\xverb{ex M1,M2 st \$1 reduces\char`_to M1 \& \$1 reduces\char`_to M2 \& M1 <> M2;}\\
\verb|A9: |\xverb{now}\\
\verb|A10: |\xverb{now}\\
\verb|   |\xverb{let M such that}\\
\verb|A11: |\xverb{ambiguous[M];}\\
\verb|   |\xverb{thus ex M' st M ---> M' \& ambiguous[M']}\\
\verb|   |\xverb{proof :: begin fig 3.3}\\
\verb|    |\xverb{consider M1,M2 such that}\\
\verb|A12: |\xverb{M -->> M1 \& M -->> M2 \& M1 <> M2}\verb| by A11|\xsemi\\
\verb|    |\xverb{per cases;}\\
\verb|    |\xverb{suppose}\\
\verb|A13:  |\xverb{not ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}\\
\verb|     M1 is_nf & M2 is_nf by Def9;|\\
\verb|     then|\\
\verb|A14:  M <> M1 & M <> M2 by A12,Th8;|\\
\verb|     then |\xverb{consider M' such that}\\
\verb|A15:  |\xverb{M ---> M' \& M' -->> M1}\verb| by A12,Th7|\xsemi\\
\verb|     |\xverb{consider M'' such that}\\
\verb|A16:  |\xverb{M ---> M'' \& M'' -->> M2}\verb| by A12,A14,Th7|\xsemi\\
\verb|     |\xverb{consider M''' such that}\\
\verb|A17:  |\xverb{M' -->> M''' \& M'' -->> M'''}\verb| by A2,A15,A16,Def11|\xsemi\\
\verb|     |\xverb{consider M3 such that}\\
\verb|A18:  |\xverb{M''' -->> M3}\verb| by A3,Def10|\xsemi\\
\verb|     |\xverb{take M';}\\
\verb|     M' -->> M3 & M'' -->> M3 by A17,A18,Th6;|\\
\verb|     then M' -->> M1 & M' -->> M3 & M1 <> M3 by A13,A15,A16;|\\
\verb|     |\xverb{hence thesis}\verb| by A15|\xsemi\\
\verb|    |\xverb{suppose ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}\\
\verb|     then |\xverb{consider M' such that}\\
\verb|A19:  |\xverb{M ---> M' \& M' -->> M1 \& M' -->> M2;}\\
\verb|     |\xverb{take M';}\\
\verb|     |\xverb{thus thesis}\verb| by A12,A19|\xsemi\\
\verb|   |\xverb{end; :: end fig 3.3}\\
\verb|  |\xverb{end;}\\
\verb|  |\xverb{thus not ex M st ambiguous[M]}\verb| from SN_induction1(A1,A10)|\xsemi\\
\verb| |\xverb{end;}\\
\verb| |\xverb{thus thesis}\verb| by A4,A9|\xsemi\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.1.11 -- 3.33.722


\section{Mathematical Logic: Diaconescu's Theorem}

\subsection{Source}

Michael Beeson,
\emph{Foundations of Constructive Mathematics}.
Springer-Verlag,\penalty-10000 1985.
%Page ?.

\subsection{Informal Proof}

\begingroup
\def\N{\textbf{N}}
\def\land{\mathrel{\&}}
\parskip=\smallskipamount

\hspace{\parindent}
\textbf{1.1  Theorem}  (Diaconescu [1975]).  \emph{The axiom of choice implies the law of
excluded middle, using separation and extensionality.}

\emph{Proof.}  Let a formula $\phi$ be given; we shall derive $\phi \lor \neg\phi$.  Let $A = \{n\in\N: n
= 0 \lor (n = 1 \land \phi)\}$.  Let $B = \{n\in\N: n = 1 \lor (n = 0 \land \phi)\}$.  Then $\forall\,x\in\{A,B\}\, \exists\,y\in\N\, (y\in x)$.
Suppose $f$ is a choice function, so that $f(A)\in A$ and $f(B)\in B$.  We have
$f(A) = f(B) \lor f(A)\ne f(B)$, since the values are integers.  If $f(A) = f(B)$ then $\phi$, so
$\phi \lor \neg\phi$.  If $f(A)\ne f(B)$, then $\neg\phi$ can be derived: suppose $\phi$. Then $A = B$ by
extensionality, so $f(A) = f(B)$, contradiction.  Hence in either case $\phi \lor \neg\phi$.  \hfill$\Box$

\endgroup

\subsection{Formal Proof Sketch: Informal Layout}

\begingroup
\parskip=\smallskipamount
\def\land{\mathrel{\&}}
\def\phi{\mbox{\it phi\,}}

\hspace{\parindent}%
\textbf{scheme} Diaconescu
\emph{$\{ \phi[] \}$ : axiom\_of\_choice implies $\phi[]$ or not $\phi[]$}

\emph{proof}
 assume axiom\_of\_choice;
 set $A = \{n : n = 0\mbox{ or }(n = 1 \land \phi[])\}$;
 set $B = \{n : n = 1\mbox{ or }(n = 0 \land \phi[])\}$;
 for $x$ st $x$ in $\{A,B\}$ holds ex $y$ st $y$ in $x$;
 consider $f$ being choice\_function such that
  $f$ is extensional;
 $f.A$ in $A \land f.B$ in $B$;
 $f.A = f.B$ or $f.A <> f.B$ by excluded\_middle\_on\_integers;
 per cases;
 suppose $f.A = f.B$;
  $\phi[]$;
  thus $\phi[]$ or not $\phi[]$;
 end;
 suppose $f.A <> f.B$;
  not $\phi[]$
  proof
   assume $\phi[]$;
   $A = B$ by extensionality;
   $f.A = f.B$;
   thus contradiction;
  end;
  thus $\phi[]$ or not $\phi[]$;
 end;
\hfill
end;

\endgroup

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|scheme Diaconescu :: 1975|\\
\verb| { phi[] } : axiom_of_choice implies phi[] or not phi[]|\\
\verb|proof|\\
\verb| assume axiom_of_choice;|\\
\verb| set A = {n : n = 0 or (n = 1 & phi[])};|\\
\verb| set B = {n : n = 1 or (n = 0 & phi[])};|\\
\mizerror{4}\verb| for x st x in {A,B} holds ex y st y in x;|\\
\verb| consider f being choice_function such that|\\
\mizerror{4}\verb|  f is extensional;|\\
\mizerror{4,4}\verb| f.A in A & f.B in B;|\\
\verb| f.A = f.B or f.A <> f.B by excluded_middle_on_integers;|\\
\verb| per cases;|\\
\verb| suppose f.A = f.B;|\\
\mizerror{4}\verb|  phi[];|\\
\verb|  thus phi[] or not phi[];|\\
\verb| end;|\\
\verb| suppose f.A <> f.B;|\\
\verb|  not phi[]|\\
\verb|  proof|\\
\verb|   assume phi[];|\\
\mizerror{4}\verb|   A = B by extensionality;|\\
\mizerror{4}\verb|   f.A = f.B;|\\
\mizerror{1}\verb|   thus contradiction;|\\
\verb|  end;|\\
\verb|  thus phi[] or not phi[];|\\
\verb| end;|\\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{scheme Diaconescu \char`\{ phi[] \char`\} :}\\
\verb| |\xverb{axiom\char`\_of\char`\_choice implies phi[] or not phi[]}\\
\xverb{proof}\\
\verb| |\xverb{assume}\\
\verb|A1: |\xverb{axiom\char`\_of\char`\_choice;}\\
\verb| |\xverb{set A = \char`\{n : n = 0 or (n = 1 \char`\&\ phi[])\char`\};}\\
\verb| |\xverb{set B = \char`\{n : n = 1 or (n = 0 \char`\&\ phi[])\char`\};}\\
\verb| deffunc F(Nat) = $1;|\\
\verb| defpred P[Nat] means $1 = 0 or ($1 = 1 & phi[]);|\\
\verb| {F(n) : P[n]} is Subset of NAT from COMPLSP1:sch 1;|\\
\verb| then reconsider A as Subset of NAT;|\\
\verb| defpred Q[Nat] means $1 = 1 or ($1 = 0 & phi[]);|\\
\verb| {F(n) : Q[n]} is Subset of NAT from COMPLSP1:sch 1;|\\
\verb| then reconsider B as Subset of NAT;|\\
\verb|A2: |\xverb{for x st x in \char`\{A,B\char`\}\ holds ex y st y in x}\\
\verb| proof|\\
\verb|  let x;|\\
\verb|  assume x in {A,B};|\\
\verb|  then|\\
\verb|A3: x = A or x = B by TARSKI:def 2;|\\
\verb|  per cases by A3;|\\
\verb|  suppose|\\
\verb|A4: x = A;|\\
\verb|   take 0;|\\
\verb|   thus thesis by A4;|\\
\verb|  end;|\\
\verb|  suppose|\\
\verb|A5: x = B;|\\
\verb|   take 1;|\\
\verb|   thus thesis by A5;|\\
\verb|  end;|\\
\verb| end|\xsemi\\
\verb| consider f being choice_function such that|\\
\verb|A6: f is extensional by A1,Def3;|\\
\verb| A in {A,B} & B in {A,B} by TARSKI:def 2;|\\
\verb| then (ex y st y in A) & (ex y st y in B) by A2;|\\
\verb| then|\\
\verb|A7: |\xverb{f.A in A \char`\&\ f.B in B}\verb| by Def1|\xverb{;}\\
\verb|A8: |\xverb{f.A = f.B or f.A <> f.B by excluded\char`\_middle\char`\_on\char`\_integers;}\\
\verb| |\xverb{per cases}\verb| by A8|\xsemi\\
\verb| |\xverb{suppose}\\
\verb|A9: |\xverb{f.A = f.B;}\\
\verb|  set n = f.A;|\\
\verb|A10: n in A & n in B by A7,A9;|\\
\verb|  then|\\
\verb|A11: ex n' st n = n' & (n' = 0 or (n' = 1 & phi[]));|\\
\verb|  |\xverb{phi[]}\\
\verb|  proof|\\
\verb|   per cases by A11;|\\
\verb|   suppose|\\
\verb|A12: n = 0;|\\
\verb|    ex n' st n = n' & (n' = 1 or (n' = 0 & phi[])) by A10;|\\
\verb|    hence thesis by A12;|\\
\verb|   end;|\\
\verb|   suppose n = 1 & phi[];|\\
\verb|    hence thesis;|\\
\verb|   end;|\\
\verb|  end|\xsemi\\
\verb|  |\xverb{hence phi[] or not phi[];}\\
\verb| |\xverb{end;}\\
\verb| |\xverb{suppose}\\
\verb|A13: |\xverb{f.A <> f.B;}\\
\verb|  |\xverb{not phi[]}\\
\verb|  |\xverb{proof}\\
\verb|   |\xverb{assume}\\
\verb|A14: |\xverb{phi[];}\\
\verb|   now|\\
\verb|    let y;|\\
\verb|    hereby|\\
\verb|     assume y in A;|\\
\verb|     then ex n st y = n & (n = 0 or (n = 1 & phi[]));|\\
\verb|     then y = 0 or (y = 1 & phi[]);|\\
\verb|     then y = 1 or (y = 0 & phi[]) by A14;|\\
\verb|     hence y in B;|\\
\verb|    end;|\\
\verb|    hereby|\\
\verb|     assume y in B;|\\
\verb|     then ex n st y = n & (n = 1 or (n = 0 & phi[]));|\\
\verb|     then y = 1 or (y = 0 & phi[]);|\\
\verb|     then y = 0 or (y = 1 & phi[]) by A14;|\\
\verb|     hence y in A;|\\
\verb|    end;|\\
\verb|   end;|\\
\verb|   then |\xverb{A = B by extensionality;}\\
\verb|   then |\xverb{f.A = f.B}\verb| by A6,Def2|\xsemi\\
\verb|   |\xverb{hence contradiction}\verb| by A13|\xsemi\\
\verb|  |\xverb{end;}\\
\verb|  |\xverb{hence phi[] or not phi[];}\\
\verb| |\xverb{end;}\\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

7.0.04 -- 4.04.834


\section{Topology: Open Intervals are Connected}

\subsection{Source}

Paul Cairns and Jeremy Gow,
\emph{Elements of Euclidean and Metric Topology},
online undergraduate course notes from the IMP project.
Project web site at \url{<http://www.uclic.ucl.ac.uk/imp/>},
course notes at \url{<http://www.uclic.ucl.ac.uk/topology/>}
and the frame of this specific proof at \url{<http://www.uclic.ucl.ac.uk/topology/ConnectedInterval.html>}.

\subsection{Informal Proof}

\begingroup
\parindent=0pt
\textsf{\textbf{Theorem}}
\parskip=.5em

Open intervals are connected

\begin{tabular}{ll}
\textsc{given:}$\,$ & $a,b \in {\cal R}$ \\
\textsc{then:}  & The open interval $(a,b)$ is connected
\end{tabular}

\textsf{\textbf{Proof}}

\textsc{sketch:}

The proof proceeds by contradiction.  Suppose that $(a,b)$ were not connected.  Then there would
be a pair of non-empty disjoint proper open subsets, $U$, $V$ say, of $(a,b)$ whose union would
be $(a,b)$.  This implies a ``gap'' so we use the completeness of the real line to show that there
can't be a gap.  To do this, find a supremum of some interval which must be contained in $U$.  Note
that there is a small open ball about the supremum wich because $U$ and $V$ are open must
be contained wholly within one or other of them.  However, in both cases, this leads to a
contradiction: if the ball is in $U$ then the ball contains points in $U$ exceeding the supremum;
if the ball is in $V$ then there are points in the ball also in $U$ by definition of the
supremum.
\endgroup

\subsection{Formal Proof Sketch: Informal Layout}

\begingroup
\parindent=0pt
\textsf{\textbf{theorem}}
\parskip=.5em

$(.a,b.)$ is connected

\textsf{\textbf{proof}}

assume $(.a,b.)$ is not connected;
consider $U, V$ being non empty open Subset of \textsc{real}, $u, v$ such that 
$U \mathop{\raise 1.5pt\hbox{\scriptsize /$\backslash$}\,} V = \{\} \mathrel{\&} U \mathop{\raise 1.5pt\hbox{\scriptsize $\backslash$/}\,} V = (.a,b.) \mathrel{\&} u \mathrel{\mbox{in}} U \mathrel{\&} v \mathrel{\mbox{in}} V$ \& $u < v$;
reconsider $X = \big\{ x : (.u,x.) \mathrel{\mbox{\textsf{c}$=$}} U \big\}$ as Subset of \textsc{real}; 
set $s = \sup X$;
per cases;
suppose $s \mathrel{\mbox{in}} U$;
consider $e$ such that $e > 0 \mathrel{\&} \mbox{Ball}(s,e) \mathrel{\mbox{\textsf{c}$=$}} U$;
ex $x$ st $x \mathrel{\mbox{in}} \mbox{Ball}(s,e) \mathrel{\&} x > s$;
thus contradiction;
suppose $s \mathrel{\mbox{in}} V$;
consider $e$ such that $e > 0 \mathrel{\&} \mbox{Ball}(s,e) \mathrel{\mbox{\textsf{c}$=$}} V$;
ex $x$ st $x \mathrel{\mbox{in}} \mbox{Ball}(s,e) \mathrel{\&} x \mathrel{\mbox{in}} U$;
thus contradiction;

\textsc{end;}
\endgroup

\subsection{Formal Proof Sketch: Formal Layout}

\begin{flushleft}\footnotesize
\verb|theorem (.a,b.) is connected| \\
\verb|proof| \\
\verb| assume (.a,b.) is not connected;| \\
\verb| consider U,V being non empty open Subset of REAL, u,v such that | \\
\mizerror{4}\verb|  U /\ V = {} & U \/ V = (.a,b.) & u in U & v in V & u < v;| \\
\mizerror{4}\verb| reconsider X = { x : (.u,x.) c= U } as Subset of REAL; | \\
\verb| set s = sup X;| \\
\mizerror{4}\verb| per cases;| \\
\verb| suppose s in U;| \\
\mizerror{4}\verb|  consider e such that e > 0 & Ball(s,e) c= U;| \\
\mizerror{4}\verb|  ex x st x in Ball(s,e) & x > s;| \\
\mizerror{1}\verb|  thus contradiction;| \\
\verb| suppose s in V;| \\
\mizerror{4}\verb|  consider e such that e > 0 & Ball(s,e) c= V;| \\
\mizerror{4}\verb|  ex x st x in Ball(s,e) & x in U;| \\
\mizerror{1}\verb|  thus contradiction;| \\
\verb|end;|
\end{flushleft}

\subsection{Formal Proof}

\begin{flushleft}\footnotesize
\xverb{theorem (.a,b.) is connected} \\
\xverb{proof} \\
\verb| |\xverb{assume (.a,b.) is not connected;} \\
\verb| then consider U,V being non empty open Subset of REAL such that| \\
\verb|A1: U /\ V = {} & U \/ V = (.a,b.) by Def8;| \\
\verb| consider u such that| \\
\verb|A2: u in U by Def1;| \\
\verb| consider v such that| \\
\verb|A3: v in V by Def1;| \\
\verb| ex U,V being non empty open Subset of REAL, u,v st| \\
\verb|  U /\ V = {} & U \/ V = (.a,b.) & u in U & v in V & u < v| \\
\verb| proof| \\
\verb|  per cases by AXIOMS:21;| \\
\verb|  suppose| \\
\verb|A4: u < v;| \\
\verb|   take U,V,u,v;| \\
\verb|   thus thesis by A1,A2,A3,A4;| \\
\verb|  suppose| \\
\verb|A5: u > v;| \\
\verb|   take V,U,v,u;| \\
\verb|   thus thesis by A1,A2,A3,A5;| \\
\verb|  suppose u = v;| \\
\verb|   hence thesis by A1,A2,A3,XBOOLE_0:def 3;| \\
\verb| end;| \\
\verb| then |\xverb{consider U,V being non empty open Subset of REAL, u,v such that} \\
\verb|A6: |\xverb{U /\char`\\\ V = \char`\{\char`\}\ \char`\&\ U \char`\\/ V = (.a,b.) \char`\&\ u in U \char`\&\ v in V \char`\&\ u < v;} \\
\verb| { x : (.u,x.) c= U } c= REAL from Fr_Set0;| \\
\verb| then |\xverb{reconsider X = \char`\{\ x : (.u,x.) c= U \char`\}\ as Subset of REAL;} \\
\verb| (.u,u.) = {} by RCOMP_1:12;| \\
\verb| then (.u,u.) c= U by XBOOLE_1:2;| \\
\verb| then| \\
\verb|A7: u in X;| \\
\verb|A8: for x st x in X holds x <= v| \\
\verb| proof| \\
\verb|  let x;| \\
\verb|  assume| \\
\verb|A9: x in X & v < x;| \\
\verb|A10: v in (.u,x.) by A6,A9,JORDAN6:45;| \\
\verb|  ex x' st x = x' & (.u,x'.) c= U by A9;| \\
\verb|  hence thesis by A6,A10,XBOOLE_0:def 3;| \\
\verb| end;  | \\
\verb| for x being real number st x in X holds x <= v by A8;| \\
\verb| then reconsider X as non empty bounded_above Subset of REAL| \\
\verb|  by A7,SEQ_4:def 1;| \\
\verb| |\xverb{set s = sup X;} \\
\verb| U c= (.a,b.) & V c= (.a,b.) by A6,XBOOLE_1:7;| \\
\verb| then a < u & u <= s & s <= v & v < b| \\
\verb|  by A6,A7,A8,JORDAN6:45,SEQ_4:def 4,PSCOMP_1:10;| \\
\verb| then a < s & s < b by AXIOMS:22;| \\
\verb| then| \\
\verb|A11: s in (.a,b.) by JORDAN6:45;| \\
\verb| |\xverb{per cases}\verb| by A6,A11,XBOOLE_0:def 2|\xsemi \\
\verb| |\xverb{suppose s in U;} \\
\verb|  then |\xverb{consider e such that} \\
\verb|A12: |\xverb{e > 0 \char`\&\ Ball(s,e) c= U}\verb| by Def7|\xsemi \\
\verb|  |\xverb{ex x st x in Ball(s,e) \char`\&\ x > s} \\
\verb|  proof| \\
\verb|   take x = s + e/2;| \\
\verb|   thus x in Ball(s,e) by A12,Th2;| \\
\verb|   e/2 > 0 by A12,SEQ_2:3;| \\
\verb|   hence thesis by REAL_1:69;| \\
\verb|  end|\xsemi \\
\verb|  then consider x such that| \\
\verb|A13: x in Ball(s,e) & x > s;| \\
\verb|  (.u,x.) c= U| \\
\verb|  proof| \\
\verb|   let y be set;| \\
\verb|   assume| \\
\verb|A14: y in (.u,x.);| \\
\verb|   then reconsider y as Real;| \\
\verb|A15: u < y & y < x by A14,JORDAN6:45;| \\
\verb|   per cases;| \\
\verb|   suppose y < s;| \\
\verb|    then consider y' such that| \\
\verb|A16: y' in X & y < y' & y' <= s by Def9;| \\
\verb|    y in (.u,y'.) & ex y'' st y' = y'' & (.u,y''.) c= U| \\
\verb|     by A15,A16,JORDAN6:45;| \\
\verb|    hence thesis;| \\
\verb|   suppose y >= s;| \\
\verb|    then s in Ball(s,e) & x in Ball(s,e) & s <= y & y <= x| \\
\verb|     by A12,A13,A14,Th1,JORDAN6:45;| \\
\verb|    then y in Ball(s,e) by Th4;| \\
\verb|    hence thesis by A12;| \\
\verb|  end;| \\
\verb|  then x in X;| \\
\verb|  |\xverb{hence contradiction}\verb| by A13,SEQ_4:def 4|\xsemi \\
\verb| |\xverb{suppose s in V;} \\
\verb|  then |\xverb{consider e such that} \\
\verb|A17: |\xverb{e > 0 \char`\&\ Ball(s,e) c= V}\verb| by Def7|\xsemi \\
\verb|  |\xverb{ex x st x in Ball(s,e) \char`\&\ x in U} \\
\verb|  proof| \\
\verb|   per cases;| \\
\verb|   suppose| \\
\verb|A18: u < s - e/2;| \\
\verb|    take x = s - e/2;| \\
\verb|    thus x in Ball(s,e) by A17,Th3;| \\
\verb|    e/2 > 0 by A17,SEQ_2:3;| \\
\verb|    then x < s by REAL_2:174;| \\
\verb|    then consider x' such that| \\
\verb|A19: x' in X & x < x' & x' <= s by Def9;| \\
\verb|    x in (.u,x'.) & ex x'' st x' = x'' & (.u,x''.) c= U| \\
\verb|     by A18,A19,JORDAN6:45;| \\
\verb|    hence thesis;| \\
\verb|   suppose| \\
\verb|A20: s - e/2 <= u;| \\
\verb|    take u;| \\
\verb|    s - e/2 in Ball(s,e) & s in Ball(s,e) & s - e/2 <= u & u <= s| \\
\verb|     by A7,A17,A20,Th1,Th3,SEQ_4:def 4;| \\
\verb|    hence thesis by A6,Th4;| \\
\verb|  end|\xsemi \\
\verb|  |\xverb{hence contradiction}\verb| by A6,A17,XBOOLE_0:def 3|\xsemi \\
\xverb{end;}
\end{flushleft}

\subsection{Mizar Version}

6.3.02 -- 3.44.763


\iffalse
\section{}

\subsection{Source}

\subsection{Informal Proof}

\subsection{Formal Proof Sketch: Informal Layout}

\subsection{Formal Proof Sketch: Formal Layout}

\subsection{Formal Proof}

\subsection{Mizar Version}

6.1.11 -- 3.33.722
\fi


\section{Missing Subjects}

\begin{itemize}
\item Calculus
\item Combinatorics
\item Complex Variables
\item Differential Equations
\item Geometry
\item Integration
\item Probability Theory
\end{itemize}


\end{document}
