diff options
Diffstat (limited to 'test/phase5/exact-inductive-nested-failure.tex')
| -rw-r--r-- | test/phase5/exact-inductive-nested-failure.tex | 21 |
1 files changed, 21 insertions, 0 deletions
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} |