Exercise exact escape authority

2 files changed, 48 insertions, 0 deletions

diff --git a/test/phase5/exact-escape-consumer.tex b/test/phase5/exact-escape-consumer.tex
new file mode 100644
index 0000000..8060dcf
--- /dev/null
+++ b/test/phase5/exact-escape-consumer.tex
@@ -0,0 +1,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}
diff --git a/test/phase5/exact-escape-producer.tex b/test/phase5/exact-escape-producer.tex
new file mode 100644
index 0000000..8181112
--- /dev/null
+++ b/test/phase5/exact-escape-producer.tex
@@ -0,0 +1,10 @@
+\begin{axiom}\label{phase5_escape_source_axiom}
+    For all $x$ we have $x = x$.
+\end{axiom}
+
+\begin{proposition}\label{phase5_escape_omitted_theorem}
+    For all $x$ we have $x = x$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}