blob: 2e8b7708f2384734df695fa62d517e2921f276d2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
\import{test/phase5/exact-producer.tex}
\begin{definition}\label{phase5_proof_seed}
$\phasefiveproofseed = \emptyset$.
\end{definition}
\begin{proposition}\label{phase5_implicit_proof}
$\phasefiveproofseed = \phasefiveproofseed$.
\end{proposition}
\begin{proposition}\label{phase5_structural_proof}
For all $x$ we have if $x = x$, then $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
Assume $x = x$.
We have $x = x$ by assumption.
Follows by \cref{phase5_definition}.
\end{proof}
\begin{proposition}\label{phase5_subclaim_proof}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
Show $x = x$.
\begin{subproof}
Follows by assumption.
\end{subproof}
Follows by assumption.
\end{proof}
\begin{proposition}\label{phase5_header_proof}
Let $A$ be a set.
Let $x \in A$.
Then $x \in A$.
\end{proposition}
\begin{proof}
Follows by assumption.
\end{proof}
\begin{proposition}\label{phase5_generalized_auto}
Let $y$ be a set.
Then $y = y$.
\end{proposition}
|
