ch:rewriting-reflection: ch:rewriting-reflection

If $μ$ counts additions, then $μ (a) < μ (a + 0) = μ (a) + 1$ . Hence only the orientation from $a + 0$ to $a$ satisfies the strict-decrease premise; the reverse orientation increases the measure. Admitting both produces the repeating three-term segment $a + 0, a, a + 0,$ whose last term is the first term. Repetition of that segment is infinite, so the well-founded recursive call used by the simplifier is unavailable.

Let $N (t)$ count additions and let $L (t) = \sum_{u + v ⪯ t} | u |$ , where $| u |$ is the number of syntax nodes and the sum ranges over addition subterms. Order $(N, L)$ lexicographically. Each zero rule lowers $N$ . The rule $(a + b) + c \mapsto a + (b + c)$ preserves $N$ and lowers $L$ by $| a | + 1$ ; all unchanged subterms contribute equally. Thus the extended database terminates. Bottom-up simplification gives $\begin{aligned} (a + 0) + (b + (0 + c)) & \overset{c o n g - +; a + 0 = a}{=} a + (b + (0 + c)) \\ \overset{c o n g - +; 0 + c = c}{=} a + (b + c) . \end{aligned}$ The result is right associated, so no associativity root remains.

Given $p : n = m$ , dependent congruence for transport first changes the vector fiber. For $v : Vec A n$ , the certificate is $\begin{aligned} {transport}_{Vec A} & : (p : n = m) \to Vec A n \to Vec A m, \\ (p, v) & ⟼ transport p v . \end{aligned}$ Rebuilding an outer dependent application therefore uses $transport p v : Vec A m$ . Omitting the transport offers the unchanged term $v : Vec A n$ where the rebuilt head requires an argument of type $Vec A m$ . That application is ill typed unless conversion already derives $n \equiv m$ , which a propositional proof $p$ alone does not provide.