In this paper we give an ordinal analysis of a set theory with $\Pi_{N}$-Collection.

§ INTRODUCTION

Throughout in this paper $N$ denotes a fixed positive integer.
In this paper we give an ordinal analysis of a Kripke-Platek
set theory with the axiom of Infinity and one of $\Pi_{N}$-Collection, denoted
by ${\sf KP}\ome+\Pi_{N}\mbox{-Collection}$.
Our proof is an extension of [1, 2].

$\Sig^{1}_{N+2}\mbox{-DC+BI}$ [$\Sig^{1}_{N+2}\mbox{-AC+BI}$]
denotes a second order arithmetic obtained from $\mbox{ACA}_{0}+\mbox{BI}$
by adding the axiom of $\Sig^{1}_{N+2}$-Dependent Choice
[$\Sig^{1}_{N+2}$-Axiom of Choice], resp.
It is easy to see that $\Sig^{1}_{N+2}\mbox{-DC+BI}$ is interpreted canonically to the set theory
${\sf KP}\ome+\Pi_{N}\mbox{-Collection}+(V=L)$ with the axiom $V=L$ of constructibility.
It is well known that $\Sig^{1}_{N+2}\mbox{-DC}_{0}$ implies $\Sig^{1}_{N+2}\mbox{-AC}$, which yields $\Del^{1}_{N+2}\mbox{-CA}$,
a fortiori $\Sig^{1}_{N+1}\mbox{-CA}$, cf. Lemma VII.6.6 of [9].
Moreover it is known that $\Sig^{1}_{N+2}\mbox{-DC+BI}$ is
$\Pi^{1}_{4}$-conservative over $\Sig^{1}_{N+2}\mbox{-AC+BI}$,
and is $\Pi^{1}_{4}$-conservative over $\Del^{1}_{N+2}\mbox{-CA+BI}$,
cf. Exercise VII.5.13 and
Theorem VII.6.16 of [9].

Let $\sig$ be a recursively regular ordinal, and $n$ a positive integer.
We say that an ordinal $\alp$ is $n$-stable if $L_{\alp}\prec_{\Sig_{n}}L$
for the constructible universe $L=\bigcup_{\alp}L_{\alp}$.
We see that
$(L_{\mI_{N}},\in)\models {\sf KP}\ome+\Pi_{N}\mbox{-Collection}$ if
$L_{\mI_{N}}$ enjoys the $\Del_{0}(\{St_{i}\}_{0<i\leq N})$-collection, where
$St_{i}$ denotes the predicate
for the class $\{\alp<\mI_{N}: L_{\alp}\prec_{\Sig_{i}}L_{\mI_{N}}\}$ of $i$-stable ordinals
in $L_{\mI_{N}}$.

We introduce an extension $S_{\mI_{N}}$ of ${\sf KP}\ome+\Pi_{N}\mbox{-Collection}$ in the language $\{\in\}\cup\{St_{i}\}_{0<i\leq N}$,
which codifies $\Sig(\{St_{i}\}_{0<i\leq N})$-reflection.
We aim to give an ordinal analysis of the theory $S_{\mI_{N}}$.

In the following theorems,
$\Ome$ denotes the least recursively regular ordinal $\ome_{1}^{CK}$, and $\psi_{\Ome}$
a collapsing function such that $\psi_{\Ome}(\alp)<\Ome$.
$\mI_{N}$ is an ordinal term denoting an ordinal such that
$L_{\mI_{N}}\models {\sf KP}\ome+\Pi_{N}\mbox{-Collection}+(V=L)$.

First we show the following Theorem <ref>.

Suppose $S_{\mI_{N}}\vdash\tht$
for a $\Sig_{1}(\Ome)$-sentence $\tht$.
$L_{\psi_{\Ome}(\veps_{\mI_{N}+1})}\models\tht$ holds.

It is not hard to see that the ordinal $\psi_{\Ome}(\veps_{\mI_{N}+1})$ is computable.
Let $<$ denote a computable well-ordering of type $\psi_{\Ome}(\veps_{\mI_{N}+1})$
on the set of natural numbers.
Conversely we show that $\Sig^{1}_{N+2}\mbox{{\rm -DC+BI}}$ proves that
each initial segment of $\psi_{\Ome}(\veps_{\mI_{N}+1})$ is well-founded.

$\Sig^{1}_{N+2}\mbox{{\rm -DC+BI}}\vdash Wo[\alp]$
for each $\alp<\psi_{\Ome}(\veps_{\mI_{N}+1})$.

For $T\supset{\rm ACA}_{0}$, $|T|$ denotes
the proof-theoretic ordinal of $T$, i.e., the supremum of order types
of computable well-orderings $\prec$ on the set of natural numbers for which
$T$ proves the fact that $\prec$ is a well-ordering.
Also let
$|{\sf KP}\ome+\Pi_{N}\mbox{-Collection}|_{\Sig_{1}^{\Ome}}$ denote the
$\Sig_{1}^{\Ome}$-ordinal of ${\sf KP}\ome+\Pi_{N}\mbox{-Collection}$, i.e., the ordinal
\min\{\alp\leq\ome_{1}^{CK}: \fal \tht\in\Sig_{1}
\left(
{\sf KP}\ome+\Pi_{N}\mbox{-Collection}\vdash\tht^{L_{\Ome}} \Rarw L_{\alp}\models\tht
\right)\}
We conclude the following Theorem <ref>, where
$\psi_{\Ome}(\veps_{\mI_{N}+1})$ denotes the order type of
the initial segment $OT(\mI_{N})\cap\Ome$ of a notation system $OT(\mI_{N})$ of

|\Del^{1}_{N+2}\mbox{{\rm -CA+BI}}|
|\Sig^{1}_{N+2}\mbox{{\rm -AC+BI}}|=
|\Sig^{1}_{N+2}\mbox{{\rm -DC+BI}}|=
|{\sf KP}\ome+\Pi_{N}\mbox{{\rm -Collection}}|_{\Sig_{1}^{\Ome}}
\psi_{\Ome}(\veps_{\mI_{N}+1})

Let $\mathbf{Z}_{2}=\Sig^{1}_{\infty}\mbox{{\rm -DC}}$ be  the full second order arithmetic with
the Dependent Choice schema, and ${\sf ZFC}-{\sf Power}$ denote
ZFC minus the power set axiom.
$\mathbf{Z}_{2}$ proves the ($\Pi^{1}_{1}$-)soundness of
$\Sigma^{1}_{N+2}\mbox{{\rm -DC}}+\mbox{BI}$,
and hence $\mathbf{Z}_{2}$ proves that
$(OT(\mI_{N}),<)$ is a well ordering for each $N$.
$\mathbf{Z}_{2}$ is canonically interpreted in $({\sf ZFC}-{\sf Power})+(V=L)$.

Assume $({\sf ZFC}-{\sf Power})+(V=L)\vdash \tht$ for a sentence $\tht$.
Since $S_{\mI_{N}}$ subsumes $\Pi_{N}\mbox{-Collection}$ and
$\Sig_{N}\mbox{-Separation}$, there is an $N$ such that
Therefore we conclude the following.

\psi_{\Omega}(\mathbb{I}_{\ome}):=\sup\{\psi_{\Omega}(\mathbb{I}_{N}) :
= |{\sf ZFC}-{\sf Power}|_{\Sigma_{1}^{\Omega}}.

Let us mention the contents of this paper.
In the next section <ref> a second order arithmetic $\Sig^{1}_{N+2}\mbox{-DC+BI}$
is interpreted to a set theory
${\sf KP}\ome+\Pi_{N}\mbox{-Collection}+(V=L)$, which is in turn shown to be
a subtheory of a set theory $S_{\mI_{N}}$.
In section <ref> ordinals for our analysis of $\Pi_{N}$-Collection are introduced,
and a computable notation system $OT(\mI_{N})$ is extracted.

Theorem <ref> is proved in sections <ref> and <ref>.
In section <ref> operator controlled derivations are introduced.
In section <ref>, stable ordinals are removed
from derivations.
Although our proof of Theorem <ref> is based on operator controlled derivations introduced by W. Buchholz[6], it is hard for us to give its sketch here.
See subsection <ref> for an outline of the proof.

Theorem <ref> is proved
in the final sections <ref> and <ref>.
For $0\leq i\leq N$, we introduce $i$-maximal distinguished sets, which are
A $0$-maximal distinguished set is $\Sig^{1}_{2}$-definable as in [1].
$\Sig^{1}_{N+2}$-(Dependent) Choice is needed to handle limits of $N$-stable ordinals.
Our proof of Theorem <ref> is based on maximal distinguished class introduced
again by Buchholz[5].
A sketch of the well-foundedness proof is outlined in subsection <ref>.

IH denotes the Induction Hypothesis, MIH the Main IH, SIH the Subsidiary IH,
and SSIH the Sub-Subsidiary IH.

§ $\PI_{N}$-COLLECTION

In this section a second order arithmetic $\Sig^{1}_{N+2}\mbox{-DC+BI}$ is interpreted canonically to a set theory
${\sf KP}\ome+\Pi_{N}\mbox{-Collection}+(V=L)$, which is in turn shown to be a subtheory of a set theory $S_{\mI_{N}}$.

For subsystems of second order arithmetic, we follow largely Simpson's monograph[9].
The schema Bar Induction, BI is denoted by TI in [9].
BI allows the transfinite induction schema for well-founded relations.

$\Sig^{1}_{N+2}\mbox{-AC+BI}$ denotes a second order arithmetic obtained from
by adding the axiom $\Sig^{1}_{N+2}\mbox{-AC}$,
$\fal n\exi XF(n,X)\to \exi Y \fal n F(n,Y_{n})$
for each $\Pi^{1}_{N+2}$-formula $F(n,X)$.
$\Sig^{1}_{N+2}\mbox{-DC+BI}$ denotes a second order arithmetic obtained from
by adding the axiom $\Sig^{1}_{N+2}\mbox{-DC}$ for each $\Pi^{1}_{N+1}$-formula $F(n,X,Y)$,
$\fal n\fal X\exi YF(n,X,Y)\to \fal X_{0}\exi Y \fal n [Y_{0}=X_{0}\land F(n,Y_{n},Y_{n+1})]$ with $m\in Y_{n}\Lrarw (n,m)\in Y$
for a bijective pairing function $(\cdot,\cdot)$.
It is easy to see that the formulas $F$ can be $\Sig^{1}_{N+2}$ in the axioms.

The axioms of the set theory ${\sf KP}\ome+\Pi_{N}\mbox{-Collection}+(V=L)$ consists of those of ${\sf KP}\ome$
(Kripke-Platek set theory with the Axiom of Infinity, cf.[4, 7]) plus the axiom
of Constructibility $V=L$, and $\Pi_{N}\mbox{-Collection}$:
for each $\Pi_{N}$-formula $A(x,y)$ in the language of set theory,
$\fal x\in a\exi yA(x,y)\to \exi b\fal x\in a\exi y\in b A(x,y)$.

$\Sig_{N}\mbox{-Separation}$ denotes the axiom $\exi y\fal x(x\in y\lrarw  x\in a \land \vphi(x))$
for each $\Sig_{N}$-formula $\vphi(x)$.
$\Del_{N+1}\mbox{-Separation}$ denotes the axiom
$\fal x\in a(\vphi(x)\lrarw \lnot \psi(x))\to \exi y\fal x(x\in y\lrarw  x\in a \land \vphi(x))$
for each $\Sig_{N+1}$-formulas $\vphi(x)$ and $\psi(x)$.

$\Sig_{N+1}\mbox{-Replacement}$ denotes the axiom stating that if
$\fal x\in a\exi !y\vphi(x,y)$, then there exists a function $f$ with its domain $dom(f)=a$ such that
$\fal x\in a\vphi(x,f(x))$
for each $\Sig_{N+1}$-formula $\vphi(x,y)$.

${\sf KP}\ome+\Pi_{N}\mbox{{\rm -Collection}}$ proves each of
$\Sig_{N}\mbox{{\rm -Separation}}$,
$\Del_{N+1}\mbox{{\rm -Separation}}$ and
$\Sig_{N+1}\mbox{{\rm -Replacement}}$.
We show that $\{x\in a:\vphi(x)\}$ exists as a set for a $\Sig_{N}$-formula $\vphi\equiv \exi y\tht(x,y)$
with a $\Pi_{N-1}$ matrix $\tht$.
We have by logic $\fal x\in a\exi y(\exi z\tht(x,z)\rarw \tht(x,y))$.
By $\Pi_{N}$-Collection pick a set $b$ so that
$\fal x\in a\exi y\in b(\vphi(x)\rarw \tht(x,y))$.
In other words,
$\{x\in a:\vphi(x)\}=\{x\in a: \exi y\in b\, \tht(x,y)\}$.

$\Del_{N+1}\mbox{-Separation}$ follows from $\Sig_{N}\mbox{-Separation}$ as in [4], p.17, Theorem 4.5($\Del$ Separation),
$\Sig_{N+1}\mbox{-Replacement}$ follows from $\Del_{N+1}\mbox{-Separation}$ as in [4], p.17, Theorem 4.6($\Sig$ Replacement).

For an ordinal $\alpha$, $L_{\alp}$ denotes the initial segment of Gödel's constructible universe
$L=\bigcup_{\alp}L_{\alp}$. $Ad(x)$ designates that $x$ is an admissible set. $<_{L}$ denotes a canonical $\Del_{1}$ well ordering of $L$, cf. p.162 of [4].

For a formula $A$ in the language of second order arithmetic let $A^{set}$ denote the formula obtained from $A$ by interpreting the first order variable $x$ as $x\in \ome$ and the second order variable $X$ as $X\subset\ome$.

The following is the Quantifier Theorem in p.125 of [7], in which
${\sf KP}l^{r}$ is defined as a set theory for limits of admissible sets with restricted induction.

For each $\Sig^{1}_{N+1}$-formula $F(n,a,Y)$,
there exists a $\Sig_{N}$-formula $A_{\Sig}(n,a,Y)$ in the language of set theory so that for
$F_{\Sig}(n,a,Y) :\Lrarw \exi d[Ad(d)\land Y\in d\land A^{d}_{\Sig}(n,a,Y)]$,

\[
{\sf KP}l^{r}\vdash n,a\in\ome\land Y\subset\ome\to \{F^{set}(n,a,Y)\lrarw F_{\Sig}(n,a,Y)\}

For each sentence $A$ in the language of second order arithmetic,

\[
\Sig^{1}_{N+2}{\rm -DC+BI}\vdash A
\Rarw
{\sf KP}\ome+\Pi_{N}\mbox{{\rm -Collection}}+(V=L)\vdash A^{set}

By the Quantifier Theorem <ref> $F^{set}(n,X,Y)$ is equivalent to a $\Pi_{N}$-formula $\vphi(n,X,Y)$
for a $\Pi^{1}_{N+1}$-formula $F(n,X,Y)$, $n\in\ome$ and $X\subset\ome$.
It suffices to show for a $\Pi_{N}$-formula $\vphi(n,X,Y)$ that assuming
$\fal n\in\ome\fal X\subset\ome\exi Y\subset\ome \vphi(n,X,Y)$ and $X_{0}\subset\ome$,
there exists a function $f$ with its domain $dom(f)=\ome$ such that
$\fal n\in\ome [f(0)=X_{0} \land \vphi(n,f(n),f(n+1))]$.
By induction on $k\in\ome$ using $V=L$ we see that there exists a unique family $(Y_{n})_{n<k}$ of subsets of $\ome$
such that
$\fal n<k[\vphi(n,Y_{n},Y_{n+1})\spand \fal Z<_{L}Y_{n+1}\neg\vphi(n,Y_{n},Z)]$.
By $\Sig_{N+1}$-Replacement pick a function $g$ with $dom(g)=\ome$ and $rng(g)\subset{}^{<\ome}{\cal P}(\ome)$
so that for any  $k\in\ome$ $g(k)$ is the unique sequence $(Y_{n})_{n<k}\in {}^{k}{\cal P}(\ome)$ with $Y_{0}=X_{0}$.
Then the function $f(n)=\left(g(n+1)\right)(n)$ is a desired one.

Next we show that ${\sf KP}\ome+\Pi_{N}\mbox{-Collection}+(V=L)$ is contained in a set theory
The language of the theory $S_{\mI_{N}}$ is $\{\in,\Ome\}\cup\{St_{i}\}_{0<i\leq N}$ with unary predicate constants $St_{i}$
and an individual constant $\Ome$.
$St_{i}(\alp)$ is intended to denote the fact that $\alp$ is an $i$-stable ordinal,
and $\Ome$ is intended to denote the least recursively regular ordinal $\ome_{1}^{CK}$.
The axioms of $S_{\mI_{N}}$ are obtained from those[In the axiom schemata $\Del_{0}$-Separation and $\Del_{0}$-Collection,
$\Del_{0}$-formulas remain to mean a $\Del_{0}$-formula in which $St_{i}$ does not occur,
while the axiom of foundation may be applied to a formula in which $St_{i}$ may occur.] of ${\sf KP}\ome$ by adding the following axioms.
By a $\Del_{0}(\{St_{i}\}_{0<i<k})$-formula we mean a bounded formula in the language

Let $ON$ denote the class of all ordinals.
For ordinals $\alp$,
$\alp^{\dagger i}$ denotes the least $i$-stable ordinal above $\alp$.
A successor $i$-stable ordinal is an ordinal $\alp^{\dagger i}$ for an $\alp$.
Note that the least $i$-stable ordinal $0^{\dagger i}$ is a successor $i$-stable ordinal.
$SSt_{i}(\alp):\Lrarw\exi\bet(\alp=\bet^{\dagger i})$, and
$LSt_{i}(\alp):\Lrarw \fal\bet<\alp(\bet^{\dagger i}<\alp)$ for $\alp>0$.

* The axiom $V=L$ of constructibility, and
the axioms for recursively regularity of $\Ome$:
$\Ome\in ON$, $\ome<\Ome$ and the $\Del_{0}$-collection schema on $\Ome$.

* $\Del_{0}(\{St_{i}\}_{0<i\leq N})\mbox{-collection}$:

\[
\fal x\in a\exi y\, \tht(x,y) \to \exi b
\fal x\in a \exi y\in b\, \tht(x,y)
\]

for each $\Del_{0}(\{St_{i}\}_{0<i\leq N})$-formula $\tht$ in which the predicates $St_{i}$ may occurs.

Note that $\Sig_{1}(\{St_{i}\}_{0<i\leq N})\mbox{-collection}$ follows from this.

* For each $i+1\leq N$, $SSt_{i+1}\subset LSt_{i}\cap St_{i}$:

St_i+1() →<<(<St_i() )
where $St_{0}(x):\Lrarw (x=x)$.
Let $\alp^{\dagger i}>\alp$ denote the least $i$-stable ordinal above an ordinal $\alp$
for $0<i\leq N$.

* Let $0<i\leq N$.
For a successor $i$-stable ordinal $\sig$,

SSt_i()(u) u∈L_ →^L_(u)
for each $\Sig_{1}(\{St_{j}\}_{j<i})$-formula $\vphi$ in the language

$S_{\mI_{N}}$ proves that
$L_{\sig}\prec_{\Sig_{i}}L$ for every $i$-stable ordinal $\sig$, i.e.,
$S_{\mI_{N}}\vdash St_{i}(\sig) \land u\in L_{\sig} \to
[\vphi^{L_{\sig}}(u)\lrarw \vphi(u)]
for set-theoretic $\Sig_{i}$-formulas $\vphi$.
Argue in $S_{\mI_{N}}$.
We show first

St_i()u∈L_ (u) →^L_(u)
for $\Sig_{1}(\{St_{j}\}_{j<i})$-formula $\vphi$ in the language $\mathcal{L}_{i}$.

We show by induction on $\sig\leq\alp$ that

\[
\vphi^{L_{\alp}}(u) \to \vphi^{L_{\sig}}(u)
\]

By IH we can assume that $\alp$ is a successor ordinal.
By the axioms (<ref>) and (<ref>)
there exists an $i$-stable ordinal $\tau$ such that
$\tau<\alp<\tau^{\dagger i}$.
Then $\vphi^{L_{\tau^{\dagger i}}}(u)$, $u\in L_{\tau}$ and $\sig\leq\tau$.
We obtain $\vphi^{L_{\tau}}(u)$ by the axiom (<ref>).
IH yields $\vphi^{L_{\sig}}(u)$.
Thus (<ref>) is shown.
In particular we obtain $L_{\sig}\prec_{\Sig_{1}}L$ for $1$-stable ordinals $\sig$.

Let $St_{N+1}(\mI_{N}):\Lrarw(0=0)$ and $\tht^{L_{\mI_{N}}}(u):\Lrarw\tht$.
Next we show

St_k() →[
^L_(u) <{St_i() u∈L_ ^L_(u)}
for $0\leq i<k\leq N+1$ and $\Pi_{1}(\{St_{j}\}_{j<i-1})$-formula $\tht(u)$.
Assume $St_{k}(\sig)$ and $\tht^{L_{\sig}}(u)$.
By the axioms (<ref>) and (<ref>)
there exists an ordinal $\kap<\sig$ such that $St_{i}(\kap)$ and $u\in L_{\kap}$.
$\tht^{L_{\kap}}(u)$ follows logically.
Conversely assume $\tht^{L_{\kap}}(u)$ for
$\kap<\sig$ such that $St_{i}(\kap)$ and $u\in L_{\kap}$.
(<ref>) yields $\tht(u)$, a fortiori $\tht^{L_{\sig}}(u)$.

Let $\vphi(u)\in\Sig_{1+n}(\{St_{j}\}_{j<i})$ and $St_{i+n}(\sig)$ with $u\in L_{\sig}$.
From (<ref>) we see by induction on $n$ that
there exists a $\Sig_{1}(\{St_{j}\}_{j<i+n})$-formula $\tht$ such that
$\vphi^{L_{\sig}}\lrarw\tht^{L_{\sig}}$ and $\vphi \lrarw\tht$.

Now we show $\vphi^{L_{\sig}}(u)\lrarw \vphi(u)$, where $0\leq n<N$,
$St_{1+n}(\sig)$, $\vphi\in\Sig_{1+n}$ and $u\in L_{\sig}$.
Suppose $\vphi^{L_{\sig}}(u)$.
Pick a $\Sig_{1}(\{St_{j}\}_{j<n})$-formula $\tht$ such that
$\vphi^{L_{\sig}}(u)\lrarw\tht^{L_{\sig}}(u)$ and $\vphi(u)\lrarw\tht(u)$.
$\tht(u)$ follows logically, and $\vphi(u)$ follows.
Conversely assume $\vphi(u)$. Then we obtain $\tht(u)$, and
(<ref>) yields $\tht^{L_{\sig}}(u)$, and hence $\vphi^{L_{\sig}}(u)$.

$S_{\mI_{N}}$ is an extension of ${\sf KP}\ome+\Pi_{N}\mbox{{\rm -Collection}}+(V=L)$.
Namely $S_{\mI_{N}}$ proves $\Pi_{N}$-Collection.
Argue in $S_{\mI_{N}}$.
Let $A(x,y)$ be a $\Pi_{N}$-formula in the language of set theory.
We obtain by the axiom (<ref>)
and Lemma <ref>

A(x,y)(St_N() x,y∈L_ A^L_(x,y))
Assume $\fal x\in a\exi yA(x,y)$.
Then we obtain
$\fal x\in a\exi y\exi \sig(St_{N}(\sig) \land x,y\in L_{\sig} \land A^{L_{\sig}}(x,y))$ by (<ref>).
Since $St_{N}(\sig) \land x,y\in L_{\sig} \land A^{L_{\sig}}(x,y)$ is a
$\Sig_{1}(\{St_{i}\}_{0<i\leq N})$-formula,
pick a set $c$ such that
$\fal x\in a\exi y\in c\exi \sig\in c(St_{N}(\sig) \land x,y\in L_{\sig} \land A^{L_{\sig}}(x,y))$
by $\Del_{0}(\{St_{i}\}_{0<i\leq N})$-Collection.
Again by (<ref>) we obtain $\fal x\in a\exi y\in c A(x,y)$.

§ ORDINALS FOR $\PI_{N}$-COLLECTION

In this section up to subsection <ref>
we work in a set theory ${\sf ZFC}(\{St_{i}\}_{0<i\leq N})$,
where each $St_{i}$ is a unary predicate symbol.
Let $St_{0}$ denote the set of uncountable cardinals below $\mI_{N}$.
$\Ome<\mI_{N}$ are strongly critical numbers, i.e.,
ordinals$>0$ which are closed under the binary Veblen function
We assume that
$St_{i+1}\subset St_{i}$ for $i<N$,
each $St_{i}$ is an unbounded class of ordinals below $\mI_{N}$ such that
the least element of $St_{i}$ is larger than $\Ome$, $\Ome<\min(\bigcup_{0<i\leq N} St_{i})$.
The predicate $St_{i}$ is identified with the class $\{\alp\in ON: \alp\in St_{i}\}$.
$\alp^{\dagger i}$ denotes the least ordinal$>\alp$ in the class $St_{i}$ when $\alp<\mI_{N}$.
$\alp^{\dagger i}:=\mI_{N}$ if $\alp\geq\mI_{N}$.
$\alp^{\dagger}:=\alp^{\dagger 1}$.
Let $SSt_{i}:=\{\alp^{\dagger i}:\alp\in ON\}$ and $LSt_{i}=St_{i}\setminus SSt_{i}$.

$\alpha>0$ is a strongly critical number if $\forall b,\xi<\alpha(\varphi_{b}(\xi)<\alpha)$.
$\Gamma_{a}$ denotes the $a$-th strongly critical number.
For ordinals $\alp$, $\veps(\alp)$ denotes the least epsilon number above $\alp$, and
$\Gam(\alp)$ the least strongly critical number above $\alp$.
For ordinals $\alp,\bet$, and $\gam$,
$\gam=\alp-\bet$ designates that $\alp=\bet+\gam$.
$\alpha\dot{+}\beta$ denotes the sum $\alpha+\beta$
when $\alpha+\beta$ equals to the commutative (natural) sum $\alpha\#\beta$, i.e., when
either $\alpha=0$ or $\alpha=\alpha_{0}+\omega^{\alpha_{1}}$ with

$u,v,w,x,y,z,\ldots$ range over sets in the universe,
$a,b,c,\alp,\bet,\gam,\del,\ldots$ range over ordinals$<\veps(\mI_{N})$, and
$\xi,\zeta,\eta,\ldots$ range over ordinals$<\Gam(\mI_{N})$,
and $\pi,\kap,\rho,\sig,\tau,\lam,\ldots$ range over ordinals$\leq\mI_{N}$.

Let $\mS\in St_{i}$ with $i>0$.
A `Mahlo degree' $m(\pi)$ of ordinals $\pi<\mS$
with higher reflections is defined to be a finite function
Let $\Lam\leq\mI_{N}$ be a strongly critical number.
To denote ordinals$<\vphi_{\Lam}(0)$,
it is convenient for us to introduce an ordinal function
$\xi<\vphi_{\Lam}(0)$ and $b<\Lam$ as in [2],
which is a $b$-th iterate of the exponential
with the base

Let $\Lam\leq\mI_{N}$ be a strongly critical number.
$\varphi_{b}(\xi)$ denotes the binary Veblen function on
$(\mI_{N})^{\dagger 0}=\omega_{\mathbb{I}_{N}+1}$ with $\varphi_{0}(\xi)=\omega^{\xi}$, and
$\tilde{\varphi}_{b}(\xi;\Lam):=\varphi_{b}(\Lam\cdot \xi)$.

Let $b,\xi<(\mI_{N})^{\dagger 0}$.
$\theta_{b}(\xi)$ [$\tilde{\theta}_{b}(\xi;\Lam)$] denotes
a $b$-th iterate of $\varphi_{0}(\xi)=\omega^{\xi}$ [of $\tilde{\varphi}_{0}(\xi)=\Lam^{\xi}$], resp.
Specifically ordinals
$\theta_{b}(\xi), \tilde{\theta}_{b}(\xi;\Lam)<\mI^{+}$ are defined by recursion on $b$ as follows.
$\tilde{\theta}_{\omega^{b}}(\xi;\Lam)=\tilde{\varphi}_{b}(\xi;\Lam)$, and
\tilde{\theta}_{c}(\tilde{\theta}_{\omega^{b}}(\xi;\Lam);\Lam)$.

Let us define a normal form of non-zero ordinals $\xi<\vphi_{\Lam}(0)$.
Let $\xi=\Lam^{\zeta}$.
If $\zeta<\Lam^{\zeta}$, then $\tilde{\theta}_{1}(\zeta;\Lam)$ is the normal form of $\xi$,
denoted by
Assume $\zeta=\Lam^{\zeta}$, and let $b>0$ be the maximal ordinal such that
there exists an ordinal $\eta$ with
Then $\xi=\tilde{\varphi}_{b}(\eta;\Lam)=_{NF}\tilde{\theta}_{\omega^{b}}(\eta;\Lam)$.

Let $\xi=\Lam^{\zeta_{m}}a_{m}+\cdots+\Lam^{\zeta_{0}}a_{0}$, where
$\zeta_{m}>\cdots>\zeta_{0}$ and $0<a_{0},\ldots,a_{m}<\Lam$.
Let $\Lam^{\zeta_{i}}=_{NF}\tilde{\theta}_{b_{i}}(\eta_{i};\Lam)$ with
$b_{i}=\omega^{c_{i}}$ for each $i$.
$\xi=_{NF}\tilde{\theta}_{b_{m}}(\eta_{m};\Lam)\cdot a_{m}+\cdots+\tilde{\theta}_{b_{0}}(\eta_{0};\Lam)\cdot a_{0}$.

Let $\xi<\vphi_{\Lam}(0)$ be a non-zero ordinal with its normal form:

\begin{equation}\label{eq:CantornfLam}
\xi=\sum_{i\leq m}\tilde{\theta}_{b_{i}}(\xi_{i};\Lam)\cdot a_{i}=_{NF}
\tilde{\theta}_{b_{m}}(\xi_{m};\Lam)\cdot a_{m}+\cdots+\tilde{\theta}_{b_{0}}(\xi_{0};\Lam)\cdot a_{0}
\end{equation}

$b_{i}=\omega^{c_{i}}<\Lam$, and
$\tilde{\theta}_{b_{0}}(\xi_{0};\Lam)$ is said to be the tail of $\xi$, denoted
$\tilde{\theta}_{b_{0}}(\xi_{0};\Lam)=tl(\xi)$, and
$\tilde{\theta}_{b_{m}}(\xi_{m};\Lam)$ the head of $\xi$, denoted

$\zeta$ is a part of $\xi$
iff there exists an $n\, (0\leq n\leq m+1)$
such that
$\zeta=_{NF}\sum_{i\geq n}\tilde{\theta}_{b_{i}}(\xi_{i};\Lam)\cdot a_{i}=
\tilde{\theta}_{b_{m}}(\xi_{m};\Lam)\cdot a_{m}+\cdots+\tilde{\theta}_{b_{n}}(\xi_{n};\Lam)\cdot a_{n}$
for $\xi$ in (<ref>).

Let $\zeta=_{NF}\tilde{\theta}_{b}(\xi;\Lam)$ with $\tilde{\theta}_{b}(\xi;\Lam)>\xi$ and $b=\omega^{b_{0}}$,
and $c$ be ordinals.
An ordinal $\tilde{\theta}_{-c}(\zeta)$ is defined recursively as follows.
If $b\geq c$, then $\tilde{\theta}_{-c}(\zeta)=\tilde{\theta}_{b-c}(\xi;\Lam)$.
Let $c>b$.
If $\xi>0$, then
$\tilde{\theta}_{-c}(\zeta)=\tilde{\theta}_{-(c-b)}(\tilde{\theta}_{b_{m}}(\xi_{m};\Lam))$ for the head term
$hd(\xi)=\tilde{\theta}_{b_{m}}(\xi_{m};\Lam)$ of
$\xi$ in (<ref>).
If $\xi=0$, then let $\tilde{\theta}_{-c}(\zeta)=0$.

Let $\xi<\vphi_{\mI_{N}}(0)$ be such that
$SC_{\mI_{N}}(\xi)\subset\Lam$ for a strongly critical number $\Lam<\mI_{N}$.
Then $\xi[\Lam/\mI_{N}]$ denotes an ordinal$<\vphi_{\Lam}(0)$ obtained from $\xi$
by changing the base $\mI_{N}$ into $\Lam$.
This means that
$\xi[\Lam:\mI_{N}]$ is obtained from $\xi$ in (<ref>)
by replacing
$\tht_{b_{i}}(\xi_{i};\mI_{N})\cdot a_{i}$ by $\tht_{b_{i}}(\xi_{i}[\Lam:\mI_{N}];\Lam)\cdot a_{i}$.

Let $\xi,\zeta<\vphi_{\mI_{N}}(0)$ be such that
$SC_{\mI_{N}}(\xi)\cup SC_{\mI_{N}}(\zeta)\subset\Lam$ for a strongly critical number $\Lam<\mI_{N}$.
$\xi<\zeta$ iff $\xi[\Lam:\mI_{N}]<\zeta[\Lam:\mI_{N}]$.

* A function $f:\Lam\to\vphi_{\Lam}(0)$ with a finite support
${\rm supp}(f)=\{c<\Lam: f(c)\neq 0\}\subset \Lam$ is said to be a finite function
with base $\Lam$
$\fal i>0(a_{i}=1)$ and $a_{0}=1$ when $b_{0}>1$
$f(c)=_{NF}\tilde{\theta}_{b_{m}}(\xi_{m};\Lam)\cdot a_{m}+\cdots+\tilde{\theta}_{b_{0}}(\xi_{0};\Lam)\cdot a_{0}$
for any $c\in{\rm supp}(f)$.

It is identified with the finite function $f\!\upharpoonright\! {\rm supp}(f)$.
When $c\not\in {\rm supp}(f)$, let $f(c):=0$.
$f,g,h,\ldots$ range over finite functions.

$SC_{\Lam}(f):=\bigcup\{\{c\}\cup SC_{\Lam}(f(c)): c\in {\rm supp}(f)\}$.

For an ordinal $c$, $f_{c}$ and $f^{c}$ are restrictions of $f$ to the domains
${\rm supp}(f_{c})=\{d\in{\rm supp}(f): d< c\}$ and ${\rm supp}(f^{c})=\{d\in{\rm supp}(f): d\geq c\}$.
$g_{c}*f^{c}$ denotes the concatenated function such that
${\rm supp}(g_{c}*f^{c})={\rm supp}(g_{c})\cup {\rm supp}(f^{c})$,
$(g_{c}*f^{c})(a)=g(a)$ for $a<c$, and
$(g_{c}*f^{c})(a)=f(a)$ for $a\geq c$.

Let $f$ be a finite function and $c<\Lam$ and $\xi<\Gam(\Lam)$ ordinals.
A relation $f<_{\Lam}^{c}\xi$ is defined by induction on the
cardinality of the finite set $\{d\in {\rm supp}(f): d>c\}$ as follows.
If $f^{c}=\emptyset$, then $f<_{\Lam}^{c}\xi$ holds.
For $f^{c}\neq\emptyset$,
$f<_{\Lam}^{c}\xi$ iff
there exists a part $\mu$ of $\xi$ such that
$f(c)< \mu$
$f<_{\Lam}^{c+d} \tilde{\theta}_{-d}(tl(\mu))$
for $d=\min\{c+d\in {\rm supp}(f): d>0\}$.

We see the following Proposition <ref>
as in [2, 1].

$f<_{\Lam}^{c}\xi\leq\zeta \Rightarrow f<_{\Lam}^{c}\zeta$.

Let $A\subset\mathbb{I}_{N}$ be a set, and $\alpha\leq\mathbb{I}_{N}$ a limit ordinal.

\[
\alpha\in M(A) :\Lrarw A\cap\alpha \mbox{ is stationary in }
\alpha
\Lrarw \mbox{ every club subset of } \alpha \mbox{ meets } A.
\]

In the following Definition <ref>,
$\varphi\alpha\beta=\varphi_{\alpha}(\beta)$ denotes the binary Veblen function on $(\mI_{N})^{\dagger 0}$, and
$\mS_{0}:=\Ome^{\dagger 1}$ the least ordinal in the class $St_{1}$.
$\xi<\Gamma(\mI_{N})$, and $X\subset\mI_{N}$,
define simultaneously
classes $\mathcal{H}_{a}(X)\subset\Gamma(\mI_{N})$,
$Mh^{a}_{i,c}(\xi)\subset(\mathbb{I}_{N}+1)\,(i>0)$, and
ordinals $\psi_{\kappa}^{f}(a)\leq\kappa$ by recursion on ordinals $a$ as follows.

$\mathcal{H}_{a}[Y](X):=\mathcal{H}_{a}(Y\cup X)
$ for $X,Y\subset \Gamma(\mI_{N})$ and $a<\varepsilon(\mI_{N})$.

(Inductive definition of $\mathcal{H}_{a}(X)$)

$\{0,\Omega,\mI_{N}\}\cup X\subset\mathcal{H}_{a}(X)$, where

If $x, y \in \mathcal{H}_{a}(X)$,
then $x+y\in \mathcal{H}_{a}(X)$,
$\varphi xy\in \mathcal{H}_{a}(X)$.

Let $\alpha=\psi_{\pi}(b)$ with $\pi\in\mathcal{H}_{a}(X)\cap SSt_{0}$,
$b\in\mathcal{H}_{a}(X)\cap a$ such that

Then $\alpha\in\mathcal{H}_{a}(X)$.

Let $\alp=\psi_{\mI_{N}}(b)$ with $b\in\mathcal{H}_{a}(X)\cap a$.

Let $\alp\in\mathcal{H}_{a}(X)\cap\mI_{N}$.
Then $\alp^{\dagger i}\in\mathcal{H}_{a}(X)\cap SSt_{i}$ for each $0< i\leq N$.

Let $\alpha=\psi_{\pi}^{f}(b)$
$b<a$, and a finite function $f:\mI_{N}\to\vphi_{\mI_{N}}(0)$ such that
$\{\pi,b\}\cup SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(X)\cap
\mathcal{H}_{b}(\alpha)$.

Then $\alpha\in\mathcal{H}_{a}(X)$.

(Definitions of $Mh^{a}_{i,c}(\xi)$ and $Mh^{a}_{i,c}(f)$ for $0<i\leq N$)

The classes $Mh^{a}_{i,c}(\xi)$ are defined for
ordinals $a<\veps(\mI_{N})$ and $\xi<\vphi_{\mI_{N}}(0)$.
By main induction on ordinals $\pi<\mI_{N}$
with subsidiary induction on $c<\mI_{N}$
we define
$\pi\in Mh^{a}_{i,c}(\xi)$ iff $\pi\in LSt_{i-1}$,
$\{a,c,\xi\}\subset\mathcal{H}_{a}(\pi)$ and
the following condition is met for any
finite functions $f,g:\mI_{N}\to\vphi_{\mI_{N}}(0)$
such that $f<_{\mI_{N}}^{c}\xi$

\[
SC_{\mI_{N}}(f,g) \subset\mathcal{H}_{a}(\pi)
\spand \pi\in Mh^{a}_{i,0}(g_{c})
\Rarw \pi\in M(Mh^{a}_{i,0}(g_{c}*f^{c}))
\]

Mh^a_i,c(f)     :=     ⋂{Mh^a_i,d(f(d)): d∈supp(f^c)}

⋂{Mh^a_i,d(f(d)): c≤d∈supp(f)}
In particular
$Mh^{a}_{i,0}(g_{c})=\bigcap\{Mh^{a}_{i,d}(g(d)): d\in {\rm supp}(g_{c})\}
=\bigcap\{Mh^{a}_{i,d}(g(d)): c> d\in {\rm supp}(g)\}$.
When $f=\emptyset$ or $f^{c}=\emptyset$, let $Mh^{a}_{i,c}(\emptyset):=LSt_{i-1}$.

(Definition of $\psi_{\pi}^{f}(a)$)

Let $a,\pi$ ordinals,
$f:\mI_{N}\to\vphi_{\mI_{N}}(0)$ a finite function.
Then $\psi_{i,\pi}^{f}(a)$ denotes the least ordinal $\kap<\pi$ such that

κ∈Mh^a_i,0(f) ℋ_a(κ)
if such a $\kap$ exists. Otherwise set $\psi_{i,\pi}^{f}(a)=\pi$.

* $\psi_{\Ome}(a):=
\min
\{\bet : \mathcal{H}_{a}(\bet)\cap\Ome\subset\bet
\}

{_N}∪{∈LSt_N : ℋ_a()∩_N⊂}

* For classes $A\subset\mathbb{I}_{N}$, let
$\alpha\in M^{a}_{i,c}(A)$ iff $\alpha\in A$ and
for any finite functions

\begin{equation}\label{eq:Mca}
\alpha\in Mh_{i,0}^{a}(g_{c}) \spand
SC_{\mI_{N}}(g_{c})\subset\mathcal{H}_{a}(\alpha) \Rarw
\alpha\in M\left( Mh_{i,0}^{a}(g_{c}) \cap A \right)
\end{equation}

Each of
$x\in Mh^{a}_{ci,}(f)$ and $x=\psi^{f}_{\kappa}(a)$
is a $\Delta_{1}(\{St_{i}\}_{0<i\leq N})$-predicate in ${\sf ZFC}(\{St_{i}\}_{0<i\leq N})$.

§.§ A small large cardinal hypothesis

It is convenient for us to assume the existence of a small large cardinal in justification of
Definition <ref>.
Shrewd cardinals as well as $\mathcal{A}$-shrewd cardinals
are introduced by M. Rathjen[8].

Let $\eta>0$.
A cardinal $\kappa$ is
$\eta$-shrewd iff for any $P\subset V_{\kappa}$, and a
set-theoretic formula $\varphi(x,y)$  if
$V_{\kappa+\eta}\models\varphi[P,\kappa]$, then there are $0<\kappa_{0},\eta_{0}<\kappa$ such that
$V_{\kappa_{0}+\eta_{0}}\models\varphi[P\cap V_{\kappa_{0}},\kappa_{0}]$.
For classes $\mathcal{A}$,
$\kappa$ is
$\mathcal{A}$-$\eta$-shrewd iff for any $P\subset V_{\kappa}$, and a formula
$\varphi(x,y)$ in the language $\{\in,\mathbf{R}\}$ with a unary predicate $\mathbf{R}$
$(V_{\kappa+\eta};\mathcal{A})\models\varphi[P,\kappa]$, then there are $0<\kappa_{0},\eta_{0}<\kappa$ such that
$(V_{\kappa_{0}+\eta_{0}};\mathcal{A})\models\varphi[P\cap V_{\kappa_{0}},\kappa_{0}]$,
where $(V_{\alp};\mathcal{A})$ denotes the structure $(V_{\alp},\in;\mathcal{A}\cap V_{\alp})$,
and for the formulas $\vphi$ in the language
$\{\in,\mathbf{R}\}$, $\mathbf{R}(t)$ is interpreted as $t\in\mathcal{A}\cap V_{\alp}$
in $(V_{\alp};\mathcal{A})\models \vphi$.

Obviously each $\mathcal{A}$-$\eta$-shrewd cardinal is $\eta$-shrewd.
We see easily that each $\eta$-shrewd cardinal is regular.
A cardinal $\kap$ is said to be $(<\eta)$-shrewd
[$\mathcal{A}$-$(<\eta)$-shrewd] if
$\kap$ is $\del$-shrewd [$\mathcal{A}$-$\del$-shrewd] for every $\del<\eta$, resp.

On the other side subtle cardinals are introduced by R. Jensen and K. Kunen.
The following Lemma <ref> is shown in [8] by Rathjen.
(Lemma 2.7 of [8])

Let $\pi$ be a subtle cardinal.
The set
$\{\kap\in V_{\pi}: (V_{\pi};\mathcal{A}) \models \mbox{`$\kap$ is $\mathcal{A}$-shrewd'}\}$
of $\mathcal{A}$-shrewd cardinals in $(V_{\pi};\mathcal{A})$
is stationary in $\pi$ for each class $\mathcal{A}$.

Let $\pi$ be a cardinal.
The classes $\mathcal{B}_{n}$ and $\mathcal{A}_{n}$ are defined recursively for $n<\ome$.
ℬ_0     =     {∈V_π: V_π}

𝒜_n     =     {i,: i≤n, ∈ℬ_i}

ℬ_n+1     =
{∈V_π: (V_π;𝒜_n)}
We say that a cardinal $\kap\in V_{\pi}$ is $n$-shrewd in $\pi$ iff
An $n$-shrewd carinal is an $n$-shrewd limit iff the set of $n$-shrewd cardinals is cofinal in it.

$\mathcal{B}_{1}$ is the set of shrewd cardinals in $V_{\pi}$, and a $1$-shrewd cardinal
is a shrewd cardinal in $\pi$.
Each $\mathcal{A}_{n+1}$-shrewd cardinal is $\mathcal{A}_{n}$-shrewd, and
each $(n+1)$-shrewd cardinal is $n$-shrewd.

Let $\pi$ be a subtle cardinal.

The set of $n$-shrewd cardinals in $\pi$ is stationary in $\pi$ for each $n<\ome$.

Let $\kap$ be an $(n+1)$-shrewd cardinal in $\pi$.
for $0<\eta<\pi$, $P\subset V_{\kappa}$ and a formula $\varphi(x,y)$ in $\{\in,\mathbf{R}\}$,
then there are an $n$-shrewd limit $\kap_{0}<\kap$
$0<\eta_{0}<\kappa$ such that
$(V_{\kappa_{0}+\eta_{0}};\mathcal{A}_{n})\models\varphi[P\cap V_{\kappa_{0}},\kappa_{0}]$.
From Lemma <ref> we see that
the set of
$\mathcal{A}_{n-1}$-shrewd cardinals is stationary in
a subtle cardinal $\pi$.

Let $\kap$ be an $(n+1)$-shrewd cardinal in $\pi$.
Then $\kap$ is $n$-shrewd, and hence
$(V_{\kap+\eta};\mathcal{A}_{n})\models\exi x(x\in P)\land \mathbf{R}(\la n,\kap\ra)$
for each $P=\{\alp\}\subset V_{\kap}$ with $\kap<\kap+\eta<\pi$.
Since $\kap$ is $\mathcal{A}_{n}$-shrewd, there are $0<\kap_{0},\eta_{0}<\kap$ such that
$(V_{\kap_{0}+\eta_{0}};\mathcal{A}_{n})\models\exi x(x\in P\cap V_{\kap_{0}}) \land \mathbf{R}(\la n,\kap_{0}\ra)$.
This means that $\alp<\kap_{0}$ is $n$-shrewd.
$\kap$ is an $n$-shrewd limit.

for $0<\eta<\pi$, $P\subset V_{\kappa}$ and a formula $\varphi(x,y)$ in $\{\in,\mathbf{R}\}$.
Then $(V_{\kappa+\eta};\mathcal{A}_{n})\models\varphi[P,\kappa]\land \mathbf{R}(\la n,\kap\ra)\land
\fal \alp<\kap\exi \sig<\kap(\sig>\alp\land \mathbf{R}(\la n,\sig\ra))$.
Since $\kap$ is $\mathcal{A}_{n}$-shrewd,
there are an $n$-shrewd limit $\kap_{0}<\kap$
$0<\eta_{0}<\kappa$ such that
$(V_{\kappa_{0}+\eta_{0}};\mathcal{A}_{n})\models\varphi[P\cap V_{\kappa_{0}},\kappa_{0}]$.

In this subsection we work in an extension $T$ of ${\sf ZFC}$ by adding
the axiom stating that
there exists a regular cardinal $\mI_{N}$ in which the set of $N$-shrewd cardinals is stationary.
$\Ome$ denotes the least uncountable ordinal $\ome_{1}$,
For $0<i<K$,
$St_{i}=\mathcal{B}_{i}$ the class of $i$-shrewd cardinals in $V_{\mI_{N}}$.
$LSt_{i}$ denotes the class of
$i$-shrewd limits in $V_{\mI_{N}}$.
Let $St_{N+1}=SSt_{N+1}=\{\mI_{N}\}$ with $\mI_{N}=\Ome^{\dagger (N+1)}$.
Also $St_{0}$ denotes the class of uncountable cardinals in $V_{\mI_{N}}$, and
$LSt_{0}$ the class of limit cardinals in $V_{\mI_{N}}$.
A successor $n$-shrewd cardinal is an $n$-shrewd cardinal in $V_{\mI_{N}}$, but not in $LSt_{n}$.

$T\vdash \forall a[
\psi_{\mI_{N}}(a)<\mI_{N}]$.
The set
$C=\{\kappa<\mI_{N} :
\mathcal{H}_{a}(\kappa)\cap\mI\subset\kappa\}$
is a club subset of the regular cardinal $\mI_{N}$.
This shows the existence of a $\kappa\in LSt_{N} \cap C$, and hence
$\psi_{\mI_{N}}(a)<\mI_{N}$ by the definition (<ref>).

$\alp^{\dagger i^{(k)}}$ is defined by recursion on $k<\ome$ by
$\alp^{\dagger i^{(0)}}=\alp$ and
$\alp^{\dagger i^{(k+1)}}=(\alp^{\dagger i^{(k)}})^{\dagger i}$.

$a\in\mathcal{H}_{a}(\psi_{\mI_{N}}(a))$, $b\in\mathcal{H}_{b}(\psi_{\mI_{N}}(b))$,
$c\in\mathcal{H}_{c}(\psi_{\Ome}(c))$ and $d\in\mathcal{H}_{d}(\psi_{\Ome}(d))$.

$\psi_{\mI_{N}}(a)<\psi_{\mI_{N}}(b)$ iff

$\Ome^{\dagger N^{(k)}}<\psi_{\mI_{N}}(b)$ for every $k<\ome$.

Let $\alp=\psi_{\mI_{N}}(a)$ and $0<k<\ome$.
Then $\alp^{\dagger N^{(k)}}<\psi_{\mI_{N}}(b)$ iff $\alp<\psi_{\mI_{N}}(b)$.
$\psi_{\mI_{N}}(b)<\alp^{\dagger N^{(k)}}$ iff $\psi_{\mI_{N}}(b)\leq\alp$.

$\psi_{\Ome}(c)<\psi_{\Ome}(d)$ iff
<ref>.<ref> and <ref>.<ref>. Let $\bet=\psi_{\mI_{N}}(b)$.
By the definition (<ref>) and
$\Ome\in\mathcal{H}_{b}(\bet)\cap\mI\subset\bet$ we obtain $\Ome<\bet$.
Let $\alp\in\{\Ome,\psi_{\mI_{N}}(a)\}$.
If $\alp<\bet$, then $\bet\in LSt_{N}$ yields $\alp^{\dagger N^{(k)}}<\bet$.

${\sf ZFC}$ proves the following:
Let $\mS$ be an $i$-shrewd cardinal with $0<i\leq N$,
$a<\veps(\mI)$, $h:\mI_{N}\to\vphi_{\mI_{N}}(0)$ a finite function
$\{a\}\cup SC_{\mI_{N}}(h)\subset\mathcal{H}_{a}(\mS)$. Then
$\mS\in Mh^{a}_{i,0}(h)\cap M(Mh^{a}_{i,0}(h))$.
By induction on $\xi<\vphi_{\mI_{N}}(0)$ we show $\mS\in Mh^{a}_{i,c}(\xi)$
for $\{a,c,\xi\}\subset\mathcal{H}_{a}(\mS)$.

Let $\{a,c,\xi\}\cup SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(\mS)$
with $f<_{\mI_{N}}^{c}\xi$ and $a<\veps(\mI_{N})$.
We show $\mS\in M^{a}_{i,c}(Mh^{a}_{i,c}(f^{c}))$,
which yields $\mS\in Mh^{a}_{i,c}(\xi)$.
IH yields $\mS\in Mh^{a}_{i,c}(f^{c})$ by $\tilde{\theta}_{-e}(\zeta)\leq\zeta$, where $\tilde{\theta}_{-e}(\zeta)$ is defined from $\tilde{\theta}(\alp;\mI_{N})$.
By the definition (<ref>) it suffices to show that

\[
\forall g
\mS\in Mh_{i,0}^{a}(g_{c}) \,\&\, SC_{\mI_{N}}(g_{c})\subset\mathcal{H}_{a}(\mS) \Rightarrow
\mS\in M\left( Mh_{i,0}^{a}(g_{c}) \cap Mh^{a}_{i,c}(f^{c})\right)

Let $g:\mI_{N}\to\vphi_{\mI_{N}}(0)$ be a finite function such that $SC_{\mI_{N}}(g_{c})\subset\mathcal{H}_{a}(\mS)$ and
$\mS\in Mh_{i,0}^{a}(g_{c})$.
We have to show $\mS\in M(A\cap B)$ for $A=Mh_{i,0}^{a}(g_{c})\cap\mS$ and
Let $C$ be a club subset of $\mS$.

We have
$\mS\in Mh_{i,0}^{a}(g_{c})\cap Mh^{a}_{i,c}(f^{c})$,
$\{a\}\cup SC_{\mI_{N}}(g_{c},f^{c})\subset\mathcal{H}_{a}(\mS)$.
Pick a $b<\mS$ so that $\{a\}\cup SC_{\mI_{N}}(g_{c},f^{c})\subset\mathcal{H}_{a}(b)$.
Since the cardinality of the set $\mathcal{H}_{a}(\mS)$ is equal to $\mS$, pick a bijection
$F:\mS\to \mathcal{H}_{a}(\mS)$.
Each $\alpha<\Gamma(\mI_{N})$ with $\alpha\in\mathcal{H}_{a}(\mS)$ is identified with its code, denoted
by $F^{-1}(\alpha)$.
Let $P$ be the class
$P=\{(\pi,d,\alpha)\in\mS^{3} : \pi\in Mh^{F(\alp)}_{i,F(d)}(F(\xi))\}$,
$F(d)\in \mathcal{H}_{a}(\mS)\cap(c+1)$ and
$F(\alpha)<\Gamma(\mI_{N})$ with
$\{F(d), F(\alpha)\}\subset\mathcal{H}_{a}(\pi)$.
For fixed $i$, $a$ and $c$, the set
\left(\mathcal{H}_{a}(\mS)\cap(c+1)\right)
\times\Gamma(\mathbb{I}_{N})   : \mS\in Mh^{a}_{i,d}(\zeta)\}$
is defined from the classes $P$ and $\{St_{j}\}_{j<i}$ by recursion on ordinals $d\leq c$.

Let $\varphi$ be a formula in $\{\in\}\cup\{St_{j}\}_{j<i}$
such that $(V_{\mS+c^{+^{i}}};\{St_{j}\}_{j<i})\models\varphi[P, C,\mS,b]$ iff
$\mS\in Mh_{i,0}^{a}(g_{c})\cap Mh^{a}_{i,c}(f^{c})$ and $C$ is a club subset of $\mS$,
where $\{St_{j}\}_{j<i}=\mathcal{A}_{i-1}$.
Since $\mS$ is $i$-shrewd in $V_{\mI_{N}}$, pick $b<\mS_{0}<\eta<\mS$ such that
$(V_{\mS_{0}+\eta};\{St_{j}\}_{j<i})\models\varphi[P\cap \mS_{0},C\cap\mS_{0},\mS_{0},b]$.
We obtain $\mS_{0}\in A\cap B\cap C$.

Therefore $\mS\in Mh^{a}_{i,c}(\xi)$ is shown
for every
This yields $\mS\in Mh_{i,0}^{a}(h)$ for
$\mS\in M(Mh^{a}_{i,0}(h))$ follows from the $i$-shrewdness of $\mS$.

Let $\mS$ be
an $i$-shrewd cardinal, $a$ an ordinal, and
$f:\mI_{N}\to\vphi_{\mI_{N}}(0)$ a finite function
such that $\{a,\mS\}\cup SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(\mathbb{S})$.
$\psi_{i,\mathbb{S}}^{f}(a)<\mathbb{S}$ holds.
Suppose $\{a,\mS\}\cup SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(\mathbb{S})$.
By Lemma <ref> we obtain
$\mathbb{S}\in M(Mh^{a}_{i,0}(f))$.
The set
\mathcal{H}_{a}(\kappa)\cap\mathbb{S}\subset\kappa,
\{a,\mS\}\cup SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(\kappa)\}$
is a club subset of
the regular cardinal $\mathbb{S}$,
and $Mh^{a}_{i,0}(f)$ is stationary in $\mathbb{S}$.
This shows the existence of a $\kappa\in Mh_{i,0}^{a}(f)\cap C\cap\mathbb{S}$, and hence
$\psi_{i,\mathbb{S}}^{f}(a)<\mathbb{S}$ by the definition (<ref>).

Let $\alp$ be either $\Ome$ or an $i$-shrewd cardinal for $0<i\leq N$
and $\mS=\alp^{\dagger i}$.
Assume $\{a,\mS\}\cup SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(\mathbb{S})$
for an ordinal $a$ and a finite function $f:\mI_{N}\to\vphi_{\mI_{N}}(0)$.
$\alp^{\dagger j}<\psi^{f}_{i,\mS}(a)$ for every $j<i$, and $\psi^{f}_{i,\mS}(a)\in LSt_{i-1}\setm St_{i}$.
Let $\kap=\psi^{f}_{i,\mS}(a)<\mS$.
We obtain $\alp\in\mathcal{H}_{a}(\kap)$ by $\alp^{\dagger i}=\mS\in\mathcal{H}_{a}(\kap)$,
and $\alp^{\dagger j}\in\mathcal{H}_{a}(\kap)\cap\mS$ for $\mS\in LSt_{j}$.
$\alp<\kap$ is seen from
$\alp^{\dagger j}\in\mathcal{H}_{a}(\kap)\cap\mS\subset\kap$
in the definition (<ref>).

The following
Corollary <ref> is seen as in [2].

For finite functions $f, g:\mI_{N}\to\Gam(\mI_{N})$,
$ Mh^{a}_{i,0}(g)\prec Mh^{a}_{i,0}(f)$ holds iff the following holds:

\[
\forall\pi\in Mh^{a}_{i,0}(f)
\left(
) \Rightarrow \pi\in M(Mh^{a}_{i,0}(g))
\right)
\]

Let $f,g:\mI_{N}\to\Gam(\mI_{N})$
be finite functions and $c\in{\rm supp}(f)$.
Assume  that
there exists an ordinal
such that
$(d,c)\cap {\rm supp}(f)=(d,c)\cap {\rm supp}(g)=\emptyset$,
\cdot\omega$,

$Mh^{a}_{i,0}(g)\prec Mh^{a}_{i,0}(f)$ holds.
In particular if $\pi\in Mh^{a}_{i,0}(f)$ and
$SC_{\mI_{N}}(g)\subset\mathcal{H}_{a}(\pi)$, then

An irreducibility of finite functions $f:\mI_{N}\to\Gam(\mI_{N})$
is defined by induction on the cardinality
$n$ of the finite set ${\rm supp}(f)$.
If $n\leq 1$, $f$ is defined to be irreducible.
Let $n\geq 2$ and $c<c+d$ be the largest two elements in ${\rm supp}(f)$, and let $g$ be
a finite function
such that ${\rm supp}(g)={\rm supp}(f_{c})\cup\{c\}$, $g_{c}=f_{c}$ and

Then $f$ is irreducible iff
$tl(f(c))>\tilde{\theta}_{d}(f(c+d);\mI_{N})$ and
$g$ is irreducible.

Let  $f,g:\mI_{N}\to\Gam(\mI_{N})$
be irreducible finite functions, and $b$ an ordinal.
Let us define a relation $f<^{b}_{lx}g$
by induction on the cardinality $\#\{e\in{\rm supp}(f)\cup{\rm supp}(g): e\geq b\}$ as follows.
$f<^{b}_{lx}g$ holds iff $f^{b}\neq g^{b}$ and
for the ordinal $c=\min\{c\geq b : f(c)\neq g(c)\}$,
one of the following conditions is met:

$f(c)<g(c)$ and let $\mu$ be the shortest part of $g(c)$ such that $f(c)<\mu$.
Then for any $c<c+d\in{\rm supp}(f)$,
if $tl(\mu)\leq\tilde{\theta}_{d}(f(c+d);\mI_{N})$, then
$f<_{lx}^{c+d}g$ holds.

$f(c)>g(c)$ and let $\nu$ be the shortest part of $f(c)$ such that $\nu>g(c)$.
Then there exist a $c<c+d\in {\rm supp}(g)$ such that
$f<_{lx}^{c+d}g$ and
$tl(\nu)\leq \tilde{\theta}_{d}(g(c+d);\mI_{N})$.

In [1]
the following Proposition <ref> is shown.

Let $f:\mI_{N}\to\Gam(\mI_{N})$.
If $f<^{0}_{lx}g$, then
$Mh^{a}_{i,0}(f)\prec Mh^{a}_{i,0}(g)$.

Let $f,g:\mI_{N}\to\Gam(\mI_{N})$ be
irreducible functions, and assume that
$\psi_{\pi}^{f}(b)<\pi$ and $\psi_{\kappa}^{g}(a)<\kappa$.

Then $\psi_{i,\pi}^{f}(b)<\psi_{i,\kappa}^{g}(a)$ iff one of the following cases holds:

$\pi\leq \psi_{i,\kappa}^{g}(a)$.

$b<a$, $\psi_{i,\pi}^{f}(b)<\kappa$, and
\}\subset\mathcal{H}_{a}(\psi_{i,\kappa}^{g}(a))$.

$b>a$, and $SC_{\mI_{N}}(g)\cup\{\kappa,a
\}\not\subset\mathcal{H}_{b}(\psi_{i,\pi}^{f}(b))$.

$b=a$, $\kappa<\pi$, and

$b=a$, $\pi=\kappa$, $SC_{\mI_{N}}(f)\subset\mathcal{H}_{a}(\psi_{i,\kappa}^{g}(a))$, and

$b=a$, $\pi=\kappa$,

This is seen from Proposition <ref> as in [2].

§.§ A computable notation system for $\Pi_{N}$-collection

Although Propositions <ref>, <ref>, and
<ref> suffice for us to define a computable notation system for
$\mathcal{H}_{\veps(\mI)}(0)$, we need a notation system closed under
Mostowski collapsings
to remove stable ordinals from derivations as in [2],
cf. section <ref>.
Two new constructors $\mI_{N}[\cdot]$ and $\mS^{\dagger\vec{i}}[\rho/\mS]$ are used to generate terms in $OT(\mI_{N})$.

$\{(\rho,\sig): \rho\prec\sig\}$ denotes the transitive closure
of the relation $\{(\rho,\sig): \exi f,a(\rho=\psi_{\sig}^{f}(a))\}$.
Let $\rho\preceq\sig:\Lrarw \rho\prec\sig \lor \rho=\sig$.

Let $\mS\in SSt_{i}$ and $\rho\prec\mS$.
We define a set $M_{\rho}=\calh_{b}(\rho)$ from $\rho$ in (<ref>)
in such a way that $\calh_{b}(\rho)\cap\mS\subset\rho$.
Then a Mostowski collapsing $M_{\rho}\ni\alp\mapsto\alp[\rho/\mS]$ in Definition <ref>
maps ordinal terms $\alp\in M_{\rho}$ to $\alp[\rho/\mS]<\mS$ isomorphically.
The transitive collapse $(M_{\rho})^{[\rho/\mS]}=\{\alp[\rho/\mS]: \alp\in M_{\rho}\}$
is an initial segment in $OT(\mI_{N})$ such that
$(M_{\rho})^{[\rho/\mS]}<\kap$ if $\rho<\kap\prec\mS$.
Note that both $\rho$ and $\kap$ are uncountable cardinals, and
the cardinality of the set $M_{\rho}$ is equal to $\rho$.

Let us define simultaneously the followings:
A set $OT(\mI_{N})$ of terms over constants $0,\Ome,\mI_{N}$ and
constructors $+,\vphi,\psi$, $\mI_{N}[*]$, $*^{\dagger i}\,(0<i\leq N)$, and
Its subsets
$SSt_{i}$, $LSt_{i}$ with $St_{i}=SSt_{i}\cup LSt_{i}$, and sets
$M_{\rho}\, (\rho\in\Psi)$,
finite sets
$K_{X}(\alp)$ of ordinals for $\sig\in St$ and $X\subset OT(\mI_{N})$.
Let $SSt=\bigcup_{0<i\leq N}SSt_{i}$ and $LSt=\bigcup_{0<i\leq N}LSt_{i}$.

For $i>0$, $\kap\in St_{i}$ is intended to designate that $\kap$ is an $i$-shrewd cardinal,
or $\kap$ is an $i$-stable ordinal.
$\kap\in SSt_{i}$ [$\kap\in LSt_{i}$] is intended to designate that $\kap$ is a
successor $i$-stable ordinal [$\kap$ is a limit of $i$-stable ordinals], resp.
$\kap\in St_{0}$ is intended to designate that $\kap$ is an uncountable cardinal,
or $\kap$ is either a recursively regular ordinal or their limit.
We have
$St_{i}=SSt_{i}\cup LSt_{i}$ with $SSt_{i}\cap LSt_{i}=\emptyset$, and
$St_{i+1}\subset LSt_{i}$.
If $\mS\in SSt_{i}$, then the ordinal term
$\psi_{\mS}^{f}(a)$ in Definition <ref>.<ref> denotes
the ordinal $\psi_{i,\mS}^{f}(a)$ in (<ref>) of Definition <ref>.<ref>.

For $\alp=\psi_{\pi}^{f}(a)$, let $m(\alp)=f$.
$SC_{\mI_{N}}(f)=\bigcup\{\{c\}\cup SC_{\mI_{N}}(f(c)): c\in {\rm supp}(f)\}$.
Immediate subterms of terms are defined as follows.
$k(\vphi\alp\bet)=\{\alp,\bet\}$, and
$k(\psi_{\sigma}^{f}(\alpha))=\{\sigma,\alpha\}\cup SC_{\mI_{N}}(f)$.

$\alp=_{NF}\alp_{m}+\cdots+\alp_{0}$ means that $\alp=\alp_{m}+\cdots+\alp_{0}$
and $\alp_{m}\geq\cdots\geq\alp_{0}$
and each $\alp_{i}$ is a non-zero additive principal number.
$\alp=_{NF}\vphi\bet\gam$ means that $\alp=\vphi\bet\gam$ and $\bet,\gam<\alp$.

$SC_{\mI_{N}}(a)$ denotes the set of strongly critical subterms$<\mI_{N}$ of $a$.
$SC_{\mI_{N}}(a)=\{a\}$ when $a<\mI_{N}$ is a strongly critical number,
$SC_{\mI_{N}}(\vphi_{\alp}(\bet))=SC_{\mI_{N}}(\alp)\cup SC_{\mI_{N}}(\bet)$ and

Note that in the following Definition <ref>, e.g.,
there is no clause for constructing $\kap=\psi_{\mS}(a)$ from $a$
for $\mS\in LSt_{i}$.

* $\alp\in\Psi :\Lrarw \exi \kap,f,a(\alp=\psi_{\kap}^{f}(a))$
$\alp\in\Psi_{\mS} :\Lrarw \exi \kap\preceq\mS\exi f,a(\alp=\psi_{\kap}^{f}(a))$.

* For a sequence $\vec{i}=(i_{0},i_{1},\ldots, i_{n})$ of numbers,
let $\alp^{\dagger\vec{i}}=(\cdots((\alp^{\dagger i_{0}})^{\dagger i_{1}}\cdots)^{\dagger i_{n}}$.

* By $\vec{i}\leq i$ let us understand that
$\vec{i}=(i_{0}, i_{1}, \ldots, i_{n})$ is a non-empty and non-increasing sequence
of numbers such that $0<i_{n}\leq\cdots\leq i_{1}\leq i_{0}\leq i$.

Let $\alp\prec\mS$ for an $\mS\in SSt$ and $b=\mathtt{ p}_{0}(\alp)$.
Then let

M_  :=  ℋ_b()

For $\alp\in\Psi$, an ordinal $\mathtt{ p}_{0}(\alp)$ is defined.
Let $\alp\in L(\mS)$ for an $\mS\in SSt$, where
$L(\mS)$ is defined in Definition <ref>.

* If $\alp\preceq\psi_{\mS}^{g}(b)$,
then $\mathtt{ p}_{0}(\alp)=b$.

* Otherwise.
Let $LSt_{i}\ni\rho\prec\mS\in SSt_{i+1}$ be such that
either $\alp\prec^{R}\mI_{N}[\rho]$ or
$\alp\prec^{R}\mS^{\dagger \vec{i}}[\rho/\mS]$ for a sequence $\vec{i}\leq i$.
Then $\alp=\bet[\rho/\mS]$ for a
$\bet\in M_{\rho}$.
$\mathtt{ p}_{0}(\alp)=\mathtt{ p}_{0}(\bet)$.

* $\mathtt{ p}_{0}(\alp)=0$ otherwise.

$\alp^{\dagger}:=\alp^{\dagger 1}$.

(Definitions of $OT(\mI_{N})$
and $K_{X}(\alp)$)

$St_{i}=SSt_{i}\cup LSt_{i}\subset OT(\mI_{N})$.
For $\del,\alp\in OT(\mI_{N})$,
$K_{\del}(\alp)=K_{X}(\alp)$, where
$X=\{\bet\in OT(\mI_{N}):\bet<\del\}$.

$\{0,\Ome, \mI_{N}\}\subset OT(\mI_{N})$ and
$\Ome^{\dagger i }\in\subset SSt_{i}$ for $0<i\leq N$.
Let $St_{N+1}=\{\mI_{N}\}$.
$\alp\in\{0,\mI_{N},\Ome\}\cup\{\Ome^{\dagger i}: 0<i\leq N\}$.

If $\alp=_{NF}\alp_{m}+\cdots+\alp_{0}\, (m>0)$ with $\{\alp_{i}:i\leq m\}\subset OT(\mI_{N})$,
$\alp\in OT(\mI_{N})$, and $m(\alp)=\emptyset$.

Let $\alp=_{NF}\vphi\bet\gam$ with $\{\bet,\gam\}\subset OT(\mI_{N})$.
$\alp\in OT(\mI_{N})$ and $m(\alp)=\emptyset$.

Let $\alp=\psi_{\Ome}(a)$ with $a\in  OT(\mI_{N})$
and $K_{\alp}(a)<a$.
$\alp\in OT(\mI_{N})$.

$K_{X}(\alp)=\emptyset$ if $\alp\in X$.
$K_{X}(\alp)=\{a\}\cup K_{X}(a)$ if $\alp\not\in X$.

Let $\alp=\psi_{\mI_{N}}(a)$ with $a\in  OT(\mI_{N})$ and $K_{\alp}(a)<a$.
$\alp\in LSt_{N}$
and $\alp^{\dagger i}\in SSt_{i}$ for $0<i\leq N$.
For $\bet\in\{\alp,\alp^{\dagger i}\}$,
$K_{X}(\alp^{\dagger i})=\emptyset$ if $\alp^{\dagger i}\in X$.
$K_{X}(\alp^{\dagger i})=K_{X}(\alp)$ if $\alp^{\dagger i}\not\in X$.
$K_{X}(\alp)=\emptyset$ if $\alp\in X$.
$K_{X}(\alp)=\{a\}\cup K_{X}(a)$ if $\alp\not\in X$.

Let $\mT\in LSt_{i}\cup\{\Ome\}$ and $\mS=\mT^{\dagger\vec{i}}\in SSt_{i+1}$
for a non-empty and non-increasing sequence of numbers
$\vec{i}=(i_{0}\geq i_{1}\geq\cdots\geq i_{n})$ such that
$i_{0}\leq i$ and $i_{n}=i+1$, cf. Proposition <ref>.
Let $\alp=\psi_{\mS}^{f}(a)$,
where $\{a,\mS\}\subset OT(\mI_{N})$, and if $f\neq\emptyset$, then
there are $\{d,\xi\}\subset OT(\mI_{N})$ such that
${\rm supp}(f)=\{d\}$, $0<f(d)=\xi<(\mI_{N})^{2}$, $d<\mI_{N}$.
$K_{\alp}(\{a\}\cup SC_{\mI_{N}}(f))<a$ for

if $\mT=\psi_{\sig}^{g}(b)$ with $k(\mT)=\{\sig,b\}\cup SC_{\mI_{N}}(g)$,

$\alp\in LSt_{i}$ and
$\alp^{\dagger j}\in SSt_{j}$ for $0<j\leq i$.

$a=\mathtt{ p}_{0}(\alp)$,
$K_{X}(\alp)=\emptyset$ if $\alp\in X$.
$K_{X}(\alp)=\{a\}\cup K_{X}(\{a,\mS\}\cup SC_{\mI_{N}}(f))$ if
$\alp\not\in X$.

$m(\alp^{\dagger j})$
$K_{X}(\alp^{\dagger j})$ are defined as in Definition <ref>.<ref>.

$\{\pi,a,d\}\subset  OT(\mI_{N})$ with
$\pi\prec\mS\in SSt_{i+1}$,
$d<c\in \supp(f)$,
and $(d,c)\cap \supp(f)=\emptyset$.

When $g\neq\emptyset$, let
be an irreducible finite function
such that
$SC_{\mI_{N}}(g)\subset OT(\mI_{N})$,
$g_{d}=f_{d}$, $(d,c)\cap \supp(g)=\emptyset$,
$g(d)<f(d)+\tilde{\theta}_{c-d}(f(c); \mI_{N})\cdot\omega$,
and $g<_{\mI_{N}}^{c}f(c)$.

$\alp=\psi_{\pi}^{g}(a)\in LSt_{i}$ and
$\alp^{\dagger j}\in SSt_{j}$ for $0<j\leq i$
$K_{\alp}(k(\alp))<a$, and

Let $m(\alp)=g$.
$K_{X}(\alp)=\emptyset$ if $\alp\in X$.
$K_{X}(\alp)=\{a\}\cup K_{X}(k(\alp))$ if $\alp\not\in X$.

$m(\alp^{\dagger j})$ and
$K_{X}(\alp^{\dagger j})$ are defined as in Definition <ref>.<ref>.

Let $\mS\in SSt_{i}$ and $0<k\leq i$.
Then $\mS^{\dagger k}\in SSt_{k}$.

$m(\mS^{\dagger k})$ and
$K_{X}(\mS^{\dagger k})$ are defined as in Definition <ref>.<ref>.

$SSt_{i}^{M}=SSt_{i}\cup\{\alp[\rho/\mS]: \rho\prec\mS\in SSt^{M}, \alp\in M_{\rho}\cap SSt_{i}^{M}\}$
$SSt^{M}=\bigcup_{0<i\leq N} SSt_{i}^{M}$.
Also let
$LSt_{i}^{M}=LSt_{i}\cup\{\alp[\rho/\mS]: \rho\prec\mS\in SSt^{M}, \alp\in M_{\rho}\cap LSt_{i}^{M}\}$
$LSt^{M}=\bigcup_{0<i\leq N} LSt_{i}^{M}$.

Let $\rho\prec\mS\in SSt_{i+1}^{M}$ and $\vec{i}=(i_{0}\geq i_{1}\geq\cdots\geq i_{n})\,(n\geq 0)$ with $0<i_{n}\leq i_{0}\leq i+1$.
$(\mS^{\dagger \vec{i}}[\rho/\mS]) \in SSt_{i+1}^{M}\subset OT(\mI_{N})$,
where a term $\mS^{\dagger \vec{i}}[\rho/\mS]$ is built from terms $\mS^{\dagger \vec{i}}$, $\rho$ and $\mS$ by the constructor $*_{0}[*_{1}/*_{2}]$.

Let $\alp=\bet[\rho/\mS]$ with
$\mS<\bet\in M_{\rho}$,
$\rho\prec\mS$, and $\mS\in SSt^{M}$.
Then $\alp\in OT(\mI_{N})\setm St$.

$\alp\in LSt_{N}$ iff $\alp=\psi_{\mI_{N}}(a)$ for an $a$.
For $0<i<N$, if $\alp\in LSt_{i}$, then there exists an $\mS\in SSt_{i+1}$ such that $\alp\prec\mS$.

In each case $LSt\subset \Psi$.

$\bet\in SSt_{k}$ iff there exists
an $\alp\in\{\Ome\}\cup LSt_{i}$ for an $k\leq i\leq N$ and
a non-empty and non-increasing sequence $\vec{i}=(i_{0}\geq i_{1}\geq\cdots\geq i_{n})$
of numbers such that $k=i_{n}>0$, $i_{0}\leq i$ and
$\bet=\alp^{\dagger \vec{i}}$.

Let $\psi_{\mS}^{f}(a)\in OT(\mI_{N})$ with $\mS\in SSt$.
Suppose that there exists a sequence $\{(\mT_{m},\mS_{m},\vec{i}_{m})\}_{m\leq n}$
of $\mT_{m}\in LSt$, $\mS_{m}\in SSt$ and sequences $\vec{i}_{m}$ of numbers such that
$\mS_{m}=\mT_{m}^{\dagger\vec{i}_{m}}$ and $\mT_{m+1}\prec\mS_{m}\,(m<n)$, and
Then $b<a$ holds.

$\alp\in SSt^{M}$ iff there exists a $\rho$ and a $\vec{i}$ such that
<ref>.<ref> and <ref>.<ref>.
We see these
from Definitions <ref>.<ref>,
<ref>.<ref> and <ref>.<ref>.

Let $\mT_{m}=\psi_{\sig_{m}}^{g_{m}}(b_{m})$ and
$\mT_{m}\preceq\psi_{\mS_{m-1}}^{f_{m-1}}(a_{m-1})$ for $\mS_{-1}=\mI_{N}$,
$f_{-1}=\emptyset$ and $a_{-1}=b$.
In general, if $\sig=\psi_{\tau}^{f}(c)\in\calh_{b}(\psi_{\sig}^{g}(b))$ with $\psi_{\sig}^{g}(b)<\sig$, then
Hence $a_{m-1}\leq b_{m}$.
On the other we obtain
$b_{m}<a_{m}$ by
(<ref>) in Definition <ref>.<ref>,
where $a_{n}=a$.
Therefore $b=a_{-1}<a_{n}=a$.

Sets $\calh_{\gam}(X)$ are defined for $\{\gam\}\cup X\subset OT(\mI_{N})$ in such a way that
$\alp\in\mathcal{H}_{\gam}(X)$ iff $K_{X}(\alp)<\gam$
$\alp,\gam\in OT(\mI_{N})$ and $X\subset OT(\mI_{N})$.
In particular $OT(\mI_{N})=\calh_{\veps_{\mI_{N}+1}}(0)$, and
$\calh_{\gam}(X)$ is closed under Mostowski collapsing $\alp\mapsto\alp[\rho/\mS]$
if $\gam\geq\mI_{N}$, and differ from sets defined in Definition <ref>.

We define terms $\alp[\rho/\mS]$, sets
$K_{X}(\alp[\rho/\mS])$ and a relation $\bet<\gam$ on $OT(\mI_{N})$
recursively as follows.

(Definitions of $\alp[\rho/\mS]$ and $K_{X}(\alp[\rho/\mS])$)

Let $\rho\prec\mS\in SSt_{i+1}^{M}$.
We define a term $\alp[\rho/\mS]\in OT(\mI_{N})$ for $\alp\in M_{\rho}$
in such a way that
$\alp[\rho/\mS]=\alp$ iff $\alp<\rho$.
$\alp[\rho/\mS]\in St$ iff either $\alp[\rho/\mS]=\alp\in St$ or $\alp[\rho/\mS]=\rho\in SSt$.

is defined
recursively as follows.
The map commutes with $\psi$,
$\vphi$, $\mI_{N}[\cdot]$, and $+$.
$K_{X}(\alp[\rho/\mS])=\emptyset$ if $\alp[\rho/\mS]\in X$.

* $\alp[\rho/\mS]:=\alp$ when $\alp<\mS$.

In what follows assume $\alp\geq\mS$, $\alp[\rho/\mS]\geq\sig$ and
$\alp[\rho/\mS]\not\in X$.

* $(\mS)[\rho/\mS]:=\rho$ and $(\mathbb{I}_{N})[\rho/\mS]:=\mathbb{I}_{N}[\rho]$.

For $\vec{i}\leq i+1$,
$(\mS^{\dagger \vec{i}})[\rho/\mS]:=\mS^{\dagger \vec{i}}[\rho/\mS]\in SSt_{i+1}^{M}$, cf. Definition <ref>.<ref>.
$\mS^{\dagger \vec{i}}[\rho/\mS]\neq\rho^{\dagger \vec{i}}$.

$K_{X}(\alp[\rho/\mS])=K_{X}(\rho)$ if
$\alp[\rho/\mS]\in\{\mI_{N}[\rho],\mS^{\dagger \vec{i}}\}$.

* Let $\alp=\psi_{\kap}^{f}(a)$. Then
\psi_{\kap[\rho/\mS]}^{f[\rho/\mS]}(a[\rho/\mS])$, where $(f[\rho/\mS]):\Lam[\rho/\mS]\to\vphi_{\Lam[\rho/\mS]}(0)$,
${\rm supp}(f[\rho/\mS])=({\rm supp}(f))[\rho/\mS]=\{c[\rho/\mS]: c\in{\rm supp}(f)\}$ and
for $f:\Lam\to\vphi_{\Lam}(0)$ and $c\in{\rm supp}(f)$.

$K_{X}(\alp[\rho/\mS])=K_{X}(\{\kap[\rho/\mS], a[\rho/\mS]\}\cup SC_{\mI_{N}}(f[\rho/\mS]))\cup\{a[\rho/\mS]\}$.

$M_{\alp[\rho/\mS]}=\calh_{b[\rho/\mS]}(\alp[\rho/\mS])$ for
$b=\mathtt{p}_{0}(\alp)$ and $b[\rho/\mS]=\mathtt{p}_{0}(\alp[\rho/\mS])$.

* Let $\alp=\mI_{N}[\tau]\neq\mI_{N}$. Then
$\alp[\rho/\mS]=\mI_{N}[\tau[\rho/\mS]]$, where
$\mI_{N}[\tau]\in M_{\rho}$ iff $\tau\in M_{\rho}$.

* Let $\alp=\tau^{\dagger \vec{j}}$ with $\mS<\tau\in LSt^{M}$. Then
$\alp[\rho/\mS]=(\tau[\rho/\mS])^{\dagger \vec{j}}$,
$\tau^{\dagger \vec{j}}\in M_{\rho}$
iff $\tau\in M_{\rho}$.

* Let $\alp=\mT^{\dagger \vec{j}}[\tau/\mT]$, where $\tau\prec\mT\in SSt^{M}$.
Then $\alp[\rho/\mS]=\mT^{\dagger \vec{j}}_{1}[\tau_{1}/\mT_{1}]$, where
$\tau_{1}=\tau[\rho/\mS] \prec \mT_{1}=\mT[\rho/\mS]\in SSt^{M}$ and
$\mT^{\dagger \vec{j}}_{1}=(\mT_{1})^{\dagger \vec{j}}$.

* Let $\alp=\vphi\bet\gam$. Then

$K_{X}(\alp[\rho/\mS])=K_{X}(\bet[\rho/\mS], \gam[\rho/\mS])$.

* For $\alp=\alp_{m}+\cdots+\alp_{0}\, (m>0)$,
$K_{X}(\alp[\rho/\mS])=\bigcup\{K_{X}(\alp_{i}[\rho/\mS])): i\leq m\}$.

A relation $\alp<\bet$ for $\alp,\bet\in OT(\mI_{N})$ is defined according to
Lemmas <ref> and <ref>,
Propositions <ref>, <ref>, and
Corollary <ref>, provided that
$\alp\in\calh_{\gam}(X)$ is replaced by $K_{X}(\alp)<\gam$.
The relation enjoys
$\psi_{\kap}^{f}(a)<\kap$ according to Lemma <ref> and Corollary <ref>.
Moreover we obtain
$\mS^{\dagger i}<\psi_{\mS^{\dagger (i+1)}}^{g_{0}}(b_{0})<\mS^{\dagger (i+1)}$ for $i+1\leq N$,
$LSt_{N}\ni \tau_{0}=\psi_{\mI_{N}}(c_{0})<\psi_{\tau_{0}^{\dagger}}^{h_{0}}(d_{0})<\tau_{0}^{\dagger}<\mI_{N}$
by Proposition <ref> and Lemma <ref>.
Hence if $\mS<\psi_{\mI_{N}}(c_{0})$, then
$\mS<\mS^{\dagger i}<\psi_{\mS^{\dagger(i+1)}}^{g_{0}}(b_{0})<\mS^{\dagger (i+1)}<
\tau_{0}=\psi_{\mI_{N}}(c_{0})<\psi_{\tau_{0}^{\dagger}}^{h_{0}}(d_{0})<\tau_{0}^{\dagger}<\mI_{N}$.
The Mostowski collapsing $\cdot[\rho/\mS]$ maps this isomorphically to
$\rho<\mS^{\dagger i}[\rho/\mS]<\psi_{\mS^{\dagger (i+1)}[\rho/\mS]}^{g}(b)<\mS^{\dagger (i+1)}[\rho/\mS]<\tau=\psi_{\mI_{N}[\rho]}(c)<
\psi_{\tau^{\dagger}}^{h}(d)<\tau^{\dagger}<\mI_{N}[\rho]<\rho^{\dagger 0}$, where
$b=b_{0}[\rho/\mS]$, etc.

For terms $\pi,\kappa\in OT(\mI_{N})$,
a relation $\pi\prec^{R} \kap$ is defined recursively as follows.

Let $\pi\prec\kap\preceq \mS\in SSt_{i+1}^{M}$, and
$\vec{i}\leq i+1$.
each of
$\mS^{\dagger\vec{i}}[\pi/\mS]\prec^{R}\kap$ and $\mI_{N}[\pi]\prec^{R}\kap$
Moreover $\pi^{\dagger \vec{i}}\prec^{R}\kap$ holds provided that
$\pi^{\dagger \vec{i}}\not\in SSt$.

$\tau\prec^{R}\pi\prec^{R}\kap\Rarw \tau\prec^{R}\kap$.
Let $\pi\preceq^{R}\kappa:\Lrarw \pi\prec^{R}\kappa \lor \pi=\kappa$.

For $\mS\in SSt$, let
$L(\mS):=\{\alp\in OT(\mI_{N}): \alp\prec^{R}\mS\}$.

Note that $L(\mS)\cap SSt=\emptyset$, and
$SSt\ni\rho^{\vec{i}}\not\prec^{R}\mS$ for $LSt_{i}\ni\rho\prec\mS\in SSt_{i+1}$
and $\vec{i}\leq i$.
For each strongly critical number $\Ome<\alp\not\in \{\mI_{N}\}\cup LSt\cup SSt$,
there exists a unique $\mS\in SSt$ such that $\alp\prec^{R}\mS$.
If $\bet\prec^{R}\mT$ and $\alp\prec^{R}\mS$ with $\mT<\mS$, then
In other words, $L(\mT)<L(\mS)$ for layers $L(\mS)$.
Moreover if $\eta\not\in\bigcup_{\mS\in SSt}L(\mS)$ and $\eta\in\Psi$,
then either $\eta\prec\Ome$ or $\eta\prec\mI_{N}$.

Let $\bet,\alp\in OT(\mI_{N})\cap\mI_{N}$ be strongly critical numbers.
$\bet<\alp$ iff one of the following cases holds:

$\bet=\psi_{\pi}(b)$, $\alp=\psi_{\kappa}(a)$,
$\pi=\kap\in\{\Ome,\mI_{N}\}\cup\{\sig\in OT(\mI_{N}): \exi\rho(\sig=\mI_{N}[\rho])\}$ and

$\bet=\Ome$ and $\Ome\neq\alp\neq\psi_{\Ome}(a)$.

$\mS^{\dagger\vec{i}}<\mT^{\dagger\vec{j}}$ iff $(\mS)*\vec{i}<_{lx}(\mT)*\vec{j}$
for $\mS,\mT\in \{\Ome\}\cup LSt$, where
$\vec{i}=(i_{0}, i_{1},\ldots,i_{n})<_{lx}(j_{0},j_{1},\ldots,j_{m})=\vec{j}$ iff
either $\exi k\leq\min\{n,m\}(\fal p<k(i_{p}=j_{p}) \spand i_{k}<j_{k})$ or $n<m\spand \fal p\leq n(i_{p}=j_{p})$.

* There is a $\mS\in SSt$ such that
$\alp\prec^{R}\mS>\bet\in LSt_{N}$.

* There is a $\mT\in SSt$ such that

There are $\mT,\mS\in SSt$ such that
$\bet\prec^{R}\mT$ and $\alp\prec^{R}\mS$ with $\mT<\mS$.

There is a $\mS\in SSt$ such that
$\bet,\alp\prec^{R}\mS$ and one of the following holds:

$\bet=\psi_{\pi}^{f}(b)$, $\alp=\psi_{\kappa}^{g}(a)$, and there is a
$\rho\preceq^{R}\mS$ such that
$\kap,\pi\preceq\rho$ and
one of the following holds: let
$\Lam$ be the base of finite functions $f,g$.

$\pi\leq \alp$.

$b<a$, $\bet<\kappa$, and

$b>a$ and $b\leq K_{\bet}(SC_{\Lam}(g)\cup\{\kappa,a\})$.

$b=a$, $\kappa<\pi$, and $b\leq K_{\bet}(\kap)$.

$b=a$, $\pi=\kappa$, $K_{\alp}(SC_{\Lam}(f))<a$, and

$b=a$, $\pi=\kappa$, and
$b\leq K_{\bet}(SC_{\Lam}(g))$.

There are $\mI_{N}[\rho]\prec^{R}\mS$,
$c,d$ and $\vec{i},\vec{j}$ such that $\bet\preceq^{R}(\psi_{\mI_{N}[\rho]}(d))^{\dagger \vec{i}}$,
$\alp\preceq^{R}(\psi_{\mI_{N}[\rho]}(c))^{\dagger \vec{j}}$
and $\psi_{\mI_{N}[\rho]}(d)<\psi_{\mI_{N}[\rho]}(c)$.

There are $\vec{i}$, $\mI_{N}[\rho]$ such that
$\bet\preceq^{R}\mT^{\dagger \vec{i}}[\rho/\mT]$ and $\alp\preceq^{R}\mI_{N}[\rho]$.

There are $\rho\prec\mT\preceq^{R}\mS$,
$\sig,\tau\prec\mU=\mT^{\dagger \vec{i}}[\rho/\mT]$, $\vec{k}$ and $\vec{l}$ such that
$\tau<\sig$, $(\tau,\sig)\neq(\bet,\alp)$,
$\alp=\sig \lor \alp\preceq^{R}\mI_{N}[\sig]\lor \alp\preceq^{R}\mU^{\dagger \vec{k}}[\sig/\mU]$,
$\bet=\tau\lor \bet\preceq^{R}\mI_{N}[\tau]\lor \bet\preceq^{R}\mU^{\dagger \vec{l}}[\tau/\mU]$.

$(OT(\mI_{N}),<)$ is a computable linear order.
each of $\alpha<\beta$ and $\alpha=\beta$ is decidable for $\alpha,\beta\in OT(\mI_{N})$,
and $\alpha\in OT(\mI_{N})$ is decidable for terms $\alpha$
over symbols $\{0,\Ome,\mI_{N}, +,\varphi, \psi\}$, $\{ {}^{\dagger i}:0<i\leq N\}$ and $*_{0}[*_{1}/*_{2}]$.

In particular the order type of the initial segment $\{\alpha\in OT(\mI_{N}): \alpha<\Omega\}$
is less than $\omega_{1}^{CK}$ if it is well-founded.

In what follows by ordinals we mean ordinal terms in $OT(\mI_{N})$.
$\ell\alp$ denotes the length of ordinal terms $\alp$, which means the number of
occurrences of symbols in $\alp$.

$St_{i+1}\subset LSt_{i}$ holds in $OT(\mI_{N})$ in the sense that
if $\mS\in St_{i+1}=SSt_{i+1}\cup LSt_{i+1}$ and $\alp<\mS$,
then $\alp^{\dagger i}<\mS$.
This is seen from Proposition <ref> and Definition <ref>.

$SC_{\mI_{N}}(m(\rho))\subset M_{\rho}$.
If $\rho=\psi_{\mS}^{f}(a)$ with an $\mS\in SSt$, then we obtain
$f=m(\rho)$, $a=\mathtt{ p}_{0}(\rho)$,
$SC_{\mI_{N}}(f)\subset \mathcal{H}_{a}(\alp)=M_{\rho}$ by
Definition <ref>.<ref>.
Otherwise $SC_{\mI_{N}}(m(\rho))\subset M_{\rho}$ follows from
in Definition <ref>.<ref>.

An ordinal term $\sig\in OT(\mI_{N})$ is said to be regular if
$\psi_{\sig}^{f}(a)$ is in $OT(\mI_{N})$ for some $f$ and $a$.
$Reg=St_{0}$ denotes the set of regular terms.
$Reg\cup LSt^{M}=SSt^{M}\cup\{\mI_{N}[\rho]:\exi\mS\in SSt^{M}(\rho\prec\mS)\}\cup\{\Ome,\mI_{N}\}$.
We see that for each $\alp\in\Psi$, there exists a $\kap\in Reg_{0}:=(Reg\setm\Psi)$ such that
Such a $\kap$ is either in $\{\Ome,\mI_{N}\}$ or
one of the form $\mI_{N}[\rho]$, $\rho^{\dagger\vec{i}}$
or $\mS^{\dagger\vec{i}}[\rho/\mS]$ with a non-empty $\vec{i}$.

Let $\psi_{\pi}^{f}(a)<\psi_{\kap}^{g}(b)<\pi<\kap$ and $\pi\preceq\rho$ and $\kap\preceq\tau$
with $\{\rho,\tau\}\subset Reg_{0}$.
Then $\rho=\tau$.
From Definition <ref> we see that the only possible case is
Definition <ref>(<ref>).

For $\rho\prec\mS$ and $\mS\in SSt$,
$\{\alpha[\rho/\mS]:\alpha\in M_{\rho}\}$ is a transitive collapse of $M_{\rho}$ in the following sense.
Let $\{\alpha,\beta,\gamma\}\subset M_{\rho}$.

$\bet\prec^{R}\alp \Lrarw \bet[\rho/\mS]\prec^{R}\alp[\rho/\mS]$.

$\mathbb{S}<\gam \Rightarrow
\left(
\Lrarw
\right)$.

$OT(\mI_{N})\cap\alpha[\rho/\mS]=\{\gamma[\rho/\mS]:\gamma\in M_{\rho}\cap\alpha\}$.

We show Lemmas <ref>.<ref>-
by induction on the sum $2^{\ell\alpha}+2^{\ell\beta}$ of lengths for
$\alpha,\beta\in M_{\rho}$.

We see easily that
$\mathbb{S}>\Gamma(\mathbb{I}_{N}[\rho])>\alpha[\rho/\mS]>\rho$ when
Also $\alpha[\rho/\mS]\leq\alpha$.

<ref>.<ref> and <ref>.<ref> are seen by IH.

Let $k(\psi^{g}_{\kappa}(a))=SC_{\mI_{N}}(g)\cup\{\kap,a\}$.
Let $\mathbb{S}<\beta=\psi^{f}_{\pi}(b)<\psi^{g}_{\kappa}(a)=\alpha$ with
$k(\bet,\alp)\subset M_{\rho}$.
From IH with Definition <ref>
we see that
Other cases are seen from IH.

Suppose $K_{\gam}(\bet)<\alp$
for $\mathbb{S}<\gam$.
Then $K_{\gam[\rho/\mS]}(\bet[\rho/\mS])<\alp[\rho/\mS]$
is seen from
IH and Lemma <ref>.<ref>
using the fact $\gamma[\rho/\mS]>\rho$.

$\beta\in OT(\mI_{N})\cap\alpha[\rho/\mS]$ for $\alpha\in M_{\rho}$.
We show by induction on $\ell\beta$ that there exists a
$\gamma\in M_{\rho}$
such that $\beta=\gamma[\rho/\mS]$.
If $\beta<\rho$, then $\beta[\rho/\mS]=\beta$．
Also $\rho=\mathbb{S}[\rho/\mS]$ and $\mathbb{I}_{N}[\rho]=(\mathbb{I}_{N})[\rho/\mathbb{S}]$.
Let $\Gam_{\mathbb{I}_{N}[\rho]+1}>\alp[\rho/\mS]>\beta>\rho$.
We can assume $\mathbb{I}_{N}[\rho]>\beta>\rho$ by IH.

If $\bet=\mathbb{I}_{N}[\tau]$, then $\mathbb{I}_{N}[\tau]>\tau$.
Pick a $\kap\in M_{\rho}$ such that $\kap[\rho/\mS]=\tau$.
Then $\bet=(\mI_{N}[\kap])[\rho/\mS]$.

If $\bet=\tau^{\dagger \vec{i}}$, then $\tau^{\dagger \vec{i}}>\tau$.
Pick a $\kap\in M_{\rho}$ such that $\kap[\rho/\mS]=\tau$.
Then $\bet=(\kap^{\dagger \vec{i}})[\rho/\mS]$.

If $\bet=\mT_{1}^{\dagger\vec{j}}[\tau_{1}/\mT_{1}]$, then
Pick a $\tau\in M_{\rho}$ such that $\tau[\rho/\mS]=\tau_{1}$.
Then for $\tau\prec \mT\in SSt^{M}$, we obtain

Finally let $\beta=\psi^{f}_{\pi}(b)$ with
$b<\Gam_{\mI_{N}[\rho]+1}$ and
$f:\Lam\to\vphi_{\Lam}(0)$ for
$\pi\preceq\sig^{\dagger \vec{k}}$ with an $\vec{k}\neq\emptyset$.
We have $\bet\prec\sig^{\dagger \vec{k}}$,
$\rho<\bet<\mI_{N}[\rho]$, and $\rho\prec\mS$.
Definition <ref>
we obtain $\sig\neq\mS$.
Suppose $\bet<\mS<\sig^{\dagger \vec{k}}$. Then $\alp<\rho$ by
Definition <ref>.
Hence we can assume $\sig^{\dagger \vec{k}}<\mS$.
Then we obtain
$\rho<\sig^{\dagger k}<\mI_{N}[\rho]$.
Hence $\sig\prec^{R}\mI_{N}[\rho]$ or $\sig\prec^{R}\mS^{\dagger \vec{i}}[\rho/\mS]$ for an $\vec{i}$.
By IH with $\pi\leq\sig^{\dagger \vec{k}}$ there are
$\{c,\kap,\lam\}\subset M_{\rho}$ and
such that $c[\rho/\mS]=b$, $\kap[\rho/\mS]=\pi$,
$SC_{\mI_{N}}(g)\subset M_{\rho}$,
$g[\rho/\mS]=f$ in the sense that
$({\rm supp}(g))[\rho/\mS]={\rm supp}(f)$ and
$(g(d))[\rho/\mS]=f(d[\rho/\mS])$ for every $d\in{\rm supp}(g)$.
Let $\gam=\psi_{\kap}^{g}(c)\in M_{\rho}$.
and $k(\gam)\subset\mathcal{H}_{c}(\gam)$.

Other cases are seen from IH.

Let $\alp=\psi_{\Ome}(a)$ with $a\in\calh_{a}(\alp)$.
Then $\calh_{a}(\alp)\cap\Ome\subset\alp$.

Let $\alp=\psi_{\mI_{N}}(a)$ with $a\in\calh_{a}(\alp)$.
Then $\calh_{a}(\alp)\cap\mI_{N}\subset\alp$.

Let $\mS\in SSt$, and
$\alp=\psi_{\kap}^{f}(a)<\kap$ with
$\kap\preceq\mS$ and
$\{\kap,a\}\cup SC_{\mI_{N}}(f)\subset\calh_{a}(\alp)$.
Then $\calh_{a}(\alp)\cap\kap\subset\alp$.
We see $\bet\in\calh_{a}(\alp)\cap\Ome \Rarw \bet<\alp=\psi_{\Ome}(a)$
by induction on the lengths $\ell\bet$ of $\bet$.
<ref>.<ref> and <ref>.<ref>
are seen similarly using the fact
$\rho<\alp\Rarw \mI_{N}[\rho]<\alp$ for $\alp\in\{\psi_{\mI_{N}}(a),\psi_{\kap}^{f}(a)\}$.

Let $\mS\in SSt$, and
$\rho=\psi_{\kap}^{f}(a)<\kap$ with
$\kap\preceq\mS$ and
$\calh_{\gam}(\kap)\cap\mS\subset\kap$ for $\gam\leq a$.
Then $\calh_{\gam}(\rho)\cap\mS\subset\rho$.
If $\kappa=\mathbb{S}$, then
by $\gamma\leq a$ and Lemma <ref>.<ref>.
Let $\kappa=\psi_{\pi}^{g}(b)<\mathbb{S}$.
We have $\kappa\in\mathcal{H}_{a}(\rho)$ by (<ref>),
and hence $b<a$ by $\mS>\kappa>\rho$.
We obtain
$\gamma\leq a$ with Lemma <ref>.<ref>
\mathcal{H}_{a}(\rho)\cap\kappa\subset\rho$.

Let $\rho\in\Psi_{\mS}$ for an $\mS\in SSt$.

$\mathcal{H}_{\gamma}(M_{\rho})\subset M_{\rho}$
if $\gam\leq\mathtt{ p}_{0}(\rho)$.

$M_{\rho}\cap\mS=\rho$ and $\rho\not\in M_{\rho}$.

If $\sig<\rho$ and $\mathtt{ p}_{0}(\sig)\leq \mathtt{ p}_{0}(\rho)$, then
$M_{\sig}\subset M_{\rho}$.
Let $\gam\leq b=\mathtt{ p}_{0}(\rho)$.
We show $\alp\in M_{\rho}=\calh_{b}(\rho)$ by induction on $\ell\alp$ for
$\alp\in \calh_{\gam}(M_{\rho})$.
\mathcal{H}_{\gamma}(M_{\rho})\cap\mathcal{H}_{a}(\alpha)$ be such that
$a<\gam\leq b$ and
IH yields $k(\alp)\subset M_{\rho}$.
We obtain $\alp\in \calh_{b}(\rho)$.

Other cases are seen from IH as in [2].

(Mostowski uncollapsing)

Let $\alpha$ be an ordinal term and $\rho\prec\mS$ with
$\mS\in SSt$.
If there exists a $\beta\in M_{\rho}$ such that
$\alpha=\beta[\rho/\mS]$, then $\alpha[\rho/\mS]^{-1}:=\beta$.
Otherwise $\alpha[\rho/\mS]^{-1}:=0$.
$X[\rho/\mS]^{-1}:=\{\alpha[\rho/\mS]^{-1}:\alpha\in X\}$ for a set $X$ of ordinal terms.

We see that
ordinal terms $\rho$ and $\beta\in M_{\rho}$
with $\rho\leq\alpha=\beta[\rho/\mS]< \Gam_{\mathbb{I}_{N}[\rho/\mS]+1}$
are uniquely determined from $\alp$, when
such $\beta$ and $\rho$ exist.

§.§ Stepping-down

The following Definitions <ref> and <ref> are needed in subsection <ref>.

$s(f)=\max(\{0\}\cup{\rm supp}(f))$ for finite function $f$, and

Let $\Lambda<\mI_{N}$ be a strongly critical number, which is a base for $\tilde{\tht}$-function.
Let $f:\Lambda\to\vphi_{\Lambda}(0)$ be a non-empty and irreducible finite function.
Then $f$ is said to be special if there exists an ordinal $\alpha$
such that $f(s(f))=\alpha+\Lambda$.
For a special finite function $f$, $f^{\prime}$ denotes a finite function such that
${\rm supp}(f^{\prime})={\rm supp}(f)$,
$f^{\prime}(c)=f(c)$ for $c\neq s(f)$, and
$f^{\prime}(s(f))=\alpha$ with $f(s(f))=\alpha+\Lambda$.

Let $f,g$ be special finite functions with base $\Lambda$, and $\rho\in\Psi_{\mS}$
for a $\mS\in SSt$.
$\tilde{\tht}$ denotes the function $\tilde{\tht}_{b}(\xi;\Lambda)$
in Definition <ref> with base $\Lambda$.

ordinals $a\leq\Lambda$, $b< s(g)$,
let us define a special finite function $h=h^{b}(g;a)$ and an ordinal $\alpha^{b}(g)$
as follows.
$s(h)=b$, and
To define $h(b)$,
let $\{b=b_{0}<b_{1}<\cdots<b_{n}=s(g)\}=\{b,s(g)\}\cup\left((b,s(g))\cap {\rm supp}(g)\right)$.
Define recursively ordinals $\alpha_{i}$ by
$\alpha_{n}=\alpha+a$ with $g(s(g))=\alpha+\Lambda$.
$\alpha_{i}=g(b_{i})+\tilde{\theta}_{c_{i}}(\alpha_{i+1})$ for
Finally let $h(b)=\alpha_{0}+\Lambda$,
and $\alpha^{b}(g)=tl((h^{b}(g;\Lambda))^{\prime}(b))=\tilde{\theta}_{c_{0}}(\alpha_{1})$, where
$\alpha_{1}$ is defined for $a=\Lambda$.

For $c\leq\min\{s(f),s(g)\}$, let
$f \triangleleft_{c} g:\Leftrightarrow \forall b<c(\alpha^{b}(f)<\alpha^{b}(g))$.

$f_{b}*g^{b}$ denotes a special function $h$ such that
${\rm supp}(h)={\rm supp}(f_{b})\cup{\rm supp}(g^{b})$,
$h^{\prime}(c)=f^{\prime}(c)$ for $c<b$, and
$h^{\prime}(c)=g^{\prime}(c)$ for $c\geq b$.

For a finite function $k$,
$f+k$ denotes a special function $h$ such that
${\rm supp}(h)={\rm supp}(f)\cup{\rm supp}(k)$ and

For $d\leq s(\rho)$,
$\sigma\in H_{\rho}(d,f)$ iff there is a finite function $k$ such that
$\forall x\in{\rm supp}(k)[0<k(x)<\alpha^{x}(m(\rho))]$, and

The following Proposition <ref> is seen as in [2].

Let $k$ be a finite function,
$f, g$ special finite functions such that
$f_{d}=g_{d}$ and
$f<^{d}g^{\prime}(d)$ for a $d\in{\rm supp}(g)$, and
$\rho\in\Psi_{\mS}$ with $g=m(\rho)$.

For $b<d$ and $a<\Lambda$,
$f_{b}=(h^{b}(g;a))_{b}$ and

For $d\leq c<s(f)$ and $a\leq\Lambda$,

Let $b\leq e<d$,
$a_{0}<a<\Lambda$, and
$h_{b}=(h^{b}(g;a))_{b}$ and

If $m(\kappa)\triangleleft_{b}g$ and $\sigma\in H_{\kappa}(\min\{b,d\},f)$, then
$\sigma\in H_{\rho}(d,f)$.

If $m(\kappa)\triangleleft_{b}g$, $\sigma\in H_{\kappa}(b,h)$,
$b\leq e$,
$h\triangleleft_{e}g$ and $h_{e}=g_{e}$, then

§ OPERATOR CONTROLLED DERIVATIONS

We prove Theorem <ref> assuming $(OT(\mI_{N}),<)$ is a well ordering.
Operator controlled derivations are introduced by W. Buchholz[6], which we follow.
In this section except otherwise stated,
$\alp,\bet,\gam,\ldots,a,b,c,d,\ldots$ and $\xi,\zeta,\nu,\mu,\ldots$ range over ordinals in $OT(\mI_{N})$,
$f,g,h,\ldots$ range over finite functions.

§.§ Classes of sentences

Following Buchholz[6] let us introduce a language for ramified set theory $RS$.

$RS$-terms and their levels are inductively defined.

* For each $\alp\in OT(\mI_{N})\cap \mI_{N}$, $L_{\alp}$ is an $RS$-term of level $\alp$.

* Let $\phi(x,y_{1},\ldots,y_{n})$ is a set-theoretic formula in the language $\{\in\}$, and $a_{1},\ldots,a_{n}$ are
$RS$-terms of levels$<\! \alp\in OT(\mI_{N})\cap\mI_{N}$.

$[x\in L_{\alp}:\phi^{L_{\alp}}(x,a_{1},\ldots,a_{n})]$
is an $RS$-term of level $\alp$.

Let $ON(x)$ be a $\Del_{0}$-formula saying that
'$x$ is a transitive set such that
$\in$ is a linear order on $x$'.
For $\alp\in OT(\mI_{N})\cap \mI_{N}$,
an $RS$-term $\bar{\alp}\equiv [x\in L_{\alp}: ON(x)]$ denotes the ordinal $\alp$.

* $|u|$ denotes the level of $RS$-terms $u$, and $Tm(\alp)$ the set of $RS$-terms of level$<\alp\in OT(\mI_{N})\cap(\mI_{N}+1)$.
$Tm=Tm(\mI_{N})$ is then the set of $RS$-terms, which are denoted by $u,v,w,\ldots$

* $RS$-formulas
are constructed from literals
$u\in v, u\not\in v$
$St_{i}(u), \lnot St_{i}(u)$
for $0<i\leq N$
by propositional connectives $\lor,\land$, bounded quantifiers $\exi x\in u, \fal x\in u$ and
unbounded quantifiers $\exi x,\fal x$.
Unbounded quantifiers $\exists x,\forall x$ are denoted by $\exists x\in L_{\mI_{N}},\forall x\in L_{\mI_{N}}$, resp.

It is convenient for us not to restrict propositional connectives $\lor,\land$ to binary ones.
Specifically when $A_{i}$ are $RS$-formulas for $i<n<\ome$,
$A_{0}\lor\cdots\lor A_{n-1}$ and $A_{0}\land\cdots\land A_{n-1}$ are $RS$-formulas.
Even when $n=1$, $A_{0}\lor\cdots\lor A_{0}$ is understood to be different from the formula $A_{0}$.
For $\Gam=\{A_{i}:i<n\}$ we write
$\bigvee\Gam\equiv(A_{0}\lor\cdots\lor A_{n-1})$ and
$\bigwedge\Gam\equiv(A_{0}\land\cdots\land A_{n-1})$.

* For $RS$-terms and $RS$-formulas $\iota$,
${\sf k}(\iota)$ denotes the set of ordinal terms $\alp$ such that the constant $L_{\alp}$ occurs in $\iota$, and

* $\mathcal{L}_{i}=\{\in\}\cup\{St_{j}:0<j<i\}$.

* $\Del_{0}(\mathcal{L}_{i})$-formulas, $\Sig_{1}(\mathcal{L}_{i})$-formulas and $\Sig(\mathcal{L}_{i})$-formulas are defined as in [4].
Specifically if $\psi$ is a $\Sig(\mathcal{L}_{i})$-formula, then so is the formula $\fal y\in z\, \psi$.
$\tht^{(a)}$ denotes a $\Del_{0}(\mathcal{L}_{i})$-formula obtained from a $\Sig(\mathcal{L}_{i})$-formula $\tht$
by restricting each unbounded existential quantifier to $a$.

* For a $\Sig_{1}(\mathcal{L}_{i})$-formula $\psi(x_{1},\ldots,x_{m})$
$u_{1},\ldots,u_{m}\in Tm(\kap)$ with $\kap\leq\mI_{N}$,
is a $\Sig_{1}(\mathcal{L}_{i}:\kap)$-formula.
$\Del_{0}(\mathcal{L}_{i}:\kap)$-formulas and $\Sig(\mathcal{L}_{i}:\kap)$-formulas are defined similarly

* For $\tht\equiv\psi^{(L_{\kap})}(u_{1},\ldots,u_{m})\in\Sig(\mathcal{L}_{i}:\kap)$
and $\lam<\kap$,
$\tht^{(\lam,\kap)}:\equiv \psi^{(L_{\lam})}(u_{1},\ldots,u_{m})$.

In what follows we need to consider sentences.
Sentences are denoted $A,C$ possibly with indices.

For each sentence $A$, either a disjunction is assigned as $A\simeq\bigvee(A_{\iota})_{\iota\in J}$, or
a conjunction is assigned as $A\simeq\bigwedge(A_{\iota})_{\iota\in J}$.
In the former case $A$ is said to be a $\bigvee$-formula, and in the latter
$A$ is a $\bigwedge$-formula.

For $v,u\in Tm(\mI_{N})$ with $|v|<|u|$, let

\[
(v\veps u) :\equiv
\left\{
\begin{array}{ll}
A(v) & \mbox{{\rm if }} u\equiv[x\in L_{\alp}: A(x)]
\\
v\not\in L_{0} & \mbox{{\rm if }} u\equiv L_{\alp}
\end{array}
\right.
\]

$(u=v):\equiv(\fal x\in u(x\in v)\land \fal x\in v(x\in u))$.

* When $A\simeq\bigvee(A_{\iota})_{\iota\in J}$,
let $\lnot A\simeq\bigwedge(A_{\iota})_{\iota\in J}$.

$(v\in u)  :\simeq  \bigvee(A_{w})_{w\in J}$
for $A_{w}:\equiv ((w\veps u)\land (\fal x\in w(x\in v)) \land (\fal x\in v(x\in w)))$
and $J=Tm(|u|)$.

$(A_{0}\lor\cdots\lor A_{n-1}):\simeq\bigvee(A_{\iota})_{\iota\in J}$

For $u\in Tm(\mI_{N})\cup\{L_{\mI_{N}}\}$,
$\exists x\in u\, A(x):\simeq\bigvee(A_{v})_{v\in J}$
$A_{v}:\equiv ((v\veps u)\land A(v))$ and

$St_{i}(a):\simeq \bigvee( (\fal x\in \iota(x\in a)) \land (\fal x\in a(x\in \iota)))_{\iota\in J_{i}}$
$J_{i}=\{\bar{\alp}: \alp\in\bigcup_{i\leq j\leq N}\left( St_{j}\cap(|a|+1) \right)\}$, where
$\bar{\alp}=[x\in L_{\alp}: ON(x)]$, and
in the LHS, $St_{i}$ denotes the predicate symbol in the language $\mathcal{L}_{N}$, while
$St_{j}\subset OT(\mI_{N})$ in the definition of $J_{i}$.

The rank $\mbox{{\rm rk}}(\iota)$ of sentences or terms $\iota$
is defined as in [2] so that the following Proposition <ref> holds.

Let $A$ be a sentence with
$A\simeq\bigvee(A_{\iota})_{\iota\in J}$ or $A\simeq\bigwedge(A_{\iota})_{\iota\in J}$.

$\mbox{{\rm rk}}(A)<\mI_{N}+\omega$.

$\rk(\bar{0})<\ome$ and $\rk(\bar{\alp})=\ome\alp$ for $\alp>0$.

$\ome |u|\leq \rk(u)\in\{\ome |u|+i: i\in\ome\}$, and
$|A|\leq \mbox{{\rm rk}}(A)\in\{\omega |A|+i  : i\in\omega\}$.

For $v\in Tm(|u|)$, $\rk(v\veps u)\leq \rk(u)$.

$\forall\iota\in J(\mbox{{\rm rk}}(A_{\iota})<\mbox{{\rm rk}}(A))$.

$\rk(\bigvee\Gam)=\max\{\rk(A): A\in\Gam\}+1$.

Let $\rho\prec\mS\in SSt_{i}$ for an $0<i\leq N$.
$\iota^{[\rho/\mS]}$ is defined for $RS$-terms and $RS$-formulas $\iota$.
$\iota^{[\rho/\mS]}$ denotes the result of replacing each unbounded quantifier
$Qx$ by $Qx\in L_{\mI_{N}[\rho]}$,
and each ordinal term $\alp\in {\sf k}(\iota)$
by $\alp[\rho/\mS]$ for the Mostowski collapse in
Definition <ref>.
The following Propositions <ref>, <ref>
and <ref> are seen from Lemma <ref>.

Let $\rho\prec\mS$.

Let $v$ be an $RS$-term with $\sfk(v)\subset M_{\rho}$,
and $\alp=|v|$.
$v^{[\rho/\mS]}$ is an $RS$-term of level $\alp[\rho/\mS]$,
$\left| v^{[\rho/\mS]} \right|=\alp[\rho/\mS]$ and

Let $\alp\leq\mI_{N}$ be such that $\alp\in M_{\rho}$. Then
\left(Tm(\alp)\right)^{[\rho/\mS]}
\{v^{[\rho/\mS]}: v\in Tm(\alp), \sfk(v)\subset M_{\rho}\}
= Tm(\alp[\rho/\mS])

Let $A$ be an $RS$-formula with $\sfk(A)\subset M_{\rho}$
and $\rho\prec\mS$.
Then $A^{[\rho/\mS]}$ is an $RS$-formula such that
$\sfk(A^{[\rho/\mS]})\subset\{\alp[\rho/\mS]: \alp\in\sfk(A)\}\cup\{\mI_{N}[\rho]\}$.

For $RS$-formulas $A$, let
$A\simeq \bigvee(A_{\iota})_{\iota\in J}$ and assume
$\sfk(A)\subset M_{\rho}$ with $\rho\prec\mS$.
$A^{[\rho/\mS]}\simeq \bigvee\left((A_{\iota})^{[\rho/\mS]}\right)_{\iota\in [\rho]J}$
for $[\rho]J=\{\iota\in J : \sfk(\iota)\subset M_{\rho}\}$.

Let $\sfk(\iota)\subset M_{\rho}$ with $\rho\prec\mS$.

§.§ A preview of elimination procedures of stable ordinals

Let us explain briefly our elimination procedures of stable ordinals in this section and
section <ref>.
In the previous paper [2], we analyzed an axiom $L_{\mS}\prec_{\Sig_{1}}L$ proof-theoretically.
The axiom is a schema
$\exi x\, B(x,v) \land v\in L_{\mS} \to \exi x\in L_{\mS}\, B(x,v)$
for $\Del_{0}$-formulas $B$.
The schema says that
$\mS$ `reflects' $\Pi_{\mS^{+}}$-formulas in transfinite levels.
In order to analyze the reflections,
Mahlo classes $Mh^{a}_{i,c}(\xi)$ are introduced in Definition <ref>.<ref>.
$\pi\in Mh^{a}_{i,c}(\xi)$
reflects every fact
$\pi\in Mh_{i,0}^{a}(g_{c})=\bigcap\{Mh^{a}_{i,d}(g(d)): c>d\in {\rm supp}(g)\}$
on the ordinals $\pi\in Mh_{i,c}^{a}(\xi)$ in lower level,
down to
`smaller' Mahlo classes $Mh_{i,c}^{a}(f)=\bigcap\{Mh^{a}_{i,d}(f(d)): c\leq d\in {\rm supp}(f)\}$.

This apparatus would suffice to analyze reflections in transfinite levels.
We need another for the axiom $L_{\mS}\prec_{\Sig_{1}}L$, i.e.,
a (formal) Mostowski collapsing:
Assume that $B(u,v)$ with $v\in L_{\mS}$ for a $\Del_{0}$-formula $B$.
We need to find a substitute $u^{\prime}\in L_{\mS}$ for $u\in L$, i.e.,
For simplicity let us assume that $v=\bet<\mS$ and $u=\alp$ are ordinals.
We may assume that $\alp\geq\mS$.
Let $\rho<\mS$ be an ordinal, which is bigger than every ordinal$<\mS$
occurring in the `context' of $B(\alp,\bet)$.
This means that if an ordinal $\del<\mS$ occurs in a `relevant' branch of a
derivation of $B(\alp,\bet)$, $\del<\rho$ holds.
Then we can define a Mostwosiki collapsing $\alp\mapsto\alp[\rho/\mS]$ for
ordinal terms $\alp$ such that
$\bet[\rho/\mS]=\bet$ for each relevant $\bet<\mS$ and $\mS[\rho/\mS]=\rho$, cf. Definition <ref>.
Then we see that $B(\alp[\rho/\mS],\bet)$ holds.

Let $M_{\rho}$ denote a set of ordinal terms $\alp$ such that
every subterm $\bet<\mS$ of $\alp$ is smaller than $\rho$.
It is shown in Lemma <ref> that
$\mathcal{H}_{\gamma}(M_{\rho})\subset M_{\rho}$
if $\mathcal{H}_{\gamma}(\rho)\cap\mathbb{S}\subset\rho$.
Let $\calh_{\gam}[\Tht]\vdash^{a}_{c}\Gamma$, and
assume that $\{\gam,a,c\}\cup\sfk(\Gam)\subset\calh_{\gam}[\Tht]$
Moreover let us assume that $\Tht\subset M_{\rho}$ holds.
Then we obtain
$\{\gam,a,c\}\cup\sfk(\Gam)\subset\calh_{\gam}[\Tht]\subset\calh_{\gam}(M_{\rho})\subset M_{\rho}$.
This means that $\sfk(\Gam)\subset M_{\rho}$ holds
as long as $\Tht\subset M_{\rho}$ holds, i.e., as long as
we are concerned with branches for $\sfk(\iota)\subset M_{\rho}$
in, e.g., inferences $(\bigwedge)$: $A\simeq\bigwedge(A_{\iota})_{\iota\in J}$

\[
\infer[(\bigwedge)]{\calh_{\gam}[\Tht]\vdash^{a}_{c}\Gam,A}
\{
\calh_{\gam}[\Tht]\vdash^{a_{0}}_{c}\Gam,A, A_{\iota}
\}_{\iota\in J}
\leadsto
\infer[(\bigwedge)]{\calh_{\gam}[\Tht]\vdash^{a}_{c}\Gam,A}
\{
\calh_{\gam}[\Tht]\vdash^{a_{0}}_{c}\Gam,A, A_{\iota}
\}_{\iota\in J, \sfk(\iota)\subset M_{\rho}}
\]

and dually $\sfk(\iota)\subset M_{\rho}$ for a minor formula $A_{\iota}$
of a $(\bigvee)$ with the main formula $A\simeq\bigvee(A_{\iota})_{\iota\in J}$,
provided that
The proviso means that $\gam_{1}\geq\gam$ when $\rho=\psi_{\mS}^{f}(\gam_{1})$.
Such a $\rho\in\calh_{\gam}[\Tht]$ only when $\rho\in\Tht$.
Let us try to replace the inferences for the stability of $\mS$

\[
\infer[({\rm stbl})]{(\mathcal{H}_{\gamma},\Theta
\vdash
\Gamma
\Gamma, B(u)
\{
\vdash
\Gamma, \lnot B(u)^{[\sigma/\mathbb{S}]}
\}_{\Theta\subset M_{\sigma}}
\]

by inferences for reflection of $\rho$ with $\Tht\subset M_{\rho}$:
If $B(u)^{[\rho/\mS]}$ holds, then $B(u)^{[\sig/\mS]}$ holds for some $\sig<\rho$.

\[
\hspace{-5mm}
\infer[({\rm rfl})]{(\mathcal{H}_{\gamma},\Theta\cup\{\rho\}
\vdash
\Gamma^{[\rho/\mS]}
\Gamma^{[\rho/\mS]}, B(u)^{[\rho/\mS]}
\{
\vdash
\Gamma^{[\rho/\mS]}, \lnot B(u)^{[\sigma/\mathbb{S}]}
\}_{\Theta\subset M_{\sigma},\sig<\rho}
\]

In analyzing the inferences for reflections in transfinite levels,
formulas $\Gam^{[\rho/\mS]}$ are replaced by $\Gam^{[\sig/\mS]}$.
This means that $\alp[\sig/\mS]$ is substituted for each $\alp[\rho/\mS]$.
Namely a composition of uncollapsing and collapsing $\alp[\rho/\mS]\mapsto\alp\mapsto\alp[\sig/\mS]$
Hence we need $\alp\in M_{\sig}\subsetneq M_{\rho}$ for $\sig<\rho$.
However we have $\rho\not\in M_{\sig}$, and we cannot replace $[\rho/\mS]$ by $[\sig/\mS]$
in the upper part of $\Gamma^{[\rho/\mS]}, B(u)^{[\rho/\mS]}$.
The schema seems to be broken.

Instead of an explicit collapsing ${}^{[\rho/\mS]}$, formulas could put on caps $\rho,\sig,\ldots$
in such a way that $\sfk(A^{(\sig)})=\sfk(A)$.
This means that the cap $\sig$ does not `occur' in a capped formula $A^{(\sig)}$.
If we choose an ordinal $\gam_{0}$ big enough (depending on a given finite proof figure),
every ordinal `occurring' in derivations (including the subscript $\gam\leq\gam_{0}$ in
the operators $\calh_{\gam}$)
is in $\calh_{\gam_{0}}(\emptyset)$
for the ordinal $\gam_{0}$, while
each cap $\rho$ exceeds the threshold $\gam_{0}$ in the sense that
Then every ordinal `occurring' in derivations is in the domain $M_{\rho}$
of the Mostowski collapsing $\alp\mapsto\alp[\rho/\mS]$.

The ordinal $\gam_{0}$ is a threshold, which means that
every ordinal occurring in derivations is in $\calh_{\gam_{0}}(0)$ and
the subscript $\gam\leq\gam_{0}$ in $\calh_{\gam}$, while
each $\rho\in{\tt Q}$ exceeds $\gam_{0}$ in such a way that
${\tt p}_{0}(\rho)\geq\gam_{0}$.
This ensures us that $\calh_{\gam}(M_{\rho})\subset M_{\rho}$.
In the end, inferences for reflections are removed in [2]
by moving outside $\calh_{\gam_{0}}(0)$.

Now we have several (successor) stable ordinals $\mS,\mT,\ldots\in dom({\tt Q})$
for a finite collection $dom(\mathtt{Q})$ of successor stable ordinals, cf. Definition <ref>.<ref>.
Inferences for stability and their children for reflections are eliminated
first for bigger $\mS>\mT$, and then smaller ones.
Therefore we need an assignment $dom({\tt Q})\ni\mS\mapsto\gam_{\mS}^{{\tt Q}}$ for
thresholds so that
$\gam_{\mS}^{{\tt Q}}<\gam_{\mT}^{{\tt Q}}$ if $\mS>\mT$ in Definition <ref>.<ref>.

We define two derivability relations
$(\mathcal{H}_{\gamma},\Theta; \mathtt{Q})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$
and $(\calh_{\gam},\Tht,\mathtt{Q})\vdash^{a}_{c,d,e}\Gam$
in in subsections <ref> and <ref>, resp.
In the former
$\mathtt{Q}(\mS)$ is a finite set of ordinals in $\Psi_{\mS}$ for each $\mS\in dom(\mathtt{Q})\subset c$,
$c$ is a bound of ranks of the inference rules for stability and of cut formulas as well as
successor stable ordinals collected in $dom(\mathtt{Q})$.

The rôle of the calculus $\vdash^{* a}_{c}$ is twofold:
first finite proof figures are embedded in the calculus, and
second the cut rank $c$ in $\vdash^{* a}_{c}$ is lowered to $\mI_{N}$.
Then the derivation is collapsed down to$<\mI_{N}$ using the collapsing function

In both of calculi,
$\{a,c,d,e\}\subset\calh_{\gam}[\Tht]$ is required,
cf. (<ref>) and (<ref>),
and $\Tht\subset M_{\mathtt{Q}}$, i.e.,
$\Tht\subset M_{\rho}$ for every ordinal $\rho$ in the collection $\mathtt{Q}$,
cf. (<ref>) and (<ref>).
Then we obtain $\{a,c,d,e\}\subset M_{\rho}$.
The reason for these constraints is to ensure the condition (<ref>), which
says that every ordinal occurring in the finite function $m(\rho)$ has to be in $M_{\rho}$.
A new ordinal $\kap=\psi_{\rho}^{h}(\alp)$ enters in derivation when a cap $\rho$ of the capped formula
$A^{(\rho)}$ is replaced by
another cap $\kap$ to $A^{(\kap)}$ in the main lemma of Recapping <ref>.
Here a finite function $h=m(\kap)$ is constructed from the function $m(\rho)$ and some ordinals $b,d,a$,
where ordinals $b$ and $s$ are ranks of formulas in derivations, and $a$ the ordinal height of the derivation.
Two constraints yield $\{b,d,a\}\subset M_{\rho}$, and the ordinal $\kap$ is chosen so that
a specified finite subset of $M_{\rho}$ is a subset of $M_{\kap}$, cf. Definition <ref>.

However the condition $\sfk(\Gam)\subset\calh_{\gam}[\Tht]$ is
incompatible with $\Tht\subset M_{\rho}$
when $(\mathcal{H}_{\gamma},\Theta; \mathtt{Q})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$
since we need to consider a collapsed formula $A^{[\rho/\mS]}$ in proving the axiom
The standard requirement $\sfk(\Gam)\subset\calh_{\gam}[\Tht]$ in operator controlled derivations
is weakened in
(<ref>) and (<ref>).
These say the following:
Assume that, e.g., $(\mathcal{H}_{\gamma},\Theta; \mathtt{Q})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$ holds,
and an ordinal $\alp$ occurs in a formula $A\in\Gam$ with $\rk(A)\geq\mS$.
Then either $\alp\in \calh_{\gam}[\Tht]$ or there are $\mS<\mT\in dom(\mathtt{Q})$, $\rho$ and
\in \calh_{\gam}[\Tht]$ such that
The weakened condition implies Proposition <ref>, which states that
every ordinal $\alp$ occurring in $A$ with $\rk(A)\geq\mS$ is in the set
In particular, $\sfk(A)\subset\calh_{\gam}[\Tht]$ when $\mS$ is the largest one in $dom(\mathtt{Q})$.
Therefore in eliminating the largest successor stable ordinal $\mS$, the above schema works in the sense that
the rank of formulas to be reflected is going down to $\mS$ by recapping successively.
Then the cap plays no rôle, i.e., $A^{(\rho)}$ is equivalent to the uncapped $A$ if $\rk(A)<\mS$,
cf. Lemma <ref>.

The weakened condition comes from a proof of Tautology lemma <ref>.<ref>
as follows.
Let $\sig\in\Psi_{\mS}$, $A\simeq\bigvee(A_{\iota})_{\iota\in J}$ and $I=\{\iota^{[\sig/\mS]}: \iota\in[\sig]J\}$,
where $\iota\in[\sig]J$ iff $\iota\in J$ and $\sfk(\iota)\subset M_{\sig}$.
Let $\rk(A)\geq\mS$. Otherwise we don't need to collapse the formula $A$.
Then $A^{[\sig/\mS]}\simeq\bigvee(B_{\nu})_{\nu\in I}$ with $B_{\nu}\equiv A_{\iota}^{[\sig/\mS]}$ for $\nu=\iota^{[\sig/\mS]}$,
$\rk(A^{[\sig/\mS]})=\rk(A)[\sig/\mS]$ and
$\sfk(\iota^{[\sig/\mS]})=\sfk(\iota)^{[\sig/\mS]}$ by Proposition <ref>.
A standard proof of the tautology $\lnot A^{[\sig/\mS]}, A^{[\sig/\mS]}$ runs as follows:

\[
\infer[(\bigwedge)]{\mathcal{H}_{\gamma}[\sfk(A^{[\sig/\mS]}] \vdash^{ 2d[\sig/\mS]}_{0}
\lnot A^{[\sig/\mS]}, A^{[\sig/\mS]}
\infer[(\bigvee)]{ \mathcal{H}_{\gamma}[\sfk(A^{[\sig/\mS]})\cup\sfk(\iota^{[\sig/\mS]})] \vdash^{ 2d_{\iota}[\sig/\mS]+1}_{0}
\lnot A_{\iota}^{[\sig/\mS]}, A^{[\sig/\mS]}
\mathcal{H}_{\gamma}[\sfk(A^{[\sig/\mS]})\cup\sfk(\iota^{[\sig/\mS]}) ]\vdash^{ 2d_{\iota}[\sig/\mS]}_{0}
\lnot A_{\iota}^{[\sig/\mS]},  A_{\iota}^{[\sig/\mS]}
\]

where $d=\rk(A)$ and $d_{\iota}=\rk(A_{\iota})$ with $\iota\in[\sig]J$, and $\mS\in dom(\mathtt{Q})$ with
$\sig\in \mathtt{Q}(\mS)$.
Here $\sfk(A^{[\sig/\mS]})\not\subset M_{\sig}$ and the condition (<ref>) does not hold.

Observe that $\sfk(A^{[\sig/\mS]})\subset \calh_{\mS}[\sfk(A)\cup\{\sig\}]$ and
$\sfk(\iota^{[\sig/\mS]})\subset \calh_{\mS}[\sfk(\iota)\cup\{\sig\}]$
since $\alp[\sig/\mS] \in \calh_{\mS}[\{\alp,\sig\}]$.
We have $\mT\leq\alp[\sig/\mS]<\mS$ and $\mT\leq \rk(A^{[\sig/\mS]})<\mS$ for $\mT<\mS$.
For every ordinal $\alp[\sig/\mS]$ occurring in $A^{[\sig/\mS]}$, either $\alp\in\calh_{\mS}[\sfk(A)]$ or
there exists a $\bet\in\calh_{\mS}[\sfk(A)]$ such that $\alp=\bet[\sig/\mS]$.
Thus we arrive at the weakened condition (<ref>), and
obtain $\sfk(A^{[\sig/\mS]})\subset \calh_{\mS}[\sfk(A)\cup \mathtt{Q}(\mS)]$ by Proposition <ref>.
In Definition <ref> of the $*$-calculus,
the operator $\calh_{\gam}$ controls ordinals occurring in
derivations of $(\calh_{\gam},\Tht;\mathtt{Q})\vdash^{* a}_{c}\Gam;\Pi^{(\cdot)}$
using ordinals in $\Tht$ with the help of the family $\mathtt{Q}$.
Instead of a standard one, we prove the tautology $\lnot A^{[\sig/\mS]}, A^{[\sig/\mS]}$ as follows:

\[
\infer[(\bigwedge)]{(\mathcal{H}_{\mI_{N}},\sfk(A),\mathtt{Q})\vdash^{ 2d}_{\mI_{N}}
\lnot A^{[\sig/\mS]}, A^{[\sig/\mS]}
\infer[(\bigvee)]{(\mathcal{H}_{\mI_{N}},\sfk(A)\cup\sfk(\iota),\mathtt{Q})\vdash^{ 2d_{\iota}+1}_{\mI_{N}}
\lnot A_{\iota}^{[\sig/\mS]}, A^{[\sig/\mS]}
(\mathcal{H}_{\mI_{N}},\sfk(A)\cup\sfk(\iota),\mathtt{Q})\vdash^{ 2d_{\iota}}_{\mI_{N}}
\lnot A_{\iota}^{[\sig/\mS]},  A_{\iota}^{[\sig/\mS]}
\]

where $2d\in\mathcal{H}_{0}[\sfk(A)]\subset\mathcal{H}_{\mI_{N}}[\sfk(A)]$ for (<ref>).
Let $B(0)$ be a $\bigwedge$-formula with $\rk(B(0))<\mS$ and $u$ an $RS$-term such that
$\sfk(B(u))\subset M_{\sig}$. We have $B(u)^{[\sig/\mS]}\equiv B(u^{[\sig/\mS]})$.
From the derivation of the tautology $\lnot B(u)^{[\sig/\mS]}, B(u)^{[\sig/\mS]}$,
the axiom $\lnot\exi x\, B(x),\exi x\in L_{\mS}B(x)$ is derived in Lemma <ref> using an inference
for the stability of a successor stable ordinal $\mS$ as follows.

\[
\infer[(\bigwedge)]{
\lnot \exists x\, B(x),\exists x\in L_{\mathbb{S}}B(x)}
\infer{
\lnot B(u),\exists x\in L_{\mathbb{S}}B(x)}
\lnot B(u),B(u)
\{
\infer[(\bigvee)]{
\lnot B(u)^{[\sigma/\mathbb{S}]}, \exists x\in L_{\mathbb{S}}B(x)
\}_{\sfk(B(u))\subset M_{\sig}}
\lnot B(u)^{[\sigma/\mathbb{S}]}, B(u^{[\sigma/\mathbb{S}]})
\]

where $u^{[\sigma/\mathbb{S}]}\in Tm(\mS)$ and
$\sig$ ranges over ordinals such that $\sfk(B(u))\subset M_{\sig}$.
The inference says that `if $B(u)$, then there exists an ordinal $\sig$ such that $B(u)^{[\sigma/\mathbb{S}]}$'.

Capping lemma <ref> of subsection <ref> the relation $\vdash^{* a}_{c}$
is embedded in another derivability relation $\vdash^{a}_{c,d,e}$ by putting caps $\rho$ on formulas.
Let $\sig<\rho$. Then $\sfk(B(u^{[\sigma/\mathbb{S}]}))\subset M_{\rho}$.
In the above derivation each formula puts on the cap $\rho$ except $\lnot B(u)^{[\sigma/\mathbb{S}]}$.
An inference for reflection says that `if $B(u)^{(\rho)}$, then there exists an ordinal $\sig$ such that $B(u)^{(\sigma)}$'.
Therefore the above derivation turns to the following.

\[
\infer[(\bigwedge)]{
(\lnot \exists x\, B(x))^{(\rho)},(\exists x\in L_{\mathbb{S}}B(x))^{(\rho)}}
\infer{
\lnot B(u)^{(\rho)},(\exists x\in L_{\mathbb{S}}B(x))^{(\rho)}}
\lnot B(u)^{(\rho)},B(u)^{(\rho)}
\{
\infer[(\bigvee)]{
\lnot B(u)^{(\sigma)}, (\exists x\in L_{\mathbb{S}}B(x))^{(\rho)}
\}_{\sfk(B(u))\subset M_{\sig}, \sig<\rho}
\lnot B(u)^{(\sigma)}, B(u^{[\sigma/\mathbb{S}]})^{(\rho)}
\]

In doing so, it is better to distinguish $\lnot B(u)^{[\sigma/\mathbb{S}]}$ from
$B(u^{[\sigma/\mathbb{S}]})$ formally.
The latter $B(u^{[\sigma/\mathbb{S}]})$ puts on a bigger cap $\rho$ as
$B(u^{[\sigma/\mathbb{S}]})^{(\rho)}$, while
the former $\lnot B(u)^{[\sigma/\mathbb{S}]}$ changes to $\lnot B(u)^{(\sig)}$ with a smaller cap $\sig<\rho$.
Let us replace the collapsed formula $\lnot B(u)^{[\sigma/\mathbb{S}]}$ by an uncollapsed
$\lnot B(u)^{\{\sigma\}}$, and collect uncollapsed formulas to the right of the semicolon as
This results in the $*$-calculus $(\mathcal{H}_{\gamma},\Theta; \mathtt{Q})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$, and a derivation of $\lnot A^{[\sig/\mS]}; A^{\{\sig\}}$ runs as follows.

\[
\infer[(\bigwedge)]{(\mathcal{H}_{\mI_{N}},\sfk(A) ;\mathtt{Q})\vdash^{ 2d}_{\mI_{N}}
\lnot A^{[\sig/\mS]}; A^{\{\sig\}}
\infer[(\bigvee)]{(\mathcal{H}_{\mI_{N}},\sfk(A)\cup\sfk(\iota) ;\mathtt{Q})\vdash^{ 2d_{\iota}+1}_{\mI_{N}}
\lnot A_{\iota}^{[\sig/\mS]}; A^{\{\sig\}}
(\mathcal{H}_{\mI_{N}},\sfk(A)\cup\sfk(\iota) ;\mathtt{Q})\vdash^{ 2d_{\iota}}_{\mI_{N}}
\lnot A_{\iota}^{[\sig/\mS]}; A_{\iota}^{\{\sig\}}
\]

In inferences $(\bigwedge)$ introducing $A\simeq\bigwedge(A_{\iota})_{\iota\in J}$,
$\iota\in J$ is restricted to $\iota\in[\mathtt{Q}(\Tht)^{c}]_{A}J\subset J$ in
Definition <ref> for the weakened condition (<ref>).

A new constraint $\mathtt{Q}(\mS)\subset \mathcal{H}_{\gam^{\mathtt{ Q}}_{\mS}+\mI_{N}}[\Theta]$ is
imposed in $(\calh_{\gam},\Tht,\mathtt{Q})\vdash^{a}_{c,d,e}\Gam$, cf. (<ref>)
in Definition <ref>.
In Lemmas <ref> and <ref> of
the elimination of the largest successor stable ordinal $\mS$,
we assume that every formula $A^{(\rho)}$
occurring in the derivation is of $\rk(A)<\mS$ if $\rho\in\mathtt{Q}(\mS)$.
Then the formula $A^{(\rho)}$ takes off the cap $\rho$, and the set $\mathtt{Q}(\mS)$ no longer
helps operators $\calh_{\gam}$.
Then the weakened condition (<ref>) states that
either $\alp\in \calh_{\gam}[\Tht]$ or there are $\mU<\mT\in dom(\mathtt{Q})\cap\mS$, $\sig$ and
$\bet\in \calh_{\gam}[\Tht]$ such that
$\alp=\bet[\sig/\mT]$ when the ordinal $\alp$ occurs in a formula $B\in\Gam$ with $\rk(B)\geq\mU$
and $(\mathcal{H}_{\gamma},\Theta, \mathtt{Q})\vdash^{a}_{c,d,\mT^{\dagger}}\Gamma$.
Let $\mT<\mS$ be the next largest successor stable ordinal.
In the derivation there may occur a formula $C^{(\sig)}$ such that $\sig\in\mathtt{Q}(\mT)$ and $\rk(C)\geq\mT$.
Then $\sfk(C)\subset\calh_{\gam}[\Tht\cup\mathtt{Q}(\mS)]$ by Proposition <ref>.
Let us lift the threshold $\gam_{0}\leq\gam^{\mathtt{ Q}}_{\mS}$ to a larger one
$\gam_{1}=\gam^{\mathtt{ Q}}_{\mS}+\mI_{N}$.
Then we obtain $\sfk(C)\subset\calh_{\gam_{1}}[\Tht]$ as long as
$\mathtt{Q}(\mS)\subset \mathcal{H}_{\gam^{\mathtt{ Q}}_{\mS}+\mI_{N}}[\Theta]$ holds.
This explains the constraint (<ref>).

Now details follow.

§.§ Operator controlled $*$-derivations

Operator controlled derivations are introduced by W. Buchholz[6].
By a successor stable ordinal we mean ordinals in $\bigcup_{0<i\leq N}SSt_{i}$,
and $\mS^{\dagger}:=\mS^{\dagger 1}$.
Let $\mathcal{L}_{i}=\{\in,\Ome\}\cup\{St_{j}\}_{j<i}$.

A finite family for an ordinal $\gam_{0}$
is a finite function ${\tt Q}\subset\coprod_{\mS}\Psi_{\mS}$ such that
its domain $dom({\tt Q})$ is a finite set of successor stable ordinals,
and ${\tt Q}(\mS)$ is a finite set of ordinals $\kap$ in $\Psi_{\mS}$ for each $\mS\in dom({\tt Q})$
such that $m(\kap)$ is special,
$\gam_{0}\leq\mathtt{p}_{0}(\kap)$, and

\left(
\mathtt{Q}(\mS)\subset \bigcap_{\mT<\mS} M_{\mathtt{Q}(\mT)}
\spand
\bigcap_{\mT\leq\mS}M_{\mathtt{ Q}(\mT)}
\right)$, where
${\tt Q}(\mT)=\emptyset$ for $\mT\not\in dom({\tt Q})$,
$SC_{\Lambda}(\mathtt{ Q}(\mS))=\bigcup\{\{\mS\}\cup SC_{\Lambda}(m(\rho)\cup\{\mathtt{p}_{0}(\rho)\}):\rho\in \mathtt{ Q}(\mS)\}$
$M_{\mathtt{Q}(\mS)}=\bigcap_{\sig\in\mathtt{Q}(\mS)} M_{\sig}$.
$\bigcup{\tt Q}=\bigcup_{\mS\in dom({\tt Q})}{\tt Q}(\mS)$ and
$M_{\mathtt{Q}}=\bigcap_{\sig\in\bigcup\mathtt{Q}} M_{\sig}$.

Let for an $RS$-term $\iota$, $\iota\in M_{\mathtt{Q}^{\mS,e}}^{-1}$ iff the following condition is met:

(<<e (ι[ρ/]^-1)⊂M_𝚀)
$\iota\in M_{\mathtt{Q}}^{-1}$ iff either $\sfk(\iota)\subset M_{\mathtt{Q}}$ or there exists a finite family
$\mathtt{Q}\cup\{(\mT,\rho)\}$ for $\gam_{0}$ such that
$\sfk(\iota[\rho/\mT]^{-1})\subset M_{\mathtt{Q}}$ and $\mT\in M_{\mathtt{Q}}$.

Obviously $M_{\mathtt{Q}^{\mS,e}}^{-1} \subset M_{\mathtt{Q}}^{-1}$.
In the definition of $\iota\in M_{\mathtt{Q}}^{-1}$, $\sfk(\iota[\rho/\mT]^{-1})\subset M_{\mathtt{Q}}$ means that
there exists a $\nu\neq\iota$ such that
$\sfk(\nu)\subset M_{\mathtt{Q}}\cap M_{\rho}$ and $\nu^{[\rho/\mT]}=\iota$.
Such $\nu,\rho,\mT$ are uniquely determined if these exist.

For $\iota\in M_{\mathtt{Q}}^{-1}$,
$\iota_{\mathtt{Q}}^{-1}$ denotes an $RS$-term such that $\iota_{\mathtt{Q}}^{-1}=\iota$, and let
$\mathtt{Q}[\iota]:=\mathtt{Q}$ and $\mathtt{R}[\iota]:=\emptyset$
if $\sfk(\iota)\subset M_{\mathtt{Q}}$.
Otherwise let $\iota_{\mathtt{Q}}^{-1}=\iota[\rho/\mT]^{-1}=\nu$ such that $\nu^{[\rho/\mT]}=\iota$, and
$\mathtt{Q}[\iota]:=\mathtt{Q}\cup\mathtt{R}[\iota]$ with $\mathtt{R}[\iota]=\{(\mT,\rho)\}$.
For $\iota\not\in M_{\mathtt{Q}}^{-1}$ let
$\iota_{\mathtt{Q}}^{-1}=\Gam_{\mI_{N}+1}$ and $\mathtt{Q}[\iota]:=\mathtt{Q}$.

$\iota_{\mathtt{Q}^{\mS,e}}^{-1}=\iota_{\mathtt{Q}}^{-1}$ when $\iota\in M_{\mathtt{Q}^{\mS,e}}^{-1}$,
and $\iota_{\mathtt{Q}^{\mS,e}}^{-1}=\Gam_{\mI_{N}+1}$ else.

For a finite set $X$ of ordinals, let
$X_{\mathtt{Q}}^{-1}:=\{\alp_{\mathtt{Q}}^{-1}:\alp\in X\}$,
$\mathtt{Q}[X]=\bigcup\{\mathtt{Q}[\alp]:\alp\in X\}$ and
$X_{\mathtt{Q}^{\mS,e}}^{-1}:=\{\alp_{\mathtt{Q}^{\mS,e}}^{-1}:\alp\in X\}$.

Let $\Tht$ be a finite set of ordinals and $c$ an ordinal.
For $A\simeq\bigvee(A_{\iota})_{\iota\in J}$ and $\iota\in J$, $\iota\in [\mathtt{ Q}(\Tht)^{c}]_{A}J = [\mathtt{ Q}(\Tht)^{c}]_{\lnot A}J$ iff the following four conditions are met:

$ \iota\in M^{-1}_{\mathtt{ Q}}$.

$\Tht\subset M_{\mathtt{R}[\iota]}$.

\rk(A)<\mS \Rarw
\mathtt{R}[\iota]\subset\mathtt{Q} \lor dom(\mathtt{R}[\iota])\subset\mS
\right]$.
Note that $[\mathtt{ Q}(\Tht)^{c}]_{A}J=J$ when $\mathtt{Q}=\emptyset$.

Let $\mathtt{Q}_{1}=\mathtt{Q}\cup\{(\mU,\sig)\}$ be a finite family for $\gam_{0}$,
$\Tht_{1}\supset\Tht$ and
$\iota\in [\mathtt{Q}_{1}(\Tht_{1})^{c}]_{A}J$ for $A\simeq\bigvee(A_{\iota})_{\iota\in J}$.
Then $\iota\in[\mathtt{Q}(\Tht)^{c}]_{A}J$,
$\iota^{-1}_{\mathtt{Q}_{1}}=\iota^{-1}_{\mathtt{Q}}$ and $\mathtt{Q}_{1}[\iota]=\mathtt{Q}[\iota]$
Note that if $\mathtt{Q}_{1}\cup\{(\mT,\rho)\}$ is a finite family for $\gam_{0}$, then so is
From (<ref>) and $M_{\mathtt{Q}_{1}}\subset M_{\mathtt{Q}}$ we see $M_{\mathtt{Q}_{1}}^{-1}\subset M_{\mathtt{Q}}^{-1}$, which yields
$\iota^{-1}_{\mathtt{Q}_{1}}=\iota^{-1}_{\mathtt{Q}}$, $\mathtt{Q}_{1}[\iota]=\mathtt{Q}[\iota]$
and $\iota\in[\mathtt{Q}(\Tht)^{c}]_{A}J$ by Definition <ref>.<ref>.

By an uncollapsed formula we mean a pair $\{ A,\rho\}$ of $RS$-sentence $A$
and an ordinal
$\rho\prec\mathbb{S}$ for a successor stable ordinal $\mS$ such that
$\mathsf{k}(A)\subset M_{\rho}$.
Such a pair is denoted by $A^{\{ \rho\}}$.
When we write $\Gamma^{\{ \rho\}}$, we tacitly assume that
$\mathsf{k}(\Gamma)\subset M_{\rho}$.

We define a derivability relation
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$
$c$ is a bound of ranks of the inference rules $(i{\rm -stbl})$ and one of ranks of cut formulas.
The relation depends on an ordinal $\gam_{0}$, and
should be written as $(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi})\vdash^{*a}_{c,\gamma_{0}} \Gamma;\Pi^{\{\cdot\}}$.
However the ordinal $\gam_{0}$ will be fixed.
So let us omit it.

Note that if $\gam_{0}\leq{\tt p}_{0}(\sig)$ for $\sig\prec\mS$, then
$\calh_{\gam_{0}}(\sig)\cap\mS\subset\sig$ by Proposition <ref>.

Let $\Theta$ be a finite set of ordinals, $a,c$ ordinals, and
$\mathtt{ Q}_{\Pi}$ a finite family for $\gam_{0}$.
$\Pi=\bigcup_{(\mS,\sig)\in\mathtt{ Q}_{\Pi}}\Pi_{\sigma}$ be
a set of formulas such that $\Pi\subset\Delta_{0}(\mathcal{L}_{N+1})$,
${\sf k}(\Pi_{\sigma})\subset M_{\sig}$
for each $(\mS,\sigma)\in\mathtt{ Q}_{\Pi}$ and
$dom(\mathtt{ Q}_{\Pi})\subset c$.
$\Pi^{\{\cdot\}}=\bigcup_{(\mS,\sig)\in\mathtt{ Q}_{\Pi}}\Pi_{\sigma}^{\{\sigma\}}$.

In the following (<ref>) means that either $\alp\in\mathcal{H}_{\gamma}[\Tht]$
or $\alp^{-1}_{\mathtt{Q}_{\Pi}^{\mS,c}}\in \mathcal{H}_{\gamma}[\Tht]$ for each
Note that $\Gam_{\mI_{N}+1}\not\in \mathcal{H}_{\gamma}[\Tht]$.

$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c, \gam_{0}} \Gamma;\Pi^{\{\cdot\}}$ holds
for a set
$\Gamma$ of formulas
if $\gam\leq\gam_{0}$

\begin{equation}
\label{eq:controlder*5}
\Tht\subset M_{\mathtt{Q}_{\Pi}}
\end{equation}

\begin{equation}
\label{eq:controlder*1}
\{\gam,a,c,\gam_{0}\}\cup dom(\mathtt{Q}_{\Pi})
\subset\mathcal{H}_{\gamma}[\Theta]
\end{equation}

\begin{equation}
\label{eq:controlder*4}
\fal\mS\in dom(\mathtt{ Q}_{\Pi})\cup\{0\}
\left(
(\sfk^{\mS}(\Gam\cup\Pi))^{-1}_{\mathtt{Q}_{\Pi}^{\mS,c}}\subset \mathcal{H}_{\gamma}[\Tht]
\right)
\end{equation}

and one of the following cases holds:

There exist
$A\simeq\bigvee(A_{\iota})_{\iota\in J}$, an ordinal
$a(\iota)<a$ and an $\iota\in J$
such that
$A\in\Gamma$ and
$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a(\iota)}_{c}\Gamma,
A_{\iota};\Pi^{\{ \cdot \}}$.

$(\bigvee)^{\{ \cdot \}}$
There exist
$A\equiv B^{\{ \sigma \}}\in\Pi^{\{ \cdot \}}$,
$B\simeq\bigvee(B_{\iota})_{\iota\in J}$, an ordinal
$a(\iota)<a$ and an
such that
$(\mathcal{H}_{\gamma},\Theta; \mathtt{ Q}_{\Pi})\vdash^{* a(\iota)}_{c}\Gamma;\Pi^{\{ \cdot \}},
A_{\iota}$ with $A_{\iota}\equiv B_{\iota}^{\{ \sigma \}}$.

There exist
$A\simeq\bigwedge(A_{\iota})_{ \iota\in J}$ such that $A\in\Gamma$.
For each $\iota\in [\mathtt{Q}_{\Pi}(\Tht)^{c}]_{A}J$
there is an ordinal $a(\iota)<a$ such that
$(\mathcal{H}_{\gamma},\Theta_{\iota} ;\mathtt{ Q}_{\Pi}[\iota]
\vdash^{* a(\iota)}_{c}\Gamma,
A_{\iota};\Pi^{\{ \cdot \}}$ holds for
$\Theta_{\iota}=\Theta\cup \iota^{-1}_{\mathtt{Q}_{\Pi}}\cup dom(\mathtt{R}[\iota])$.

$(\bigwedge)^{\{ \cdot \}}$
There exist
$A\equiv B^{\{ \sigma \}}\in\Pi^{\{ \cdot \}}$,
$B\simeq\bigwedge(B_{\iota})_{\iota\in J}$, ordinals
$a(\iota)<a$ such that
$(\mathcal{H}_{\gamma},\Theta_{\iota};\mathtt{ Q}_{\Pi}[\iota])\vdash^{* a(\iota)}_{c}\Gamma;
B^{\{ \sigma \}}_{\iota},\Pi^{\{ \cdot \}}$
for each $\iota\in [\mathtt{Q}_{\Pi}(\Tht)^{c}]_{B}J \cap[\sigma]J$.

There exist an ordinal $a_{0}<a$ and a formula $C$
such that
$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a_{0}}_{c}\Gamma,\lnot C;\Pi^{\{\cdot\}}$
$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a_{0}}_{c}C,\Gamma;\Pi^{\{\cdot\}}$
with $\mbox{{\rm rk}}(C)<c$.

$(\Sigma(St)\mbox{{\rm -rfl}})$
There exist ordinals
$a_{\ell}, a_{r}<a$ and a formula $C\in\Sigma(\mathcal{L}_{N+1})$
such that
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{\ell}}_{c}\Gamma,C; \Pi^{\{\cdot\}}$
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{r}}_{c}
\lnot \exists x\,C^{(x,\mI_{N})}, \Gamma; \Pi^{\{\cdot\}}$, where

$(\Sigma(\Ome)\mbox{{\rm -rfl}})$
There exist ordinals
$a_{\ell}, a_{r}<a$ and a formula $C\in\Sigma(\mathcal{L}_{0}:\Ome)$
such that
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{\ell}}_{c}\Gamma,C; \Pi^{\{\cdot\}}$
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{r}}_{c}
\lnot \exists x<\Ome\,C^{(x,\Ome)}, \Gamma;\Pi^{\{\cdot\}}$, where

$(i{\rm -stbl}(\mS))$
$0<i\leq N$ and $c\geq\mI_{N}$.
There exist an ordinal $a_{0}<a$,
an $i$-successor stable ordinal $\mS\in SSt_{i}\cap c$,
a $\bigwedge$-formula
$B(0)\in\Del_{0}(\mathcal{L}_{i})$ with $\rk(B(0))<\mS$
and a $u\in Tm(\mI_{N})$
for which the following hold:
\mS\leq\rk(B(u))<c

$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi}
)\vdash^{* a_{0}}_{c}
\Gamma, B(u);\Pi^{\{\cdot\}}$, and
\mathtt{ Q}_{\Pi}^{\sigma}
\vdash^{* a_{0}}_{c}
\Gamma; \lnot B(u)^{\{\sigma\}},\Pi^{\{\cdot\}}$
holds for every ordinal $\sigma\in\Psi_{\mS}$ such that
${\tt p}_{0}(\sig)\geq\gam_{0}$ and

where $\mathtt{ Q}_{\Pi}^{\sigma}={\tt Q}_{\Pi}\cup\{(\mS,\sigma)\}$ with
$dom(\mathtt{ Q}_{\Pi}^{\sigma})=dom({\tt Q}_{\Pi})\cup\{\mS\}$
$\left(\mathtt{ Q}_{\Pi}^{\sigma}\right)(\mS)={\tt Q}_{\Pi}(\mS)\cup\{\sig\}$.

\[
\hspace{-10mm}
\infer{(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c} \Gamma;\Pi^{\{\cdot\}}}
(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi}
)\vdash^{* a_{0}}_{c}
\Gamma, B(u);\Pi^{\{\cdot\}}
\{
\mathtt{ Q}_{\Pi}^{\sigma}
\vdash^{* a_{0}}_{c}
\Gamma; \lnot B(u)^{\{\sigma\}},\Pi^{\{\cdot\}}
\}_{\sig}
\]

It is clear that if
$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c} \Gamma;\Pi^{\{\cdot\}}$ and
$\gam\leq\gam_{1}\leq\gam_{0}$ with $\gam_{1}\in\calh_{\gam_{1}}[\Tht]$,
then $(\mathcal{H}_{\gamma_{1}},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c} \Gamma;\Pi^{\{\cdot\}}$

Let $(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c, \gam_{0}} \Gamma;\Pi^{\{\cdot\}}$ with $dom(\mathtt{Q}_{\Pi})\subset c$.
Then $\sfk^{\mS}(\Gam\cup\Pi)\subset\calh_{\gam}[\Tht(\mathtt{Q}_{\Pi})^{\mS,c}]$
for $\mS\in dom(\mathtt{Q}_{\Pi})\cup\{0\}$, where
Let $\alp\in\sfk^{\mS}(\Gam\cup\Pi)$.
By (<ref>) we have either $\alp\in\mathcal{H}_{\gamma}[\Tht]$
or $\alp^{-1}_{\mathtt{Q}_{\Pi}^{\mS,c}}\in \mathcal{H}_{\gamma}[\Tht]$.
Assume the latter.
Then there is a $\rho\in\mathtt{Q}_{\Pi}(\mT)$ with a $\mS<\mT\in dom(\mathtt{Q}_{\Pi})$ such that
$\alp=\bet[\rho/\mT]$ and $\bet=\alp^{-1}_{\mathtt{Q}_{\Pi}^{\mS,c}}\in \mathcal{H}_{\gamma}[\Tht]$.
$\alp\in\calh_{\mT}[\calh_{\gam}[\Tht]\cup\mathtt{Q}_{\Pi}(\mT)]\subset\calh_{\gam}[\Tht(\mathtt{Q}_{\Pi})^{\mS,c}]$ by $\gam>\mT$.

We will state some lemmas for the operator controlled derivations.
These can be shown as in [6].

Let $d=\mbox{{\rm rk}}(A)$ and $\{\gam,\gam_{0}\}\subset \calh_{\gam}[\sfk(A)]$.

$(\mathcal{H}_{\gamma},{\sf k}(A);\emptyset
)\vdash^{* 2d}_{0}
\lnot A, A; \emptyset$.

$(\mathcal{H}_{\gamma},{\sf k}(A)\cup\{\mS\};\{(\mS,\sig)\}
)\vdash^{* 2d}_{\mI_{N}}
\lnot A^{[\sig/\mS]};A^{\{\sig\}}$ if
\subset M_{\sig}$,
$A\in\Delta_{0}(\mathcal{L}_{N+1})$, $\rk(A)<\mI_{N}$ and $\gam\geq\mI_{N}$.

Each is seen by induction on $d=\mbox{{\rm rk}}(A)$.
For example consider the lemma <ref>.<ref>.
Let $\mathtt{Q}_{\Pi}=\{(\mS,\sig)\}$ and $\Tht=\sfk(A)\cup\{\mS\}$.
We have
$\Tht\subset M_{\sig}=M_{\mathtt{Q}_{\Pi}}$ for (<ref>),
$\{\gam, 2d,\mI_{N},\gam_{0}\}\subset\calh_{\gam}[\Tht]$ for (<ref>),
and $(\sfk^{0}(A^{[\sig/\mS]}))^{-1}_{\mathtt{Q}_{\Pi}^{0,\mI_{N}}}=(\sfk(A^{[\sig/\mS]}))^{-1}_{\mathtt{Q}_{\Pi}^{0,\mI_{N}}}\subset\calh_{0}(\sfk(A))$
for (<ref>).

Let $A\simeq\bigvee(A_{\iota})_{\iota\in J}$ and $I=\{\iota^{[\sig/\mS]}: \iota\in[\sig]J\}$.
Then $A^{[\sig/\mS]}\simeq\bigvee(B_{\nu})_{\nu\in I}$ with $B_{\nu}\equiv A_{\iota}^{[\sig/\mS]}$ for $\nu=\iota^{[\sig/\mS]}$ by Proposition <ref>.
Let $\iota\in[\sig]J$. Then $\iota^{[\sig/\mS]}\in M_{\mathtt{Q}_{\Pi}}^{-1}$,
and $\iota^{[\sig/\mS]} \in [\mathtt{Q}_{\Pi}(\Tht)^{\mI_{N}}]_{A^{[\sig/\mS]}}J$
with $\mathtt{Q}_{\Pi}[\iota]=\mathtt{Q}_{\Pi}$.
$[\mathtt{Q}_{\Pi}(\Tht)^{\mI_{N}}]_{A^{[\sig/\mS]}}J=\{\iota^{[\sig/\mS]}: \iota\in[\sig]J\}$.

For $d_{\iota}=\rk(A_{\iota})\in\calh_{\gam}[\sfk(A,\iota)]$ with
we obtain by IH

\[
\infer[(\bigwedge)]{(\mathcal{H}_{\gamma},\Tht ;\mathtt{Q}_{\Pi})\vdash^{* 2d}_{\mI_{N}}
\lnot A^{[\sig/\mS]}; A^{\{\sig\}}}
\infer[(\bigvee)^{\{\cdot\}}]{(\mathcal{H}_{\gamma},\Tht\cup\sfk(\iota) ;\mathtt{Q}_{\Pi})\vdash^{* 2d_{\iota}+1}_{\mI_{N}}
\lnot A_{\iota}^{[\sig/\mS]}; A^{\{\sig\}}}
(\mathcal{H}_{\gamma},\Tht\cup\sfk(\iota) ;\mathtt{Q}_{\Pi})\vdash^{* 2d_{\iota}}_{\mI_{N}}
\lnot A_{\iota}^{[\sig/\mS]}; A_{\iota}^{\{\sig\}}
\]

\[
\infer[(\bigwedge)^{\{\cdot\}}]{(\mathcal{H}_{\gamma},\Tht ;\mathtt{Q}_{\Pi})\vdash^{* 2d}_{\mI_{N}}
A^{[\sig/\mS]}; \lnot A^{\{\sig\}}}
\infer[(\bigvee)]{(\mathcal{H}_{\gamma},\Tht\cup\sfk(\iota) ;\mathtt{Q}_{\Pi})\vdash^{* 2d_{\iota}+1}_{\mI_{N}}
A^{[\sig/\mS]}; \lnot A_{\iota}^{\{\sig\}}}
(\mathcal{H}_{\gamma},\Tht\cup\sfk(\iota) ;\mathtt{Q}_{\Pi})\vdash^{* 2d_{\iota}}_{\mI_{N}}
A_{\iota}^{[\sig/\mS]}; \lnot A_{\iota}^{\{\sig\}}
\]

(Embedding of Axioms)
For each axiom $A$ in $S_{\mI_{N}}$
there is an $m<\omega$ such that
\vdash^{* \mI_{N}\cdot 2}_{\mI_{N}, \mI_{N}+1} A;\emptyset$
Let us suppress the operator $\calh_{\mI_{N}}$ in the proof.
We show first that the axiom (<ref>),
$SSt_{i}(\sig)\land \vphi(u) \land u\in L_{\sig} \to \vphi^{L_{\sig}}(u)$
by an inference $(i{\rm -stbl}(\mathbb{S}))$ for successor $i$-stable ordinals $\mathbb{S}<\mI_{N}$.
Let $B(0)\in\Delta_{0}(\mathcal{L}_{i})$ be a $\bigwedge$-formula with $\rk(B(0))<\mS$,
and $u\in Tm(\mI_{N})$.

We may assume that
$\mI_{N}>d={\rm rk}(B(u))\geq\mathbb{S}$ with $|u|\geq\mS$.
Let ${\sf k}_{0}={\sf k}(B(0))$ and ${\sf k}_{u}={\sf k}(u)$.
We obtain by Tautology <ref>.<ref>,
$({\sf k}_{0}\cup{\sf k}_{u};\emptyset
)\vdash^{* 2d}_{0}
\lnot B(u),B(u);\emptyset$.

Let $\sigma\in\Psi_{\mS}$ be an ordinal such that
${\sf k}_{0}\cup{\sf k}_{u}
\subset M_{\sig}$ and
$\gam_{0}\leq\mathtt{ p}_{0}(\sig)$.
Tautology <ref>.<ref> yields
$({\sf k}_{0}\cup{\sf k}_{u}\cup\{\mS\};\{(\mS,\sigma)\})
\vdash^{* 2d}_{\mI_{N}}
B(u^{[\sigma/\mathbb{S}]}); \lnot B(u)^{\{\sigma\}}$.
Then for $\exists x\in L_{\mathbb{S}}B(x)\simeq\bigvee(B(v))_{v\in J}$
we obtain
u^{[\sigma/\mathbb{S}]}\in J=Tm(\mathbb{S})$ with
$B(u^{[\sigma/\mathbb{S}]})\equiv B(u)^{[\sigma/\mathbb{S}]}$.

\[
\hspace{-2mm}
\infer[(\bigwedge)]{ {\sf k}_{0}\cup\{\mS\};\vdash^{* \mathbb{I}_{N}+1}_{\mathbb{I}_{N}}
\lnot \exists x\, B(x),\exists x\in L_{\mathbb{S}}B(x);}
\infer[(i{\rm -stbl}(\mS))]{{\sf k}_{0}\cup{\sf k}_{u}\cup\{\mS\}; \vdash^{* \mathbb{I}_{N}}_{\mathbb{I}_{N}}
\lnot B(u),\exists x\in L_{\mathbb{S}}B(x);}
{\sf k}_{0}\cup{\sf k}_{u};  \vdash^{* 2d}_{0}\lnot B(u),B(u);
\{
\infer[(\bigvee)]{{\sf k}_{0}\cup\sfk_{u}\cup\{\mS\};\{(\mS,\sig)\}\vdash^{* 2d+1}_{\mI_{N}}
\exists x\in L_{\mathbb{S}}B(x);\lnot B(u)^{\{\sigma\}}
\}_{\sig}
{\sf k}_{0}\cup{\sf k}_{u}\cup\{\mS\};\{(\mS,\sig)\} \vdash^{* 2d}_{\mI_{N}}
B(u^{[\sigma/\mathbb{S}]}); \lnot B(u)^{\{\sigma\}}
\]

$(\mathcal{H}_{\mI_{N}}, \emptyset;\emptyset)\vdash^{* \mI_{N}+\ome}_{\mI_{N}}
\fal\mS, v
\left[
A(v) \land v\in L_{\mathbb{S}} \to A^{(\mathbb{S},\mI_{N})}(v)
\right]$, where
\left(St_{i}(\alp)\land \exi\bet<\alp
\fal \gam<\alp(St_{i}(\gam)\to \gam\leq\bet)]\right)$.

Next we show the axiom (<ref>).
Let $\alp$ be an ordinal such that $\alp<\mI_{N}$.
We obtain for $\alp<\alp^{\dagger N}<\mI_{N}$ with $d_{0}=\rk(\alp<\alp^{\dagger N})$
and $\alp^{\dagger N}\leq d_{1}=\rk(St_{N}(\alp^{\dagger N}))<d_{2}=\ome(\alp^{\dagger N}+1)$
with $\alp^{\dagger N}\in\mathcal{H}_{0}[\{\alp\}]$

\[
\infer[(\bigwedge)]{
\emptyset;\emptyset \vdash^{* \mI_{N}}_{0}
\fal \alp\in ON \exi \sig \left(\alp<\sig \land St_{N}(\sig) \right);\emptyset
\infer[(\bigvee)]{
\{\alp\};\emptyset \vdash^{* d_{2}+1}_{0} \exi \sig \left(\alp<\sig \land St_{N}(\sig)\right);\emptyset
\infer[(\bigwedge)]{
\{\alp\};\emptyset \vdash^{* d_{2}}_{0}
\alp<\alp^{\dagger N} \land St_{N}(\alp^{\dagger N});\emptyset
\{\alp\};\emptyset \vdash^{* d_{0}}_{0}\alp<\alp^{\dagger N};\emptyset
\{\alp\};\emptyset \vdash^{* 2d_{1}}_{0} St_{N}(\alp^{\dagger N});\emptyset
\]

Third the axiom (<ref>) is seen similarly.
Let $\mS\in St_{j+1}$ for a $j\geq i$.
We see
$St_{i}(\mS)$ immediately from Definition <ref>.<ref>.
For a given $\alp<\mS$ let $\sig=\alp^{\dagger j}\in St_{j}\cap\calh_{0}[\{\alp\}]$.
Then $\alp<\sig<\mS$ by Proposition <ref>, i.e., by $\mS\in St_{j+1}\subset LSt_{j}$.

$\Del_{0}(\mathcal{L}_{N+1})$-Collection follows from an inference $(\Sig(St){\rm -rfl})$, and
the $\Del_{0}$-collection for the recursively regularity of $\Ome$ follows from an inference
$(\Sig(\Ome){\rm -rfl})$.

If $S_{\mI_{N}}\vdash \Gamma$ for sets $\Gamma$ of sentences,
there are $m,k<\omega$ such that
$(\mathcal{H}_{\mI_{N}},\emptyset;\emptyset)\vdash_{\mI_{N}+m}^{* \mI_{N}\cdot 2+k}\Gamma;\emptyset$

Let $(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$,
and $\mS$ a successor stable ordinal and $\sig\in\Psi_{\mS}$.
Assume $\mathtt{ Q}_{\Pi}\cup\{(\mS,\sig)\}$ is a finite family for $\gam_{0}$,
$\mS\in \mathcal{H}_{\gamma}[\Theta]$ and
$\Tht\subset M_{\sig}$.
$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi}\cup\{(\mS,\sig)\})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$ holds.
By induction on $a$.
By the assumptions, (<ref>) in $(\mathcal{H}_{\gamma},\Theta;\mathtt{Q}^{\sig}_{\Pi})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$
is enjoyed for
Moreover (<ref>) and
(<ref>) follow from the assumptions.
For (<ref>) we have
$\mathcal{H}_{\gamma}[\Tht]\subset M_{\sig}$ by Proposition <ref>,
$\Tht\subset M_{\sig}$ and

Let $A\simeq\bigvee(A_{\iota})_{\iota\in J}$ and $\iota\in [\mathtt{Q}_{\Pi}^{\sig}(\Tht)^{c}]_{A}J$.
By Proposition <ref> we obtain
$\iota^{-1}_{\mathtt{Q}_{\Pi}^{\sig}}=\iota^{-1}_{\mathtt{Q}}$ and $\mathtt{Q}_{\Pi}^{\sig}[\iota]=\mathtt{Q}[\iota]$.
We need to prune some branches at inferences $(\bigwedge)$.

$(\mathcal{H}_{\gam},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c}\Gamma;\Pi^{\{\cdot\}}$ with
$A\simeq \bigwedge(A_{\iota})_{\iota\in J}$, $A\in\Gam$,
and $\iota\in [\mathtt{ Q}_{\Pi}(\Tht)^{c}]_{A}J$ .
$(\mathcal{H}_{\gam},\Theta\cup \iota^{-1}_{\mathtt{Q}_{\Pi}}\cup dom(\mathtt{R}[\iota]) ;
\mathtt{Q}_{\Pi}[\iota]
\vdash^{* a}_{c}
\Gamma,A_{\iota};\Pi^{\{\cdot\}}$.
By induction on $a$.
For (<ref>) in inferences $(i{\rm -stbl}(\mS))$,
we need to prune some branches such that
$\iota^{-1}_{\mathtt{Q}_{\Pi}}\cup dom(\mathtt{R}[\iota]) \subset M_{\sig}$.
Also by Proposition <ref> we need to prune some branches at inferences

Let $C\simeq\bigvee(C_{\iota})_{\iota\in J}$ and
either $c\geq\mI_{N}$ or $c<\Ome$.
$(\mathcal{H}_{\gamma},\Theta; \mathtt{ Q}_{\Pi})\vdash^{*a}_{c}\Gamma_{0},\lnot C
$(\mathcal{H}_{\gamma},\Theta; \mathtt{ Q}_{\Pi})\vdash^{*b}_{c}C,\Gam_{1};\Pi^{\{\cdot\}}$.
$(\mathcal{H}_{\gamma},\Theta; \mathtt{ Q}_{\Pi})\vdash^{* a+ b}_{c}\Gamma_{0},\Gam_{1};\Pi^{\{\cdot\}}$.
By induction on $b$ using
Lemma <ref> and Inversion <ref>.

$(\mathcal{H}_{\gamma},\Theta;\mathtt{Q}_{\Pi})\vdash^{* b(\iota)}_{c}C_{\iota},\Gam_{1};\Pi^{\{\cdot\}}$ for an $\iota\in J$.
We claim that $\iota\in[\mathtt{Q}_{\Pi}(\Tht)^{c}]_{C}J$.
We may assume that $\sfk(\iota)\subset\sfk(C_{\iota})$.
We obtain
$\iota^{-1}_{\mathtt{Q}_{\Pi}^{0,c}}\subset\calh_{\gam}[\Tht]\subset M_{\mathtt{Q}_{\Pi}}$ by (<ref>), (<ref>), Proposition <ref> and
$\gam\leq\gam_{0}\leq\mathtt{p}_{0}(\sig)$ for each $\sig\in\bigcup\mathtt{Q}_{\Pi}$.
Hence $\iota\in M^{-1}_{\mathtt{Q}_{\Pi}^{0,c}}\subset M^{-1}_{\mathtt{Q}_{\Pi}}$ and
$\mathtt{Q}_{\Pi}[\iota]=\mathtt{Q}_{\Pi}$, i.e., $\mathtt{R}[\iota]=\emptyset$.
Therefore $\iota\in[\mathtt{Q}_{\Pi}(\Tht)^{c}]_{C}J$.

Let $c\in\mathcal{H}_{\gamma}[\Theta]$ and
$(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* a}_{c+b}\Gamma;\Pi^{\{ \cdot \}}$,
where either $c\geq\mathbb{I}_{N}$ or $\lnot(c<\Omega<c+b)$.
Then $(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q}_{\Pi})\vdash^{* \varphi_{b}(a)}_{c}\Gamma;\Pi^{\{ \cdot \}}$.
By main induction on $b$ with subsidiary induction on $a$
using Reduction <ref>.

$A\in\Sigma(\mathcal{L}_{N+1})$ with $\rk(A)\leq\mI_{N}$,
$dom({\tt Q}_{\Pi})\subset \alpha<\beta\in\mathcal{H}_{\gamma}[\Theta]\cap\mI_{N}$, and
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi})\vdash^{* a}_{c}
\Gamma,A^{(\alpha,\mI_{N})};\Pi^{\{\cdot\}}$.

$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi})
\vdash^{* a}_{c}
\Gamma,A^{(\beta,\mI_{N})};\Pi^{\{\cdot\}}$.
This is seen by induction on $a$.
(<ref>) follows from $\beta\in\mathcal{H}_{\gamma}[\Theta]$.

$\Gamma\subset\Sigma(\mathcal{L}_{N+1})$ be a set of formulas.
\mathcal{H}_{\gamma}(\psi_{\mI_{N}}(\gamma))$
(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a}_{\mI_{N}}\Gamma;\Pi^{\{\cdot\}}
$\beta=\psi_{\mI_{N}}(\hat{a})$ with $\hat{a}=\gamma+\omega^{a}$.
$(\mathcal{H}_{\hat{a}+1},\Theta;{\tt Q}_{\Pi})
\vdash^{* \beta}_{\beta}
\Gamma^{(\beta,\mI_{N})};\Pi^{\{\cdot\}}$ holds.
By induction on $a$ as in [6].
We have
$\{\gamma, a\}\subset\mathcal{H}_{\gamma}[\Theta]$ by (<ref>),
$\beta=\psi_{\mI_{N}}(\hat{a})$ needs to be in $LSt_{N}$ due to the axiom (<ref>).

When the last inference is an $(i-{\rm stbl}(\mS))$, let
$B(0)\in\Delta_{0}(\mathcal{L}_{N+1})$ be a $\bigwedge$-formula with $\rk(B(0))<\mS$
and a term $u\in Tm(\mI_{N})$ such that
(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{0}}_{\mI_{N}}
\Gamma, B(u);\Pi^{\{\cdot\}}
$ for an ordinal $a_{0}\in\mathcal{H}_{\gamma}[\Theta]\cap a$.
Then we obtain for $\Theta(\mathtt{Q}_{\Pi})=\Tht\cup\bigcup_{\mT}\mathtt{Q}_{\Pi}(\mT)$,
${\sf k}(B(u))\subset \mathcal{H}_{\gamma}[\Theta(\mathtt{Q}_{\Pi})]$
by Proposition <ref> and the assumption $dom(\mathtt{Q}_{\Pi})\subset\gam$
with $\mathtt{Q}_{\Pi}(\mT)\subset \mT\in dom(\mathtt{Q}_{\Pi})$.
Hence $\Theta(\mathtt{Q}_{\Pi})\subset\mathcal{H}_{\gamma}(\psi_{\mI_{N}}(\gamma))$,
${\rm rk}(B(u))<\beta$ for $\rk(B(u))<\mI_{N}$.

Consider the case when the last inference is a $(\Sigma(St)\mbox{{\rm -rfl}})$ on $\mI_{N}$.
We have ordinals
$a_{\ell}, a_{r}<a$ and a formula $C\in\Sigma(\mathcal{L}_{N+1})$ such that
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{\ell}}_{\mI_{N}}\Gamma,C;\Pi^{\{\cdot\}}$
$(\mathcal{H}_{\gamma},\Theta;{\tt Q}_{\Pi}
)\vdash^{* a_{r}}_{\mI_{N}}
\lnot \exists x\,C^{(x,\mI_{N})} , \Gamma;\Pi^{\{\cdot\}}$.

Let $\beta_{\ell}=\psi_{\mI_{N}}(\widehat{a_{\ell}})\in\mathcal{H}_{\hat{a}+1}[\Theta]\cap\beta$ with
IH with $\Sigma$-persistency <ref> yields
$(\mathcal{H}_{\hat{a}+1},\Theta;\mathtt{ Q}_{\Pi}
)\vdash^{* \beta_{\ell}}_{\beta}\Gamma^{(\beta,\mI_{N})},
On the other, Inversion <ref> yields
$(\mathcal{H}_{\widehat{a_{\ell}}+1},\Theta;\mathtt{ Q}_{\Pi}
)\vdash^{* a_{r}}_{\mI_{N}}
\lnot C^{(\beta_{\ell},\mI_{N})} , \Gamma;\Pi^{\{\cdot\}}$.
For $\beta_{r}=\psi_{\mI_{N}}(\widehat{a_{r}})\in\mathcal{H}_{\hat{a}+1}[\Theta]\cap\beta$
with $\widehat{a_{r}}=\widehat{a_{\ell}}+\omega^{a_{r}}$, IH yields
$(\mathcal{H}_{\hat{a}+1},\Theta;\mathtt{ Q}_{\Pi}
)\vdash^{* \beta_{r}}_{\beta}
\lnot C^{(\beta_{\ell},\mI_{N})} , \Gamma^{(\beta,\mI_{N})}; \Pi^{\{\cdot\}}$.
We obtain
$(\mathcal{H}_{\hat{a}+1},\Theta;\mathtt{ Q}_{\Pi}
)\vdash^{* \beta}_{\beta}
\Gamma^{(\beta,\mI_{N})};\Pi^{\{\cdot\}}$
by a $(cut)$.

$\Gamma\subset\Sigma(\mathcal{L}_{0}:\Omega)$ be a set of formulas.
\mathcal{H}_{\gamma}(\psi_{\Omega}(\gamma))$
(\mathcal{H}_{\gamma},\Theta; \emptyset
)\vdash^{* a}_{\Omega,\gamma_{1}}\Gamma;\emptyset
$\beta=\psi_{\Omega}(\hat{a})$ with $\hat{a}=\gamma+\omega^{a}<\gamma_{1}$.
$(\mathcal{H}_{\hat{a}+1},\Theta; \emptyset)
\vdash^{* \beta}_{\beta,\gamma_{1}}
\Gamma^{(\beta,\Omega)};\emptyset$ holds.
By induction on $a$ as in [6].

§.§ Operator controlled derivations with caps

Let us fix an ordinal $\gam_{0}\in\calh_{0}$ and a strongly critical number
which depend on a given finite proof figure, and will be specified in the end of the next section <ref>.
$\Lambda$ is the base of the $\tilde{\theta}$-function
$\tilde{\theta}_{b}(\xi)=\tilde{\theta}_{b}(\xi;\Lambda)$ in Definition <ref>.
<ref> and <ref> depend on the ordinals $\gam_{0},\Lambda$.

By a capped formula we mean a pair $(A,\rho)$ of $RS$-sentence $A$
and an ordinal $\rho\prec\mathbb{S}$ with a successor stable ordinal $\mS$
such that
${\sf k}(A)\subset M_{\rho}$ and
Such a pair is denoted by $A^{(\rho)}$.
It is convenient for us to regard uncapped formulas $A$ as capped formulas
$A^{({\tt u})}$ with its cap ${\tt u}$, where

A sequent is a finite set of capped or uncapped formulas, denoted by
$\Gamma_{0}^{(\rho_{0})},\ldots,\Gamma_{n}^{(\rho_{n})},\Pi^{({\tt u})}$,
where each formula in the set $\Gamma_{i}^{(\rho_{i})}$ puts on the cap
When we write $\Gamma^{(\rho)}$, we tacitly assume that
${\sf k}(\Gamma)\subset M_{\rho}$
with $M_{{\tt u}}=OT(\mI_{N})\cap\mI_{N}$.

A capped formula $A^{(\rho)}$ is said to be a $\Sigma(\mathcal{L}_{i}: \pi)$-formula if
Let $\sfk(A^{(\rho)}):=\sfk(A)$.

A pair $\mathtt{ Q}=((\mathtt{ Q})_{0},
\gam_{\cdot}^{\mathtt{ Q}})$
is said to be a finite family for a pair $(e,\gamma_{0})$ of ordinals
if $(\mathtt{ Q})_{0}$ is a finite family in the sense of Definition <ref> and the following conditions are met.

Let $dom(\mathtt{Q})=dom((\mathtt{Q})_{0})$,
$dom_{e}(\mathtt{Q})=\{\mS\in dom(\mathtt{Q}):\mS<e\}$, cf. Lemma <ref>,
$\mathtt{ Q}(\mS)=(\mathtt{ Q})_{0}(\mS)$.
$\bigcup_{e}\mathtt{ Q}=\bigcup\{\mathtt{Q}(\mS):\mS<e\}$.

$\gam_{\cdot}^{\mathtt{ Q}}$ is a map $dom_{e}(\mathtt{ Q})\ni\mS\mapsto\gam_{\mS}^{\mathtt{ Q}}$ such that
$\gam_{0}+(\mI_{N})^{2}>\gam^{\mathtt{ Q}}_{\mS}\geq \gam_{0}+\mI_{N}$,
$\gam^{\mathtt{ Q}}_{\mS}\geq \gam^{\mathtt{ Q}}_{\mT}+\mI_{N}$ for $\{\mS<\mT\}\subset dom_{e}(\mathtt{ Q})$.

$\mathtt{Q}$ is said to have gaps $\eta$ if
$\gam^{\mathtt{ Q}}_{\mS}\geq \gam^{\mathtt{ Q}}_{\mT}+\mI_{N}\cdot\eta$ holds
for $\{\mS<\mT\}\subset dom_{e}(\mathtt{ Q})$, and
$\gam^{\mathtt{ Q}}_{\mS}\geq \gam_{0}+\mI_{N}\cdot\eta$ for $\mS\in dom_{e}(\mathtt{ Q})$.

For each $\rho\in\mathtt{ Q}(\mS)$,
\to\vphi_{\Lambda}(0)$ is special,
and $\gam_{\mS}^{\mathtt{ Q}}\leq\mathtt{ p}_{0}(\rho)$.

* For a finite family $\mathtt{Q}$ for $(e,\gam_{0})$ and a pair $(\mS,\rho)$ such that
$(\mathtt{Q})_{0}\cup\{(\mS,\rho)\}$ is a finite family for $\gam_{0}$,
$\mathtt{Q}\cup\{(\mS,\rho)\}=\mathtt{ R}=((\mathtt{ R})_{0},
\gam^{\mathtt{ R}}_{\cdot})$
denotes a finite family for
$(e,\gam_{0})$ enjoying the following:

* $dom(\mathtt{ R})=dom(\mathtt{ Q})\cup\{\mS\}$,
$\mathtt{ R}(\mT)=\mathtt{ Q}(\mT)$ for $\mT\neq\mS$ and
$\mathtt{ R}(\mS)=\mathtt{Q}(\mS)\cup\{\rho\}$.

* $\gam^{\mathtt{ R}}_{\cdot}$ extends $\gam^{\mathtt{ Q}}_{\cdot}$ in such a way that
$\gam^{\mathtt{ R}}_{\mT}=\gam^{\mathtt{ Q}}_{\mT}$ for $\mT\in dom_{e}(\mathtt{ Q})$,
$\gam^{\mathtt{ R}}_{\mS}\geq\gam^{\mathtt{ Q}}_{\mT}+\mI_{N}$ for every $\mS<\mT\in dom_{e}(\mathtt{ Q})$,
$\gam^{\mathtt{ Q}}_{\mU}\geq\gam^{\mathtt{ R}}_{\mS}+\mI_{N}$ for every $\mS>\mU\in dom_{e}(\mathtt{ Q})$,
and $\gam^{\mathtt{ R}}_{\mS}\geq\gam_{0}+\mI_{N}$.

A pair $\mathtt{ Q}=((\mathtt{Q})_{0},
\gam^{\mathtt{ Q}}_{\cdot})$
is simply denoted by $\mathtt{ Q}$
$\gam^{\mathtt{ Q}}_{\cdot}$
is irrelevant.

Let for $\rho\in OT(\mI_{N})\cup\{\mathtt{u}\}$, cf. Definition <ref>.<ref>:

[Q()]_A^(ρ)J = [Q()]_¬A^(ρ)J : =
$[\mathtt{u}]J=J$ with $M_{\mathtt{u}}=OT(\mI_{N})\cap\mI_{N}$.

Let $\rho\in\Psi_{\mS}$.

$\kappa\in L^{\mathtt{ Q}}_{\rho}(\Tht)$ iff
\{\mathtt{ p}_{0}(\rho)\}\cup
\cup(\mathtt{Q}(\mS)\cap\rho)
\subset M_{\kappa}$,
$\gam_{\mS}^{\mathtt{Q}}\leq\mathtt{ p}_{0}(\kappa)\leq\mathtt{ p}_{0}(\rho)$,
\mathcal{H}_{\gam^{\mathtt{R}}_{\mS}+\mI_{N}}[\Theta]$,
$\fal\mT<\mS(\kap\in M_{\mathtt{Q}(\mT)})$,
$m(\kappa)$ is special such that
$SC_{\Lambda}(m(\kappa))\subset M_{\mathtt{ Q}(\mT)}$ for every
$\{\mT\leq\mS\}\subset dom(\mathtt{Q})$.

$H^{\mathtt{ Q}}_{\rho}(d,f,\Theta)$
denotes the resolvent class defined by
$\kappa\in H^{\mathtt{ Q}}_{\rho}(d,f,\Theta)$ iff
$\kappa\in L^{\mathtt{ Q}}_{\rho}(\Tht)$,
$m(\kappa)\in H_{\rho}(d,f)$, cf. Definition <ref>.<ref>.

Let $\Gamma$ be a sequent,
$\Theta$ a finite set of ordinals$<\mI_{N}$,
$\{\gamma, a,c,s,e\}\subset OT(\mI_{N})$, and
$\mathtt{ Q}$ a finite family for $(e,\gamma_{0})$.

We define another derivability  relation $(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q}
$c$ is a bound of ranks of cut formulas,
$e$ a bound of ordinals $\mS$,
$d$ a bound of ranks
in the inference rules $(i-{\rm rfl}_{\mS}(\rho,s,f))$.
The relation depends on an ordinal $\gam_{0}$, and
should be written as $(\mathcal{H}_{\gamma},\Theta;\mathtt{ Q})\vdash^{a}_{c,d,e,\gam_{0}}\Gamma$.
However the ordinal $\gam_{0}$ will be fixed.
So let us omit it.

Let $\mathtt{ Q}=((\mathtt{ Q})_{0},
\gam^{\mathtt{ Q}}_{\cdot}
)$ be a finite family for
$(e,\gamma_{0})$, and
$a,c,d,e$ ordinals with $d,e<\Lambda$.
$\Gamma=\bigcup\{\Gam_{\sig}^{(\sig)}:\sig\in\{\mathtt{ u}\}\cup\bigcup_{e}\mathtt{ Q}\}$
be a set of formulas
such that ${\sf k}(\Gamma_{\sigma})\subset M_{\sigma}$
for each $\sigma\in\bigcup_{e}\mathtt{ Q}$.

$(\mathcal{H}_{\gamma},\Tht, \mathtt{ Q})\vdash^{a}_{c,d,e} \Gamma$ holds
$\gam\leq\gam_{0}$, cf. (<ref>), (<ref>) and (<ref>),

\begin{equation}
\label{eq:controlder_cap4}
\Tht\subset M_{\mathtt{Q}}
\end{equation}

\begin{equation}
\label{eq:controlder_cap3}
\{\gamma,a,c,d,e\}
\cup dom_{e}(\mathtt{Q})\cup\{\gamma^{\mathtt{Q}}_{\mS}: \mS\in dom_{e}(\mathtt{Q})\}
\subset\mathcal{H}_{\gamma}[\Theta]
\end{equation}

\begin{equation}
\label{eq:controlder_cap1}
\fal\mS\in dom_{e}(\mathtt{Q})\cup\{0\}
\left(
(\sfk^{\mS}(\Gam))^{-1}_{\mathtt{Q}^{\mS,e}}\subset \mathcal{H}_{\gamma}[\Tht]
\right)
\end{equation}

\begin{equation}
\label{eq:controlder_cap5}
\fal \mS\in dom_{e}(\mathtt{Q})
\left(
\mathtt{Q}(\mS)\subset
\mathcal{H}_{\gam^{\mathtt{ Q}}_{\mS}+\mI_{N}}[\Theta]
\right)
\end{equation}

and one of the following cases holds:

$\{\lnot A^{(\rho)},A^{(\rho)}\}\subset\Gam$ for
a $\rho\in\{\mathtt{ u}\}\cup\bigcup_{e}\mathtt{ Q}$ and a formula $A$ such that $\rk(A)<\mS$
for a successor stable ordinal $\mS\in dom_{e}(\mathtt{Q})$.

There exist $A\simeq\bigvee(A_{\iota})_{\iota\in J}$, a cap $\rho\in\{\mathtt{ u}\}\cup\bigcup_{e}\mathtt{ Q}$,
an ordinal
$a(\iota)<a$ and an
$\iota\in [\rho]J$
such that
$A^{(\rho)}\in\Gamma$ and
$(\mathcal{H}_{\gamma},\Tht,\mathtt{ Q})\vdash^{a(\iota)}_{c,d,e}\Gamma,
\left(A_{\iota}\right)^{(\rho)}$.

There exist
$A\simeq\bigwedge(A_{\iota})_{ \iota\in J}$ and  a cap $\rho\in\{\mathtt{ u}\}\cup\bigcup_{e}\mathtt{ Q}$ such that
For each $\iota\in[\mathtt{Q}(\Tht)]_{A^{(\rho)}} J$ there exists an ordinal $a(\iota)<a$ such that
$(\mathcal{H}_{\gamma},\Tht\cup \iota^{-1}_{\mathtt{Q}}\cup dom(\mathtt{R}[\iota]), \mathtt{ Q}]\iota]
\vdash^{a(\iota)}_{c,d,e}\Gamma,
\left(A_{\iota}\right)^{(\rho)}$, where
$\mathtt{Q}[\iota]=\mathtt{Q}\cup\mathtt{R}[\iota]$ and $\mathtt{Q}\cap\mathtt{R}[\iota]=\emptyset$.

There exist $\rho\in\{\mathtt{ u}\}\cup\bigcup_{e}\mathtt{ Q}$, an ordinal $a_{0}<a$ and a formula $C$
such that
$(\mathcal{H}_{\gamma},\Tht, \mathtt{ Q})\vdash^{a_{0}}_{c,d,e}\Gamma,\lnot C^{(\rho)}$
$(\mathcal{H}_{\gamma},\Tht, \mathtt{ Q})\vdash^{a_{0}}_{c,d,e}C^{(\rho)},\Gamma$
with $\mbox{{\rm rk}}(C)<c$.

$(\Sigma(\Ome)\mbox{{\rm -rfl}})$
There exist ordinals
$a_{\ell}, a_{r}<a$ and an uncapped formula $C\in\Sigma(\mathcal{L}_{0}:\Ome)$
such that
$c\geq \Ome$,
$(\mathcal{H}_{\gamma},\Tht, \mathtt{ Q}
$(\mathcal{H}_{\gamma},\Tht, \mathtt{ Q}
\lnot \exists x<\pi\,C^{(x,\Ome)}, \Gamma$.

$(i {\rm -rfl}_{\mS}(\rho,s,f))$
There exist
a successor $i$-stable ordinal $e>\mS\in\mathcal{H}_{\gam}[\Tht]$
an ordinal $\rho\in\Psi_{\mS}$ for which the following holds:

Let $\mathtt{ P}=\mathtt{Q}\cup\{(\mS,\rho)\}$.

Also there exist
an ordinal
$s\in {\rm supp}(m(\rho))$,
a special function $f$ with $s(\rho),s(f)\leq d<\Lambda$,
an ordinal $a_{0}<a$,
and an $\mathcal{L}_{i}$-formula $\del$, which is a $\bigwedge$-formula
with $\del\simeq\bigwedge(\del_{\iota})_{\iota\in J}$
enjoying the following conditions
(r1), (r2), (r3) and (r4).

For $g=m(\rho)$,
f_{s}=g_{s} \,\&\, f^{s}<_{\Lambda}^{s} g^{\prime}(s)$,
cf. Definition <ref>.<ref>.

For each $\iota\in[\mathtt{R}(\Tht)]_{\del^{(\rho)}}J$ and
$\Tht_{\iota}=\Theta\cup \iota^{-1}_{\mathtt{R}}\cup dom(\mathtt{R}[\iota])$
$(\mathcal{H}_{\gamma},\Tht_{\iota}, \mathtt{ P}[\iota]
)\vdash^{a_{0}}_{c,d,e}\Gamma, \delta_{\iota}^{(\rho)}$ and cf. (<ref>),

\mathtt{ P}^{\sig}
)\vdash^{a_{0}}_{c,d,e}\Gamma, \lnot\delta^{(\sig)}$ holds
for every $\sigma\in H^{\mathtt{ R}}_{\rho}(d,f,\Tht)$, where
$(\mathtt{ P}^{\sig})_{0}=(\mathtt{P})_{0}\cup\{(\mS,\sig)\}$ and

\[
\hspace{-10mm}
\infer[(i-{\rm rfl}_{\mS}(\rho,s,f))]{(\mathcal{H}_{\gamma},\Tht,
\mathtt{ Q}
\{
)\vdash^{a_{0}}_{c,d,e}\Gamma, \delta_{\iota}^{(\rho)}
\}_{\iota}
\{
\mathtt{ P}^{\sig}
\}_{\sig}
\]

In this subsection the ordinals $d$ and $\gam_{0}$ will be fixed, and
we write $\vdash^{a}_{c,e}$ for $\vdash^{a}_{c,d,e,\gam_{0}}$.
Note that
need not to hold.

Let $(\mathcal{H}_{\gamma},\Tht, \mathtt{ Q})\vdash^{a}_{c,e}\Gamma$.
Let $\mS\in\mathcal{H}_{\gam}[\Tht]$.
$\rho\in\Psi_{\mS}$ be an ordinal such that
$\{\mS,\gam_{\mS}^{\mathtt{P}}\}\subset \mathcal{H}_{\gamma}[\Theta]$
$\Tht\subset M_{\rho}$, cf. (<ref>),
$\mathtt{P}=\mathtt{Q}\cup\{(\mS,\rho)\}$, $\mathtt{P}^{\sig}=\mathtt{P}\cup\{(\mS,\sig)\}$ are finite families
determined from $\mathtt{ Q},\rho$ and
$\sigma\in L^{\mathtt{P}}_{\rho}(\Tht)$ in the inference $(i-{\rm rfl}_{\mS}(\rho,s,f))$.
$(\mathcal{H}_{\gamma},\Tht, \mathtt{P})\vdash^{a}_{c,e}\Gamma$
$(\mathcal{H}_{\gamma},\Tht, \mathtt{P}^{\sig})\vdash^{a}_{c,e}\Gamma$.
By induction on $a$ as in Lemma <ref> using
Proposition <ref>.

For $\rho_{1}\in\Psi_{\mS_{1}}$ with $\mS_{1}>\mS$, we obtain
$L^{\mathtt{P}^{\sig}}_{\rho_{1}}(\Tht)\subset L^{\mathtt{P}}_{\rho_{1}}(\Tht)\subset L_{\rho_{1}}^{\mathtt{Q}}(\Tht)$, and need to prune some branches at
$(i_{1}-{\rm rfl}_{\mS_{1}}(\rho_{1},s_{1},f_{1}))$.
By $\Tht\subset M_{\rho}\cap M_{\sig}$,
each of (<ref>) and
(<ref>) holds in
$(\mathcal{H}_{\gamma},\Tht, \mathtt{P})\vdash^{a}_{c,e}\Gamma$
and in
$(\mathcal{H}_{\gamma},\Tht, \mathtt{P}^{\sig})\vdash^{a}_{c,e}\Gamma$.

Let $C\simeq\bigvee(C_{\iota})_{\iota\in J}$,
$\Ome\leq\mbox{{\rm rk}}(C)\leq c<\mI_{N}$ and $dom_{e}(\mathtt{Q})\cap (c,e)=\emptyset$.
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a}_{c,e}\Gamma_{0},\lnot C^{(\tau)}$
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{b}_{c,e}C^{(\tau)},\Gam_{1}$.
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a\# b}_{c,e}\Gamma_{0},\Gam_{1}$
for the natural sum $a\#b$ of ordinals $a$ and $b$.
By induction on $a\#b$ using
Lemma <ref>.
We may assume that $\rk(C)=c$, and we see that
$C^{(\tau)}$ is not introduced by any (Taut)
from the assumption $dom_{e}(\mathtt{Q})\cap(c,e)=\emptyset$.

Case 1. The last inference in
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a}_{c,e}\Gamma_{0},\lnot C^{(\tau)}$ is a
$(\bigwedge)$ with its major formula $\lnot C^{(\tau)}$,
and one in
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{b}_{c,e}C^{(\tau)},\Gam_{1}$
is a
$(\bigvee)$ with its major formula $C^{(\tau)}$:
We have
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{b(\iota)}_{c,e}
\left(C_{\iota}\right)^{(\tau)},C^{(\tau)},\Gam_{1}$
for an
$\iota\in [\tau]J$ and a $b(\iota)<b$.
We obtain
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a\#b(\iota)}_{c,e}
\left(C_{\iota}\right)^{(\tau)},\Gam_{0},\Gam_{1}$ by IH.

We claim that $\iota\in[\mathtt{Q}(\Tht)]_{C^{(\tau)}}J$, cf. (<ref>).
We may assume that $\sfk(\iota)\subset\sfk(C_{\iota})$.
By (<ref>) and (<ref>)
with $\gam\leq\gam_{0}\leq\mathtt{p}_{0}(\sig)$ for every $\sig\in\bigcup_{e}\mathtt{Q}$
we obtain
$(\sfk^{0}(C_{\iota}))^{-1}_{\mathtt{Q}^{0,e}}\subset \mathcal{H}_{\gamma}[\Tht]\subset M_{\mathtt{Q}}$.
This yields
$\iota\in M^{-1}_{\mathtt{Q}}$ and $\mathtt{R}[\iota]\subset\mathtt{Q}$.
Hence $\Tht\subset M_{\mathtt{R}[\iota]}$ and $dom(\mathtt{R}[\iota])\subset M_{\mathtt{Q}}\cap e$,
and $\iota\in[\mathtt{Q}(\Tht)]_{C^{(\tau)}}J$ follows.

On the other hand we have
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a(\iota)}_{c,e}\Gamma_{0},\lnot C^{(\tau)},\lnot(C_{\iota})^{(\tau)}$ for an $a(\iota)<a$ with $\iota\in[\mathtt{Q}(\Tht)]_{C^{(\tau)}}J$.
IH yields
$(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a(\iota)\# b}_{c,e}\Gamma_{0},\Gam_{1},\lnot(C_{\iota})^{(\tau)}$.
We obtain  $(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a\# b}_{c,e}\Gamma_{0},\Gam_{1}$
by a $(cut)$ with $\rk(C_{\iota})<\rk(C)=c$.
Suppressing the part $(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})$, let us depict it as follows.

\[
\hspace{-5mm}
\infer[(cut)]{(\mathcal{H}_{\gamma},\Theta, \mathtt{ Q})\vdash^{a\# b}_{c,e}\Gamma_{0},\Gam_{1}}
\infer[\mathrm{IH}]{\vdash^{a(\iota)\# b}_{c,e}\Gamma_{0},\Gam_{1},\lnot(C_{\iota})^{(\tau)}}
\vdash^{a(\iota)}_{c,e}\Gamma_{0},\lnot C^{(\tau)},\lnot(C_{\iota})^{(\tau)}
\vdash^{b}_{c,e}C^{(\tau)},\Gam_{1}
\infer[\mathrm{IH}]{\vdash^{a\#b(\iota)}_{c,e}
\left(C_{\iota}\right)^{(\tau)},\Gam_{0},\Gam_{1}}