[proofplan] The proof isolates the particular reducible cut occurrence transformed by the chosen one-step reduction and writes the whole proof as a one-hole proof context applied to that local redex. The theorem's hypotheses include the clause-by-clause local decrease property for Gentzen's ordinal assignment, so the reduct has strictly smaller local ordinal than the redex. The context monotonicity hypothesis for the recursive clauses defining $o$ then propagates this strict decrease through the unchanged surrounding proof tree; membership in $\mathcal O_{<\varepsilon_0}$ gives the upper bound. [/proofplan] [step:Declare the proof context and the local redex] Let $\mathcal P$ denote the set of proof trees in the fixed Gentzen sequent calculus, and let $\mathcal O_{<\varepsilon_0}$ denote the ordinal notation system below $\varepsilon_0$ used by the assignment. The theorem gives a map \begin{align*} o: \mathcal P &\to \mathcal O_{<\varepsilon_0}. \end{align*} Let $\pi \in \mathcal P$ contain a reducible cut, and suppose $\pi \rightsquigarrow \pi'$ is one step of the specified [Gentzen cut reduction](/page/Gentzen%20Cut%20Reduction). By the definition of the chosen one-step relation $\pi \rightsquigarrow \pi'$, this reduction selects one occurrence of a reducible cut subtree $\rho \in \mathcal P$, replaces it by its one-step reduct $\rho' \in \mathcal P$, and leaves the rest of the proof tree unchanged. Hence there is a one-hole proof context $C[-]$ such that \begin{align*} \pi = C[\rho], \qquad \pi' = C[\rho']. \end{align*} The context $C[-]$ is the proof tree obtained from $\pi$ by replacing the selected occurrence of the redex by a hole; it has the same inference labels and side subproofs as $\pi$ outside that selected reducible cut. [guided] We first separate the part of the proof that changes from the part that does not. Let $\mathcal P$ denote the set of proof trees in the fixed Gentzen sequent calculus, and let $\mathcal O_{<\varepsilon_0}$ denote the ordinal notation system below $\varepsilon_0$ used by the assignment. The theorem gives a map \begin{align*} o: \mathcal P &\to \mathcal O_{<\varepsilon_0}. \end{align*} Let $\pi \in \mathcal P$ contain a reducible cut, and suppose $\pi \rightsquigarrow \pi'$ is one step of the specified [Gentzen cut reduction](/page/Gentzen%20Cut%20Reduction). The reduction step may be available at several cut occurrences in $\pi$, so uniqueness is only relative to the chosen step $\pi \rightsquigarrow \pi'$. For that chosen step, the definition of $\rightsquigarrow$ selects one reducible cut subtree $\rho \in \mathcal P$, replaces it by a one-step reduct $\rho' \in \mathcal P$, and leaves all inference labels and side subproofs outside that occurrence unchanged. Therefore there is a one-hole proof context $C[-]$ satisfying \begin{align*} \pi = C[\rho], \qquad \pi' = C[\rho']. \end{align*} Here $C[-]$ records exactly the surrounding inference steps and side subproofs. This reduction to a local comparison is essential because Gentzen's ordinal assignment is recursive on proof trees: after the ordinal assigned to the changed subtree is known to decrease, the monotonicity of the surrounding recursive clauses transfers that decrease to the whole proof. [/guided] [/step] [step:Invoke the stated local decrease clause for the selected redex] The statement assumes the clause-by-clause local decrease property for the specified [Gentzen cut reduction](/page/Gentzen%20Cut%20Reduction) and the associated ordinal assignment $o$. Applied to the selected redex $\rho \in \mathcal P$ and its one-step reduct $\rho' \in \mathcal P$, this hypothesis gives \begin{align*} o(\rho') < o(\rho). \end{align*} This invocation is legitimate because $\rho \rightsquigarrow \rho'$ is exactly one of the local redex-reduct pairs selected by the global reduction $\pi \rightsquigarrow \pi'$. [guided] We now use the defining compatibility between the specified [Gentzen cut reduction](/page/Gentzen%20Cut%20Reduction) and the ordinal assignment $o$. The theorem statement explicitly assumes the clause-by-clause local decrease property: whenever a local redex $\sigma \in \mathcal P$ is replaced by its one-step reduct $\sigma' \in \mathcal P$ under one of the specified reduction clauses, the assigned ordinal strictly decreases, \begin{align*} o(\sigma') < o(\sigma). \end{align*} In the previous step, the chosen global reduction $\pi \rightsquigarrow \pi'$ was decomposed as \begin{align*} \pi = C[\rho], \qquad \pi' = C[\rho'], \end{align*} where $\rho \in \mathcal P$ is the selected local redex and $\rho' \in \mathcal P$ is its one-step reduct. Therefore the hypothesis applies with $\sigma = \rho$ and $\sigma' = \rho'$. Substituting these symbols into the local decrease property gives \begin{align*} o(\rho') < o(\rho). \end{align*} No additional reduction clause is being suppressed here: the clause-by-clause verification is part of the hypotheses on the fixed ordinal assignment, and this step records the exact instance of that hypothesis needed for the selected redex. [/guided] [/step] [step:Propagate the strict local decrease through the unchanged context] The statement assumes that every one-hole proof context operation induced by the recursive definition of $o$ is monotone in all side-premise arguments and strictly monotone in the distinguished premise occupied by the hole. Since the side subproofs in $C[-]$ are unchanged and $o(\rho') < o(\rho)$, induction on the height of the context $C[-]$ gives \begin{align*} o(C[\rho']) < o(C[\rho]). \end{align*} Using $\pi = C[\rho]$ and $\pi' = C[\rho']$, this is \begin{align*} o(\pi') < o(\pi). \end{align*} [guided] The local inequality must now be lifted through the rest of the proof tree. The context $C[-]$ is built by stacking inference rules above the hole and attaching side subproofs that are identical in $C[\rho]$ and $C[\rho']$. At each inference node, the recursive definition of $o$ applies an ordinal operation to the ordinals of the immediate premises. The theorem statement assumes that each such operation is monotone in every side-premise argument and strictly monotone in the argument corresponding to the premise containing the hole. We prove the context comparison by induction on the number of inference nodes of $C[-]$ above the hole. If the context is just the hole, then the claim is exactly the local inequality \begin{align*} o(\rho') < o(\rho). \end{align*} For the induction step, write the top inference of the context as an ordinal operation $F$ applied to the hole-premise ordinal and to fixed side-premise ordinals $\alpha_1, \dots, \alpha_m \in \mathcal O_{<\varepsilon_0}$. By the induction hypothesis, the ordinal in the hole-premise position is smaller for $C[\rho']$ than for $C[\rho]$, while each side-premise ordinal $\alpha_j$ is unchanged. Strict monotonicity of $F$ in the hole-premise argument gives the strict inequality at the top node. Therefore \begin{align*} o(C[\rho']) < o(C[\rho]). \end{align*} Substituting $\pi' = C[\rho']$ and $\pi = C[\rho]$ yields $o(\pi') < o(\pi)$. [/guided] [/step] [step:Use the codomain of the ordinal assignment to obtain the bound below $\varepsilon_0$] Because $o$ is a map from $\mathcal P$ to $\mathcal O_{<\varepsilon_0}$ and $\pi \in \mathcal P$, the ordinal notation $o(\pi)$ lies below $\varepsilon_0$: \begin{align*} o(\pi) < \varepsilon_0. \end{align*} Combining this with the strict decrease proved above gives \begin{align*} o(\pi') < o(\pi) < \varepsilon_0. \end{align*} This is the asserted decrease for one step of Gentzen reduction. [/step]