blob: b3c6df8eacf5814eef1577e7ddedd769c6706abd (
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
|
\import{test/phase5/exact-escape-producer.tex}
\begin{proposition}\label{phase6_admitted_omission}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Omitted.
\end{proof}
\begin{proposition}\label{phase6_rejected_declaration}
For all $x$ we have if $x = x$, then $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
Assume $x = \emptyset$.
Follows by assumption.
\end{proof}
\begin{axiom}\label{phase6_unadmitted_axiom}
For all $x$ we have $x = x$.
\end{axiom}
\begin{proposition}\label{phase6_unadmitted_omission}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Omitted.
\end{proof}
|
