7 files changed, 197 insertions, 2 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}
diff --git a/test/phase5/exact-replacement.tex b/test/phase5/exact-replacement.tex
index 901fabe..d23ba42 100644
--- a/test/phase5/exact-replacement.tex
+++ b/test/phase5/exact-replacement.tex
@@ -8,5 +8,4 @@
 \begin{proof}
     Fix $A, x$.
     Assume $x \in A$.
-    Follows by assumption.
 \end{proof}
diff --git a/test/phase5/exact-separation.tex b/test/phase5/exact-separation.tex
index e5b23a6..82f4263 100644
--- a/test/phase5/exact-separation.tex
+++ b/test/phase5/exact-separation.tex
@@ -8,5 +8,4 @@
 \begin{proof}
     Fix $A, x$.
     Assume $x \in \{ y \in A \mid y = y \}$.
-    Follows by assumption.
 \end{proof}
diff --git a/test/phase5/exact-structure.tex b/test/phase5/exact-structure.tex
index b1a0d86..fb34abe 100644
--- a/test/phase5/exact-structure.tex
+++ b/test/phase5/exact-structure.tex
@@ -25,3 +25,69 @@
 \begin{proof}
     Follows by assumption.
 \end{proof}
+
+\begin{proposition}\label{pointed_self_member}
+    Let $X$ be a pointed set.
+    Then $X \in X$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_member_explicit}
+    Let $X$ be a pointed set.
+    Then $X \in \carrier[X]$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_not_member}
+    Let $X$ be a pointed set.
+    Then $X \notin X$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_not_member_explicit}
+    Let $X$ be a pointed set.
+    Then $X \notin \carrier[X]$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_element}
+    Let $X$ be a pointed set.
+    Then $X$ is an element of $X$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_element_explicit}
+    Let $X$ be a pointed set.
+    Then $X$ is an element of $\carrier[X]$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_header_member}
+    Let $X$ be a pointed set.
+    Let $x \in X$.
+    Then $x = x$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_header_member_explicit}
+    Let $X$ be a pointed set.
+    Let $x \in \carrier[X]$.
+    Then $x = x$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}