1 files changed, 82 insertions, 0 deletions
diff --git a/test/phase5/exact-proof-local-reasoning.tex b/test/phase5/exact-proof-local-reasoning.tex
new file mode 100644
index 0000000..40f9343
--- /dev/null
+++ b/test/phase5/exact-proof-local-reasoning.tex
@@ -0,0 +1,82 @@
+\begin{proposition}\label{suffices_exact}
+    Let $A$ be a set.
+    $A=A$.
+\end{proposition}
+\begin{proof}
+    It suffices to show that $A=A\land A=A$.
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{calculation_equality_exact}
+    Let $A$ be a set.
+    Suppose $A=\emptyset\land \emptyset=\{A\}$.
+    Then $A=\{A\}$.
+\end{proposition}
+\begin{proof}
+    \begin{align*}
+        A
+            &= \emptyset
+                \explanation{by \cref{suffices_exact}}
+            \\
+            &= \{A\}
+                \explanation{by assumption}
+    \end{align*}
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{calculation_biconditional_exact}
+    Let $A$ be a set.
+    $(A=A)\iff ((A=A)\lor(A\neq A))$.
+\end{proposition}
+\begin{proof}
+    \begin{align*}
+        A=A
+            &\iff \top
+                \\
+            &\iff (A=A)\lor(A\neq A)
+                \explanation{by assumption}
+    \end{align*}
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{calculation_quantified_exact}
+    Let $A$ be a set.
+    For all $x,y\in A$ such that $x=y$ we have $x=y$.
+\end{proposition}
+\begin{proof}
+    For all $x,y\in A$ such that $x=y$, we have
+    \begin{align*}
+        x
+            &= y
+    \end{align*}
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{since_structural_exact}
+    Let $A$ be a set.
+    Suppose $A=A$.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    Since $A=A$, we have $A=A$ by assumption.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{since_discharge_exact}
+    Let $A,B$ be sets.
+    Suppose $A=A$.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    Since $B=B$, we have $A=A$ by assumption.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{suffices_omitted_exact}
+    Let $A$ be a set.
+    $A=A$.
+\end{proposition}
+\begin{proof}
+    It suffices to show that $A=A$.
+    Omitted.
+\end{proof}