4 files changed, 131 insertions, 0 deletions
diff --git a/test/phase5/exact-proof-parity-invalid-assume.tex b/test/phase5/exact-proof-parity-invalid-assume.tex
new file mode 100644
index 0000000..3bb04bc
--- /dev/null
+++ b/test/phase5/exact-proof-parity-invalid-assume.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{invalid_disjunct_assume}
+    Let $A,B$ be sets.
+    $A=A$ or $B=B$.
+\end{proposition}
+\begin{proof}
+    Assume $A=A$.
+    Follows.
+\end{proof}
diff --git a/test/phase5/exact-proof-parity-invalid-fix-shape.tex b/test/phase5/exact-proof-parity-invalid-fix-shape.tex
new file mode 100644
index 0000000..16a58a2
--- /dev/null
+++ b/test/phase5/exact-proof-parity-invalid-fix-shape.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{invalid_fix_shape}
+    Let $A$ be a set.
+    $A=A$.
+\end{proposition}
+\begin{proof}
+    Fix $x\in A$.
+    Follows.
+\end{proof}
diff --git a/test/phase5/exact-proof-parity-invalid-fix.tex b/test/phase5/exact-proof-parity-invalid-fix.tex
new file mode 100644
index 0000000..0a2b24c
--- /dev/null
+++ b/test/phase5/exact-proof-parity-invalid-fix.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{invalid_bounded_fix}
+    Let $A$ be a set.
+    For all $x\in A$ we have $x\in A$.
+\end{proposition}
+\begin{proof}
+    Fix $x\notin A$.
+    Follows.
+\end{proof}
diff --git a/test/phase5/exact-proof-parity.tex b/test/phase5/exact-proof-parity.tex
new file mode 100644
index 0000000..73d849f
--- /dev/null
+++ b/test/phase5/exact-proof-parity.tex
@@ -0,0 +1,107 @@
+\begin{proposition}\label{bounded_fix_single}
+    Let $A$ be a set.
+    For all $x\in A$ we have $x\in A$.
+\end{proposition}
+\begin{proof}
+    Fix $x\in A$.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{bounded_fix_multiple}
+    Let $A$ be a set.
+    For all $x,y\in A$ we have $x\in A$ and $y\in A$.
+\end{proposition}
+\begin{proof}
+    Fix $x,y\in A$.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{bounded_fix_negative}
+    Let $A$ be a set.
+    For all $x\notin A$ we have $x\notin A$.
+\end{proposition}
+\begin{proof}
+    Fix $x\notin A$.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{fix_such_that}
+    Let $A$ be a set.
+    For all $x$ such that $x\in A$ we have $x\in A$.
+\end{proposition}
+\begin{proof}
+    Fix $x$ such that $x\in A$.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{assume_left_conjunct}
+    Let $A,B$ be sets.
+    If $A=A$ and $B=B$, then $A=A$.
+\end{proposition}
+\begin{proof}
+    Assume $A=A$.
+    Assume $B=B$.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{assume_right_conjunct}
+    Let $A,B$ be sets.
+    If $A=A$ and $B=B$, then $B=B$.
+\end{proposition}
+\begin{proof}
+    Assume $B=B$.
+    Assume $A=A$.
+    Follows by assumption.
+\end{proof}
+
+\begin{proposition}\label{take_bounded}
+    Let $A$ be a set.
+    Suppose there exists $x\in A$ such that $x=x$.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    Take $x\in A$ such that $x=x$ by assumption.
+    We have $x\in A$ by assumption.
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{take_named_noun}
+    Let $A$ be a set.
+    Suppose there exist sets $x,y$ such that $x=x$ and $y=y$.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    Take a set $x,y$ such that $x=x$ and $y=y$ by assumption.
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{take_anonymous_noun}
+    Let $A$ be a set.
+    Suppose there exists a set.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    Take a set by assumption.
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{existential_have_witness}
+    Let $A$ be a set.
+    Suppose there exists $x\in A$ such that $x=x$.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    We have there exists $x\in A$ such that $x=x$ by assumption.
+    We have $x\in A$ by assumption.
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{take_omitted_continuation}
+    Let $A$ be a set.
+    Suppose there exists $x\in A$ such that $x=x$.
+    Then $A=A$.
+\end{proposition}
+\begin{proof}
+    Take $x\in A$ such that $x=x$ by assumption.
+    Omitted.
+\end{proof}