blob: 0a4e9a40baf43e50adbce88abfe69178cdc28beb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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}
|
