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