ch:inference-rules: ch:inference-rules

Take three judgments $P,Q,R$ and the one-rule system

The sets $S=\{P\}$ and $T=\{Q\}$ are each closed: in either set at least one premise of the rule is absent. Their union contains both premises but not the conclusion, and therefore is not closed. This also explains why intersections, rather than unions, occur in proposition 1.5.

The grammar is presented by the three rules

Writing $\overline{1}=\mathsf{suc}(\mathsf{0})$ and using the metalevel operation $\oplus$ defined in the exercise, the required relation is generated by

Rule induction shows simultaneously that a derivable length judgment has a combinator as its first subject and that its second subject is precisely the number of leaves labeled $\mathsf{s}$ or $\mathsf{k}$.

Every node in the numeral-equality derivation is forced: $$\frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{is}\mathsf{0}}}\mathrm{Is}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{is}\mathsf{suc}(\mathsf{0})}}\mathrm{Is}-\mathrm{S}}{\mathsf{suc}(\mathsf{suc}(\mathsf{0}))\mathsf{is}\mathsf{suc}(\mathsf{suc}(\mathsf{0}))}\mathrm{Is}-\mathrm{S}.$$ The tree derivation uses one axiom for each empty subtree and one Tree-Node for each node: $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\mathsf{emp}\mathsf{tree}}}\mathrm{Tree}-\mathrm{Emp}\\ {\displaystyle \frac{\phantom{X}}{\mathsf{emp}\mathsf{tree}}}\mathrm{Tree}-\mathrm{Emp}\end{array}}{\mathsf{node}(\mathsf{emp};\mathsf{emp})\mathsf{tree}}}\mathrm{Tree}-\mathrm{Node}\\ {\displaystyle \frac{\phantom{X}}{\mathsf{emp}\mathsf{tree}}}\mathrm{Tree}-\mathrm{Emp}\end{array}}{\mathsf{node}(\mathsf{node}(\mathsf{emp};\mathsf{emp});\mathsf{emp})\mathsf{tree}}\mathrm{Tree}-\mathrm{Node}.$$

The only conclusions of the equality rules are $\mathsf{0}\mathsf{is}\mathsf{0}$ and $\mathsf{suc}(a)\mathsf{is}\mathsf{suc}(b)$. Hence no rule instance has conclusion $\mathsf{suc}(\mathsf{0})\mathsf{is}\mathsf{0}$, so a finite derivation of that judgment has no possible final rule.

Likewise, the outer successor on both sides of $\mathsf{suc}(a)\mathsf{is}\mathsf{suc}(b)$ excludes Is-Z. Its final rule must therefore be $$\frac{a\mathsf{is}b}{\mathsf{suc}(a)\mathsf{is}\mathsf{suc}(b)}\mathrm{Is}-\mathrm{S}.$$ Thus the derivation contains a derivation of $a\mathsf{is}b$ as its immediate subtree.

For reflexivity, induct on $a\mathsf{nat}$. The Nat-Z case is Is-Z. If the premise derivation gives, by induction, $a\mathsf{is}a$, then Is-S gives $\mathsf{suc}(a)\mathsf{is}\mathsf{suc}(a)$.

For transitivity, induct on the derivation of $a\mathsf{is}b$. If it ends in Is-Z, then $a=b=\mathsf{0}$. Final-rule inspection of $\mathsf{0}\mathsf{is}c$ forces Is-Z, hence $c=\mathsf{0}$, and Is-Z proves the result. In the successor case the two derivations have the shapes $$\frac{a_0\mathsf{is}{b}_0}{\mathsf{suc}(a_0)\mathsf{is}\mathsf{suc}(b_0)}\mathrm{Is}-\mathrm{S},\frac{b_0\mathsf{is}{c}_0}{\mathsf{suc}(b_0)\mathsf{is}\mathsf{suc}(c_0)}\mathrm{Is}-\mathrm{S}.$$ The induction hypothesis derives $a_0\mathsf{is}{c}_0$, and Is-S derives the required successor judgment.

Finally, the outer form of $\mathsf{suc}(a)\mathsf{is}\mathsf{suc}(b)$ excludes Is-Z; the final rule is Is-S, and its premise is exactly $a\mathsf{is}b$. This proves successor injectivity.

Only Ev-S concludes a judgment whose subject is a successor and whose tag is $\mathsf{even}$. Thus a derivation of $\mathsf{suc}(a)\mathsf{even}$ has immediate premise $a\mathsf{odd}$. Similarly, only Od-S can conclude $\mathsf{suc}(a)\mathsf{odd}$, and its premise is $a\mathsf{even}$.

Assume for contradiction that both $a\mathsf{even}$ and $a\mathsf{odd}$ are derivable. Either derivation gives $a\mathsf{nat}$ by lemma 1.24. Induct on that numeral derivation. If $a=\mathsf{0}$, no rule concludes $\mathsf{0}\mathsf{odd}$. If $a=\mathsf{suc}(b)$, the two inversion facts extract both $b\mathsf{odd}$ and $b\mathsf{even}$. The induction hypothesis for the predecessor derivation rules this out. Hence no expression has both parity tags.

The complete tree is $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{nat}}}\mathrm{Nat}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{nat}}}\mathrm{Nat}-\mathrm{S}}{\mathsf{sum}(\mathsf{0};\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0}))}}\mathrm{Sum}-\mathrm{Z}}{\mathsf{sum}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{suc}(\mathsf{0})))}}\mathrm{Sum}-\mathrm{S}}{\mathsf{sum}(\mathsf{suc}(\mathsf{suc}(\mathsf{0}));\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{suc}(\mathsf{suc}(\mathsf{0}))))}\mathrm{Sum}-\mathrm{S}.$$ Deleting the final Sum-S leaves $$\mathsf{sum}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{suc}(\mathsf{0})))$$ at the root. This premise is forced: Sum-Z can conclude only a sum whose first argument is $\mathsf{0}$, so the displayed successor-headed conclusion can only arise from Sum-S. Matching that rule against the conclusion uniquely determines the premise above.

Let ${\mathcal{E}}_i$ derive $K_i$ from $\mathrm{\Gamma }$. For the iterated proof, weaken ${\mathcal{E}}_1$ to the ambient hypotheses $\mathrm{\Gamma },K_2,\dots ,K_n$ and apply transitivity to discharge $K_1$. The result derives $J$ from $\mathrm{\Gamma },K_2,\dots ,K_n$. Repeat with ${\mathcal{E}}_2$, and so on. After $n$ applications, the result derives $J$ from $\mathrm{\Gamma }$.

For the single proof, induct on the given derivation $\mathcal{D}$ of $J$ from $\mathrm{\Gamma },K_1,\dots ,K_n$. A hypothesis leaf from $\mathrm{\Gamma }$ is retained. A leaf $K_i$ is replaced by the fixed tree ${\mathcal{E}}_i$. At a primitive-rule node, transform every immediate subderivation by the induction hypotheses and reapply the same rule. Every new leaf is now justified by $\mathrm{\Gamma }$, and every internal node has the same conclusion as before, so the transformed root is a derivation of $J$ from $\mathrm{\Gamma }$.

One direction is immediate: every $\mathcal{R}$-derivation is also an $\mathcal{R}\cup \{r\}$-derivation. Conversely, induct on a derivation over $\mathcal{R}\cup \{r\}$. If its final rule lies in $\mathcal{R}$, transform its premises by the induction hypotheses and reapply that rule. For a two-premise instance of $r$, the induction hypotheses transform ${\mathcal{D}}_1,{\mathcal{D}}_2$ into closed $\mathcal{R}$-derivations, and admissibility supplies $\mathcal{E}$. The complete final-rule transformation is $$\frac{\begin{array}{c}{\mathcal{D}}_1::\mathrm{\varnothing }{⊢}_{\mathcal{R}\cup \{r\}}{J}_1\\ {\mathcal{D}}_2::\mathrm{\varnothing }{⊢}_{\mathcal{R}\cup \{r\}}{J}_2\end{array}}{\mathrm{\varnothing }{⊢}_{\mathcal{R}\cup \{r\}}J}\mathrm{r}\stackrel{\text{induction; admissibility}}{⟹}\mathcal{E}::\mathrm{\varnothing }{⊢}_{\mathcal{R}}J.$$ Thus every judgment derivable after adjoining $r$ was already derivable before adjoining it.

For the reverse direction, assume that adjoining $r$ preserves and reflects derivability. Fix a two-premise instance $J_1,J_2/J$ whose premises have closed $\mathcal{R}$-derivations ${\mathcal{D}}_1,{\mathcal{D}}_2$. The one use of the added rule and the right-to-left implication are $$\frac{\begin{array}{c}{\mathcal{D}}_1::\mathrm{\varnothing }{⊢}_{\mathcal{R}}{J}_1\\ {\mathcal{D}}_2::\mathrm{\varnothing }{⊢}_{\mathcal{R}}{J}_2\end{array}}{\mathrm{\varnothing }{⊢}_{\mathcal{R}\cup \{r\}}J}\mathrm{r}\stackrel{\text{right-to-left implication}}{⟹}\mathcal{E}::\mathrm{\varnothing }{⊢}_{\mathcal{R}}J.$$ Since the instance was arbitrary, $r$ is admissible.

Fix an instance of Ev-Inv and suppose its premise $\mathsf{suc}(a)\mathsf{even}$ is derivable in the original parity system. The axiom Ev-Z concludes only $\mathsf{0}\mathsf{even}$, and Od-S concludes an odd judgment. The final rule can only be $$\frac{a\mathsf{odd}}{\mathsf{suc}(a)\mathsf{even}}\mathrm{Ev}-\mathrm{S}.$$ Its immediate subtree derives the desired conclusion, so every instance is admissible.

After adjoining the new axiom, there is a one-node derivation $$\frac{\phantom{X}}{\mathsf{suc}(\mathsf{0})\mathsf{even}}\mathrm{New}.$$ For the concrete instance $a=\mathsf{0}$, admissibility would require a derivation of $\mathsf{0}\mathsf{odd}$. No parity rule has that conclusion, so it remains underivable. The new premise is derivable while the required conclusion is not; admissibility is destroyed.

Put $e_0=\mathsf{add}(\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0}));\mathsf{suc}(\mathsf{0}))$. The complete one-step trees are $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{num}}}\mathrm{Num}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{num}}}\mathrm{Num}-\mathrm{S}}{\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0})){⟼}_{\mathsf{A}}\mathsf{suc}(\mathsf{0})}}\mathrm{A}-\mathrm{Add}-\mathrm{Z}}{e_0{⟼}_{\mathsf{A}}\mathsf{add}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0}))}\mathrm{A}-\mathrm{Add}-\mathrm{L},$$ $$\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{num}}}\mathrm{Num}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{num}}}\mathrm{Num}-\mathrm{S}\\ {\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{num}}}\mathrm{Num}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{num}}}\mathrm{Num}-\mathrm{S}\end{array}}{\mathsf{add}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0})){⟼}_{\mathsf{A}}\mathsf{suc}(\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0})))}\mathrm{A}-\mathrm{Add}-\mathrm{S}.$$ The final one-step tree is $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{num}}}\mathrm{Num}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{num}}}\mathrm{Num}-\mathrm{S}}{\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0})){⟼}_{\mathsf{A}}\mathsf{suc}(\mathsf{0})}}\mathrm{A}-\mathrm{Add}-\mathrm{Z}}{\mathsf{suc}(\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0}))){⟼}_{\mathsf{A}}\mathsf{suc}(\mathsf{suc}(\mathsf{0}))}\mathrm{A}-\mathrm{Suc}.$$

Let ${\mathcal{V}}_0$ and ${\mathcal{V}}_1$ denote the complete AB-Z and AB-S(AB-Z) derivations of $\mathsf{0}{\Downarrow }_{\mathsf{A}}\mathsf{0}$ and $\mathsf{suc}(\mathsf{0}){\Downarrow }_{\mathsf{A}}\mathsf{suc}(\mathsf{0})$. The big-step tree is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\mathcal{V}}_0\\ {\mathcal{V}}_1\\ {\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{nat}}}\mathrm{Nat}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{nat}}}\mathrm{Nat}-\mathrm{S}}{\mathsf{sum}(\mathsf{0};\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0}))}}\mathrm{Sum}-\mathrm{Z}\end{array}}{\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0})){\Downarrow }_{\mathsf{A}}\mathsf{suc}(\mathsf{0})}}\mathrm{AB}-\mathrm{Add}\\ {\mathcal{V}}_1\\ {\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{0}\mathsf{nat}}}\mathrm{Nat}-\mathrm{Z}}{\mathsf{suc}(\mathsf{0})\mathsf{nat}}}\mathrm{Nat}-\mathrm{S}}{\mathsf{sum}(\mathsf{0};\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0}))}}\mathrm{Sum}-\mathrm{Z}}{\mathsf{sum}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{suc}(\mathsf{0})))}}\mathrm{Sum}-\mathrm{S}\end{array}}{e_0{\Downarrow }_{\mathsf{A}}\mathsf{suc}(\mathsf{suc}(\mathsf{0}))}\mathrm{AB}-\mathrm{Add}.$$

Because $y\ne x$, the first renaming passes under the binder: $$(\lambda y.x(yz))⟨w/x⟩=\lambda y.w(yz).$$ Its free variables are $\{w,z\}$, which equals $(\{x,z\}\setminus \{x\})\cup \{w\}$. In the second term the binder is the source name, so renaming stops: $$(\lambda x.xy)⟨w/x⟩=\lambda x.xy.$$ Its free-variable set remains $\{y\}$; the source $x$ was not free in the complete abstraction, so the absent-source branch of the free-variable equation adds no $w$.

Choose $w\notin \{x,y,u,v\}$. Opening the outer abstractions gives $$\lambda y.w\text{and}\lambda v.w.$$ Choose $r\notin \{w,y,v\}$. Opening their binders gives $w$ on both sides, and the variable clause gives $w{=}_{\alpha }w$. The abstraction clause with witness $r$, followed by the abstraction clause with witness $w$, therefore derives $$\lambda x.\lambda y.x{=}_{\alpha }\lambda u.\lambda v.u.$$ The choice $w=y$ is invalid because $y\in \mathrm{Names}(e)$; opening to an existing binder name would not satisfy the common freshness premise.

The displayed binder $y$ would capture a free $y$ in the inserted term, so first rename it to a fresh $u$: Its free-variable set is $\{x,y,z\}$; the displayed $u$ is bound.

For the composition equation, the binder $z$ is already clean for the displayed data. The left side is $$(\lambda z.xy)[y/x][\mathsf{tt}/y]=(\lambda z.yy)[\mathsf{tt}/y]=\lambda z.\mathsf{tt}\mathsf{tt}.$$ The right side is $$(\lambda z.xy)[\mathsf{tt}/y][y[\mathsf{tt}/y]/x]=(\lambda z.x\mathsf{tt})[\mathsf{tt}/x]=\lambda z.\mathsf{tt}\mathsf{tt}.$$ Thus both sides agree, and the hypotheses $x\ne y$ and $x\notin \mathrm{FV}(\mathsf{tt})$ hold.

Put $$v=\lambda x.\mathsf{add}(x;\mathsf{suc}(\mathsf{0})).$$ At the first term, $E=v[-]$ and $r=\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0}))$, which contracts to $\mathsf{suc}(\mathsf{0})$. At $v\mathsf{suc}(\mathsf{0})$, the context is empty and the whole term is the beta-redex; it contracts to $\mathsf{add}(\mathsf{suc}(\mathsf{0});\mathsf{suc}(\mathsf{0}))$. This whole addition is again the redex in the empty context and contracts to $$\mathsf{suc}(\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0}))).$$ Finally $E=\mathsf{suc}([-])$ and the redex in its hole is $\mathsf{add}(\mathsf{0};\mathsf{suc}(\mathsf{0}))$, contracting to $\mathsf{suc}(\mathsf{0})$. The final term is $\mathsf{suc}(\mathsf{suc}(\mathsf{0}))$, a value.

With argument $\lambda y.y$, beta contraction first produces $\mathsf{add}(\lambda y.y;\mathsf{suc}(\mathsf{0}))$. Both arguments are values, but the first is not numeric. It cannot step, no addition contraction matches it, and the whole term is not a value. Hence it is in clause 3 of unique decomposition.

The original step is $$\frac{{\displaystyle \frac{\phantom{X}}{\mathsf{tt}\mathsf{val}}}\mathrm{V}-\mathrm{True}}{(\lambda y.xy)\mathsf{tt}⟼x\mathsf{tt}}\mathrm{E}-\mathrm{Beta}.$$ Because $y$ is fresh for $\lambda z.z$, substitution throughout the derivation gives $$\frac{{\displaystyle \frac{\phantom{X}}{\mathsf{tt}\mathsf{val}}}\mathrm{V}-\mathrm{True}}{(\lambda y.(\lambda z.z)y)\mathsf{tt}⟼(\lambda z.z)\mathsf{tt}}\mathrm{E}-\mathrm{Beta}\frac{{\displaystyle \frac{\phantom{X}}{\mathsf{tt}\mathsf{val}}}\mathrm{V}-\mathrm{True}}{(\lambda z.z)\mathsf{tt}⟼\mathsf{tt}}\mathrm{E}-\mathrm{Beta}.$$

If the original display uses binder $z$, clean it first: $$(\lambda z.xz)\mathsf{tt}{=}_{\alpha }(\lambda u.xu)\mathsf{tt}.$$ Now substitution produces $$\frac{{\displaystyle \frac{\phantom{X}}{\mathsf{tt}\mathsf{val}}}\mathrm{V}-\mathrm{True}}{(\lambda u.(\lambda z.z)u)\mathsf{tt}⟼(\lambda z.z)\mathsf{tt}}\mathrm{E}-\mathrm{Beta}.$$ The second complete tree is the preceding E-Beta/V-True tree for $(\lambda z.z)\mathsf{tt}⟼\mathsf{tt}$. The fresh representative is what prevents the inserted binder name from being confused with the binder discharged by the outer beta step.

Since $\omega$ is a value, E-Beta applies: $$\frac{{\displaystyle \frac{\phantom{X}}{\omega \mathsf{val}}}\mathrm{V}-\mathrm{Lam}}{(\lambda x.xx)\omega ⟼(xx)[\omega /x]}\mathrm{E}-\mathrm{Beta}.$$ The contractum satisfies $(xx)[\omega /x]=\omega \omega$. The same step repeats forever. Thus $\omega \omega$ diverges, but it is not stuck because it always has a next step.

In $(\lambda x.\mathsf{tt})(\mathsf{tt}\mathsf{ff})$, the function is already a value, so call by value must next reduce the argument. But $\mathsf{tt}\mathsf{ff}$ is neither a value nor a redex: both subterms are final and the function is not an abstraction. Consequently the argument has no step, the outer application has no step, and the outer term is not a value; it is stuck. Unevaluated beta substitution would instead give $\mathsf{tt}[(\mathsf{tt}\mathsf{ff})/x]=\mathsf{tt}$, but call by value forbids that contraction until the argument is a value.

Induct on the displayed value derivation. A final V-Lam, V-True, or V-False conclusion has a source shape matched by no reduction rule. A final V-Num reduces the claim to the premise $n\mathsf{num}$; rule induction on that premise excludes a step from $\mathsf{0}$, and excludes a step from $\mathsf{suc}(n)$ because E-Suc would require a step from the smaller numeral. Structural induction on the raw syntax would expose arbitrary successors as well as numeral successors and would therefore have to recover the missing numeric premise by inversion.

After deleting E-Suc, the premise $\mathsf{add}(\mathsf{0};\mathsf{0})⟼\mathsf{0}$ remains derivable by E-Add-Z, but no remaining rule has source $\mathsf{suc}(\mathsf{add}(\mathsf{0};\mathsf{0}))$; hence the proposed rule is not admissible. Restoring E-Suc makes the transformation immediate: append one E-Suc inference below any derivation of $e⟼e^{\prime }$ to obtain $\mathsf{suc}(e)⟼\mathsf{suc}(e^{\prime })$. Thus admissibility depends on the complete ambient rule set.

First prove the backward-step lemma $$e{⟼}_{\mathsf{A}}{e}^{\prime }\text{and}{e}^{\prime }{\Downarrow }_{\mathsf{A}}n⟹e{\Downarrow }_{\mathsf{A}}n$$ by induction on the one-step derivation. In A-Suc, inversion of the target evaluation selects AB-S; apply the induction hypothesis to its premise and rebuild AB-S. In A-Add-L, inversion selects AB-Add; apply the induction hypothesis to the changed left evaluation, retain the right evaluation and sum derivation, and rebuild AB-Add. The A-Add-R case applies its induction hypothesis to the changed right evaluation; its left evaluation and sum derivation are unchanged.

In A-Add-Z, the target is a numeral $n_2$. From $n_2{\Downarrow }_{\mathsf{A}}q$, lemma 1.44, lemma 1.37 gives $q\mathsf{nat}$. Rule Sum-Z gives $\mathsf{sum}(\mathsf{0};q;q)$, so AB-Add, with AB-Z and the assumed target evaluation, derives $\mathsf{add}(\mathsf{0};n_2){\Downarrow }_{\mathsf{A}}q$.

In A-Add-S, inversion of the target evaluation gives a numeral $q$ and derivations $$n_1{\Downarrow }_{\mathsf{A}}{p}_1,n_2{\Downarrow }_{\mathsf{A}}{p}_2,\mathsf{sum}(p_1;p_2;q),$$ with final result $\mathsf{suc}(q)$. Rule AB-S changes the first evaluation to $\mathsf{suc}(n_1){\Downarrow }_{\mathsf{A}}\mathsf{suc}(p_1)$, and Sum-S changes the sum premise to $\mathsf{sum}(\mathsf{suc}(p_1);p_2;\mathsf{suc}(q))$. Reapplying AB-Add derives the required source evaluation.

Finally fix $n\mathsf{num}$ and induct on $e{⟼}_{\mathsf{A}}^{\ast }n$. In M-Refl, lemma 1.45 gives $n{\Downarrow }_{\mathsf{A}}n$. In M-Step, the induction hypothesis gives $e_1{\Downarrow }_{\mathsf{A}}n$ for the many-step tail, and the backward-step lemma applied to $e{⟼}_{\mathsf{A}}{e}_1$ gives $e{\Downarrow }_{\mathsf{A}}n$.