diff options
Diffstat (limited to 'test/phase5')
38 files changed, 567 insertions, 28 deletions
diff --git a/test/phase5/exact-case-failure.tex b/test/phase5/exact-case-failure.tex new file mode 100644 index 0000000..95530d5 --- /dev/null +++ b/test/phase5/exact-case-failure.tex @@ -0,0 +1,14 @@ +\begin{proposition}\label{case_failure_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A=\emptyset$.} + Follows. + \caseOf{$A=\{A\}$.} + Follows. + \caseOf{$A=\{\emptyset\}$.} + Follows. + \end{byCase} +\end{proof} diff --git a/test/phase5/exact-cases-contradiction.tex b/test/phase5/exact-cases-contradiction.tex new file mode 100644 index 0000000..cf08a8e --- /dev/null +++ b/test/phase5/exact-cases-contradiction.tex @@ -0,0 +1,45 @@ +\begin{proposition}\label{cases_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A=\emptyset$.} + Follows. + \caseOf{$A=\{A\}$.} + Follows. + \caseOf{$A=A$.} + Follows. + \end{byCase} +\end{proof} + +\begin{proposition}\label{by_contradiction_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + Suppose not. + Follows. +\end{proof} + +\begin{proposition}\label{arbitrary_contradiction_exact} + Let $A$ be a set. + Suppose $A\neq A$. + Then $A=A$. +\end{proposition} +\begin{proof} + Contradiction. +\end{proof} + +\begin{proposition}\label{omitted_case_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A=A$.} + Omitted. + \caseOf{$A\neq A$.} + Follows. + \end{byCase} +\end{proof} diff --git a/test/phase5/exact-contradiction-goal.tex b/test/phase5/exact-contradiction-goal.tex deleted file mode 100644 index 007683f..0000000 --- a/test/phase5/exact-contradiction-goal.tex +++ /dev/null @@ -1,7 +0,0 @@ -\begin{proposition}\label{phase5_invalid_contradiction} - For all $A$ we have $A = A$. -\end{proposition} -\begin{proof} - Fix $A$. - Contradiction. -\end{proof} diff --git a/test/phase5/exact-datatype.tex b/test/phase5/exact-datatype.tex index 515638f..1f856e1 100644 --- a/test/phase5/exact-datatype.tex +++ b/test/phase5/exact-datatype.tex @@ -2,7 +2,7 @@ Define $\phasefivedata$ inductively as follows. \begin{enumerate} \item $\phasefivezero \in \phasefivedata$. - \item $\phasefiveatom{n} \in \phasefivedata$ for $n \in \unions{\emptyset}$. + \item $\phasefiveatom{n} \in \phasefivedata$ for $n \in \{\emptyset\}$. \item $\phasefivejoin{x}{y} \in \phasefivedata$ for $x \in \phasefivedata$ and $y \in \phasefivedata$. \end{enumerate} \end{datatype} diff --git a/test/phase5/exact-definition-alias-failure.tex b/test/phase5/exact-definition-alias-failure.tex new file mode 100644 index 0000000..e83fb3a --- /dev/null +++ b/test/phase5/exact-definition-alias-failure.tex @@ -0,0 +1,3 @@ +\begin{definition}\label{phase5_combined_alias} + The parity combined value of $X$, $\cons{X}{X}$, is $X$. +\end{definition} diff --git a/test/phase5/exact-definition-annotation-failure.tex b/test/phase5/exact-definition-annotation-failure.tex new file mode 100644 index 0000000..f772475 --- /dev/null +++ b/test/phase5/exact-definition-annotation-failure.tex @@ -0,0 +1,3 @@ +\begin{definition}\label{phase5_restricted_annotation} + A set equal to $A$ $X$ is parity restricted iff $X = X$. +\end{definition} diff --git a/test/phase5/exact-definition-boundary.tex b/test/phase5/exact-definition-boundary.tex new file mode 100644 index 0000000..d0c756c --- /dev/null +++ b/test/phase5/exact-definition-boundary.tex @@ -0,0 +1,15 @@ +\begin{definition}\label{phase5_annotated_adjective} + A set $X$ is parity canonical iff $X = X$. +\end{definition} + +\begin{definition}\label{phase5_annotated_verb} + A set $X$ parity contains $Y$ iff $Y \in X$. +\end{definition} + +\begin{definition}\label{phase5_symbolic_primary} + $\phasefivesymbolic{X} = X$. +\end{definition} + +\begin{abbreviation}\label{phase5_functional_wrapper} + The parity symbolic value of $X$ is $\phasefivesymbolic{X}$. +\end{abbreviation} diff --git a/test/phase5/exact-definition-guard-failure.tex b/test/phase5/exact-definition-guard-failure.tex new file mode 100644 index 0000000..0bab2cc --- /dev/null +++ b/test/phase5/exact-definition-guard-failure.tex @@ -0,0 +1,4 @@ +\begin{definition}\label{phase5_guarded_definition} + Suppose $\top$. + The parity guarded value of $X$ is $X$. +\end{definition} diff --git a/test/phase5/exact-direct-contradictory.tex b/test/phase5/exact-direct-contradictory.tex new file mode 100644 index 0000000..e29498e --- /dev/null +++ b/test/phase5/exact-direct-contradictory.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{direct_contradictory_exact} + Let $A$ be a set. + Suppose $A\neq A$. + Then $A=A$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} diff --git a/test/phase5/exact-induction-ambiguous.tex b/test/phase5/exact-induction-ambiguous.tex new file mode 100644 index 0000000..8029041 --- /dev/null +++ b/test/phase5/exact-induction-ambiguous.tex @@ -0,0 +1,7 @@ +\begin{proposition}\label{phase5_ambiguous_set_induction} + Let $A,B$ be sets. + Then $A=A$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Follows. +\end{proof} diff --git a/test/phase5/exact-induction-fixed.tex b/test/phase5/exact-induction-fixed.tex new file mode 100644 index 0000000..500cc55 --- /dev/null +++ b/test/phase5/exact-induction-fixed.tex @@ -0,0 +1,11 @@ +\begin{proposition}\label{phase5_fixed_set_induction} + For all sets $x$ we have $x=x$. +\end{proposition} +\begin{proof} + Fix $x$. + Show $x=x$. + \begin{subproof}[Proof by \in-induction on $x$] + Follows. + \end{subproof} + Follows by assumption. +\end{proof} diff --git a/test/phase5/exact-induction-formula-quantified.tex b/test/phase5/exact-induction-formula-quantified.tex new file mode 100644 index 0000000..9f9b322 --- /dev/null +++ b/test/phase5/exact-induction-formula-quantified.tex @@ -0,0 +1,10 @@ +\begin{proposition}\label{phase5_formula_quantified_set_induction} + $\forall x. x = x$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Show $x = x$. + \begin{subproof} + Follows. + \end{subproof} + Follows by assumption. +\end{proof} diff --git a/test/phase5/exact-induction-initial.tex b/test/phase5/exact-induction-initial.tex new file mode 100644 index 0000000..542ab40 --- /dev/null +++ b/test/phase5/exact-induction-initial.tex @@ -0,0 +1,7 @@ +\begin{proposition}\label{phase5_initial_set_induction} + Suppose $x\in A$. + Then $x=x$. +\end{proposition} +\begin{proof}[Proof by \in-induction on $x$] + Follows. +\end{proof} diff --git a/test/phase5/exact-induction-nested.tex b/test/phase5/exact-induction-nested.tex index 060a787..e9c5402 100644 --- a/test/phase5/exact-induction-nested.tex +++ b/test/phase5/exact-induction-nested.tex @@ -1,10 +1,11 @@ \begin{proposition}\label{phase5_nested_set_induction} - For all sets $x$ we have $x = x$. + Let $A$ be a set. + Then for all $x\in A$ such that $x\neq A$ we have $x = x$. \end{proposition} \begin{proof} - Fix $x$. - Show $x = x$. - \begin{subproof}[Proof by \in-induction on $x$] + Show for all $x\in A$ such that $x\neq A$ we have $x = x$. + \begin{subproof}[Proof by \in-induction] + Assume $x\in A$ and $x\neq A$. Follows by assumption. \end{subproof} Follows by assumption. diff --git a/test/phase5/exact-inductive-nested-failure.tex b/test/phase5/exact-inductive-nested-failure.tex new file mode 100644 index 0000000..0a4e9a4 --- /dev/null +++ b/test/phase5/exact-inductive-nested-failure.tex @@ -0,0 +1,21 @@ +\begin{axiom}\label{phase5_nested_failure_guard_1} + For all $A, x$ we have if $x\in\pow{\cumul{A}}$, then + $x\in\cumul{A}$. +\end{axiom} + +\begin{axiom}\label{phase5_nested_failure_guard_2} + For all $A, x$ we have if $x\in\pow{\pow{\cumul{A}}}$, then + $x\in\cumul{A}$. +\end{axiom} + +\begin{inductive}\label{phase5_nested_failure} + Define $\phasefivenestedfailure{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $x\in\pow{\phasefivenestedfailure{A}}$, then + $x\in\phasefivenestedfailure{A}$. + \item If $x\in\pow{\pow{\phasefivenestedfailure{A}}}$, then + $x\in\phasefivenestedfailure{A}$. + \item If $y\in\pow{\phasefivenestedfailure{A}}$, then + $y\in\phasefivenestedfailure{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-nested.tex b/test/phase5/exact-inductive-nested.tex index a784652..cd7cf90 100644 --- a/test/phase5/exact-inductive-nested.tex +++ b/test/phase5/exact-inductive-nested.tex @@ -1,9 +1,20 @@ -% Nested recursion is outside the exact direct-inductive fragment. +\begin{proposition}\label{phase5_nested_guard} + For all $A, x$ we have if $x\in\pow{\cumul{A}}$, then + $A\in\cumul{A}$. +\end{proposition} +\begin{proof} + Fix $A, x$. + Assume $x\in\pow{\cumul{A}}$. +\end{proof} + +\begin{axiom}\label{phase5_nested_unsafe_support} + For all $A$ we have $A=A$. +\end{axiom} \begin{inductive}\label{phase5_nested} Define $\phasefivenested{A}\subseteq\cumul{A}$ inductively as follows. \begin{enumerate} \item If $x\in\pow{\phasefivenested{A}}$, then - $x\in\phasefivenested{A}$. + $A\in\phasefivenested{A}$. \end{enumerate} \end{inductive} diff --git a/test/phase5/exact-inductive-outside-membership.tex b/test/phase5/exact-inductive-outside-membership.tex new file mode 100644 index 0000000..0cefc39 --- /dev/null +++ b/test/phase5/exact-inductive-outside-membership.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_outside_membership} + Define $\phasefiveoutside{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $\phasefiveoutside{A}=\phasefiveoutside{A}$, then + $A\in\phasefiveoutside{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-recursive-domain.tex b/test/phase5/exact-inductive-recursive-domain.tex new file mode 100644 index 0000000..2259e9e --- /dev/null +++ b/test/phase5/exact-inductive-recursive-domain.tex @@ -0,0 +1,6 @@ +\begin{inductive}\label{phase5_recursive_domain} + Define $\phasefivedomain{A}\subseteq\phasefivedomain{A}$ inductively as follows. + \begin{enumerate} + \item $A\in\phasefivedomain{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-recursive-element.tex b/test/phase5/exact-inductive-recursive-element.tex new file mode 100644 index 0000000..c8ea915 --- /dev/null +++ b/test/phase5/exact-inductive-recursive-element.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_recursive_element} + Define $\phasefiveelement{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $\phasefiveelement{A}\in\pow{\phasefiveelement{A}}$, then + $A\in\phasefiveelement{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-recursive-result.tex b/test/phase5/exact-inductive-recursive-result.tex new file mode 100644 index 0000000..3309c64 --- /dev/null +++ b/test/phase5/exact-inductive-recursive-result.tex @@ -0,0 +1,6 @@ +\begin{inductive}\label{phase5_recursive_result} + Define $\phasefiveresult{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item $\phasefiveresult{A}\in\phasefiveresult{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-unsupported-context.tex b/test/phase5/exact-inductive-unsupported-context.tex new file mode 100644 index 0000000..9783630 --- /dev/null +++ b/test/phase5/exact-inductive-unsupported-context.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_unsupported_context} + Define $\phasefiveunsupported{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $x\in\{z\in\phasefiveunsupported{A}\mid z=z\}$, then + $x\in\phasefiveunsupported{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-wrapper.tex b/test/phase5/exact-inductive-wrapper.tex new file mode 100644 index 0000000..057528c --- /dev/null +++ b/test/phase5/exact-inductive-wrapper.tex @@ -0,0 +1,22 @@ +\begin{abbreviation}\label{phase5_nested_wrapper} + $\phasefivenestedwrapper{A}=\pow{A}$. +\end{abbreviation} + +\begin{proposition}\label{phase5_nested_wrapper_guard} + For all $A, x$ we have if + $x\in\phasefivenestedwrapper{\cumul{A}}$, then + $A\in\cumul{A}$. +\end{proposition} +\begin{proof} + Fix $A, x$. + Assume $x\in\phasefivenestedwrapper{\cumul{A}}$. +\end{proof} + +\begin{inductive}\label{phase5_nested_wrapper_inductive} + Define $\phasefivenestedwrapped{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If + $x\in\phasefivenestedwrapper{\phasefivenestedwrapped{A}}$, then + $A\in\phasefivenestedwrapped{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-wrong-arguments.tex b/test/phase5/exact-inductive-wrong-arguments.tex new file mode 100644 index 0000000..76f7508 --- /dev/null +++ b/test/phase5/exact-inductive-wrong-arguments.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_wrong_arguments} + Define $\phasefivewrongargs{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $x\in\pow{\phasefivewrongargs{x}}$, then + $x\in\phasefivewrongargs{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-local-definition.tex b/test/phase5/exact-local-definition.tex index a1d2fcf..ddbd9d8 100644 --- a/test/phase5/exact-local-definition.tex +++ b/test/phase5/exact-local-definition.tex @@ -8,7 +8,7 @@ \begin{subproof} Fix $x$. Assume $x \in B$. - Follows by assumption. + Follows. \end{subproof} Follows by assumption. \end{proof} 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} 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-quantified-proposition-terms.tex b/test/phase5/exact-quantified-proposition-terms.tex new file mode 100644 index 0000000..b713700 --- /dev/null +++ b/test/phase5/exact-quantified-proposition-terms.tex @@ -0,0 +1,22 @@ +\begin{abbreviation}\label{phase5_quantified_identity} + The phase five quantified identity of $A$ is $A$. +\end{abbreviation} + +\begin{abbreviation}\label{phase5_quantified_contains} + $A$ contains $B$ iff $B\in A$. +\end{abbreviation} + +\begin{proposition}\label{phase5_quantified_function_argument} + The phase five quantified identity of every set $A$ is equal to $A$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{phase5_quantified_verb_argument} + Let $A$ be a set. + Then $A$ contains every element of $A$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} diff --git a/test/phase5/exact-quantified-subject-nested.tex b/test/phase5/exact-quantified-subject-nested.tex deleted file mode 100644 index 69bed48..0000000 --- a/test/phase5/exact-quantified-subject-nested.tex +++ /dev/null @@ -1,9 +0,0 @@ -\import{set.tex} - -\begin{definition}\label{phase5_contains} - $A$ contains $B$ iff $B\in A$. -\end{definition} - -\begin{proposition}\label{phase5_nested_quantified_subject} - Then $A$ contains every set. -\end{proposition} diff --git a/test/phase5/exact-quantified-term-valued.tex b/test/phase5/exact-quantified-term-valued.tex new file mode 100644 index 0000000..8a841f5 --- /dev/null +++ b/test/phase5/exact-quantified-term-valued.tex @@ -0,0 +1,3 @@ +\begin{abbreviation}\label{phase5_invalid_quantified_value} + The phase five invalid quantified value of $A$ is every set. +\end{abbreviation} diff --git a/test/phase5/exact-relational-replacement-failure.tex b/test/phase5/exact-relational-replacement-failure.tex new file mode 100644 index 0000000..915ba91 --- /dev/null +++ b/test/phase5/exact-relational-replacement-failure.tex @@ -0,0 +1,7 @@ +\begin{definition}\label{phase5_relational_prefix} + $\phasefiverelationalprefix = \emptyset$. +\end{definition} + +\begin{definition}\label{phase5_relational_nonfunctional} + $\phasefivenonfunctional{A} = \{ y \mid \exists x\in A. y = y \}$. +\end{definition} diff --git a/test/phase5/exact-relational-replacement-local-failure.tex b/test/phase5/exact-relational-replacement-local-failure.tex new file mode 100644 index 0000000..6a051cd --- /dev/null +++ b/test/phase5/exact-relational-replacement-local-failure.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{phase5_relational_local_failure} + For every set $A$ we have $A = A$. +\end{proposition} +\begin{proof} + Fix $A$. + Let $B = \{ y \mid \exists x\in A. y = y \}$. + Follows. +\end{proof} diff --git a/test/phase5/exact-relational-replacement.tex b/test/phase5/exact-relational-replacement.tex new file mode 100644 index 0000000..43ef06f --- /dev/null +++ b/test/phase5/exact-relational-replacement.tex @@ -0,0 +1,16 @@ +\begin{axiom}\label{phase5_relational_support} + For every set $A$ we have $A = A$. +\end{axiom} + +\begin{definition}\label{phase5_relational_replacement_definition} + $\phasefiverelational{A} = \{ y \mid \exists x\in A. y = x \}$. +\end{definition} + +\begin{proposition}\label{phase5_relational_replacement_local} + For every set $A$ we have $A = A$. +\end{proposition} +\begin{proof} + Fix $A$. + Let $B = \{ y \mid \exists x\in A. y = x \}$. + Follows. +\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..5b7e39d 100644 --- a/test/phase5/exact-separation.tex +++ b/test/phase5/exact-separation.tex @@ -3,10 +3,9 @@ \end{definition} \begin{proposition}\label{phase5_separation_theorem} - For all $A, x$ we have if $x \in \{ y \in A \mid y = y \}$, then $x \in A$. + For all $A, x$ we have if $x \in \phasefiveseparation{A}$, then $x \in A$. \end{proposition} \begin{proof} Fix $A, x$. - Assume $x \in \{ y \in A \mid y = y \}$. - Follows by assumption. + Assume $x \in \phasefiveseparation{A}$. \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} |