blob: 8060dcf306ce57a4f3d2384f0fa9ab61431213e4 (
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
|
\import{test/phase5/exact-escape-producer.tex}
\begin{proposition}\label{phase5_from_source_axiom}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
Follows by \cref{phase5_escape_source_axiom}.
\end{proof}
\begin{proposition}\label{phase5_from_omitted_theorem}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
Follows by \cref{phase5_escape_omitted_theorem}.
\end{proof}
\begin{proposition}\label{phase5_source_axiom_through_local}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
We have $x = x$ by \cref{phase5_escape_source_axiom}.
Follows by assumption.
\end{proof}
\begin{proposition}\label{phase5_omitted_with_checked_continuation}
For all $x$ we have $x = x$.
\end{proposition}
\begin{proof}
Fix $x$.
Show $x = x$.
\begin{subproof}
Omitted.
\end{subproof}
Follows by \cref{phase5_escape_source_axiom}.
\end{proof}
|
