ch:supercompilation: ch:supercompilation

Unfolding append exposes a case on $x$. Rule D-Case-Open first creates two refinement edges, to the same case with scrutinee $\mathsf{Nil}$ and with scrutinee $\mathsf{Cons}(a,z)$, respectively. The edge substitutions are $[\mathsf{Nil}/x]$ and $[\mathsf{Cons}(a,z)/x]$. At the second node on each path, D-Case-Known contracts the case and gives the residual leaves $$C_{\mathsf{nil}}=\mathsf{Cons}(b,\mathsf{Nil}),C_{\mathsf{cons}}=\mathsf{Cons}(a,\mathsf{append}(z,\mathsf{Cons}(b,\mathsf{Nil}))).$$ The second leaf contains the one residual recursive call; its first argument is the constructor tail $z$.

At the roots, Emb-Couple reduces the forward judgment to its two children. Rule Emb-Var gives $x\preccurlyeq a$. For the tail, Emb-Dive selects the tail of the outer right-hand $\mathsf{Cons}$, after which Emb-Couple gives $\mathsf{Nil}\preccurlyeq \mathsf{Nil}$. Hence the required embedding holds. Reversing it would couple the outer $\mathsf{Cons}$ heads and then require $\mathsf{Cons}(x,\mathsf{Nil})\preccurlyeq \mathsf{Nil}$. The heads do not match for Emb-Couple, and $\mathsf{Nil}$ has no child for Emb-Dive; the derivation stops there.

The first five call configurations are $$Q_i=\mathsf{loop}({\mathsf{S}}^i(x))(0\le i\le 4).$$ The first whistle is $Q_0\preccurlyeq Q_1$: couple the common $\mathsf{loop}$ head and use Emb-Dive with Emb-Var for $x\preccurlyeq \mathsf{S}(x)$. Their most-specific generalization is $$g=\mathsf{loop}(z),\sigma =[x/z],\tau =[\mathsf{S}(x)/z].$$ Direct substitution gives $g\sigma =Q_0$ and $g\tau =Q_1$. Root agreement forces any common generalization to retain the loop head, while the child disagreement forces a variable, so the factorization clause of lemma 128.5 proves most-specificity.

Let the faulty test erase constructor names before comparing states. It then identifies the same-arity closed states $\mathsf{S}(\mathsf{Z})$ and $\mathsf{P}(\mathsf{Z})$, where $\mathsf{S}$ and $\mathsf{P}$ are distinct unary constructors, and folds the former to the latter’s residual node. The unfolded state returns $\mathsf{S}(\mathsf{Z})$, whereas the folded state returns $\mathsf{P}(\mathsf{Z})$, so returned constructors differ. Variant equivalence repairs the test by demanding identical constructor heads and only a bijective renaming of free variables. For an accepted pair $Q^{\prime }=Q\pi$, the residual equation for $Q$ abstracts exactly $\mathrm{fv}(Q)$; applying it to $\pi$ alpha-renames that equation to $Q^{\prime }$. Thus the repaired back edge satisfies the folding equation and preserves evaluation.