test/phase5/exact-inductive-recursive.tex


1
2
3
4
5
6
7
8
9
10

\begin{axiom}\label{phase5_recursive_guard}
    For all $A, x$ we have if $x \in \cumul{A}$, then $0 \in \cumul{A}$.
\end{axiom}

\begin{inductive}\label{phase5_recursive}
    Define $\phasefiverecursive{A}\subseteq\cumul{A}$ inductively as follows.
    \begin{enumerate}
        \item If $x\in\phasefiverecursive{A}$, then $0\in\phasefiverecursive{A}$.
    \end{enumerate}
\end{inductive}