2019–11–21

A **matrix interpretation on integers** is the following:

a positive integer \(d\);

for every symbol \(f\) of arity \(n\), \(n\) matrices \(M_{f,1}\dots,M_{f,n} \in \mathbb{N}^{d \times d}\);

for every symbol of arity \(n\), a vector \(V_f \in \mathbb{N}^d\);

a non-empty set \(I \subseteq \{1,\dots,d\}\) satisfying that for every symbol \(f\) of arity \(n\) the map \[L_f: (\mathbb{N}^d)^n \to \mathbb{N}^d\text{ defined as } L_f(X_1,\dots,X_n) = V_f + \sum_{i=1}^n M_{f,i}X_i\] is monotonic with respect to \(>_I\) were \(X >_I Y\) holds if and only if for every \(i \in \{1,\dots,d\}\), \(X[i] \geq Y[i]\) and there is \(j \in I\) such that \(X[j] > Y[j]\).

Then \((\mathbb{N}^d, (L_f)_f, >_I)\) is a well-founded monotone algebra.

Consider the TRS \(\{\ \mathtt{s}(\mathtt{a}) \to \mathtt{s}(\mathtt{p}(\mathtt{a})),\ \mathtt{p}(\mathtt{b}) \to \mathtt{p}(\mathtt{s}(\mathtt{b}))\ \}\).

Prove that its termination cannot be proved by a polynomial interpretation on integers;

Use the following matrix interpretation to prove termination w.r.t. \(>_{\{1,2\}}\). \[L_{\mathtt{s}}(X) = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix}X \qquad L_{\mathtt{p}}(X) = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix}X \qquad L_{\mathtt{a}} = \begin{bmatrix} 0 \\ 1 \end{bmatrix} \qquad L_{\mathtt{b}} = \begin{bmatrix} 1 \\ 0 \end{bmatrix}\]

Why does it fail if we take \(>_{\{1\}}\) instead? Is there another matrix interpretation that works with this ordering?

(1) From the first rule, the degree of \(\mathtt{P}_\mathtt{p}\) must be one. The same holds for \(\mathtt{P}_\mathtt{s}\), thanks to the second rule. This implies that \(\mathtt{P}_{\mathtt{s}(\mathtt{a})}\) of the form \(s_1a + s_0\) whereas \(\mathtt{P}_{\mathtt{s}(\mathtt{p}(\mathtt{a}))}\) of the form \(s_1p_1a + s_1p_0 + s_0\) which, since \(p_1 \geq 1\), is sufficient to conclude that the termination of this TRS cannot be proved by a polynomial interpretation on integers.

(2) It holds that: \[L_{\mathtt{s}}(L_{\mathtt{a}}) = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = \begin{bmatrix} 1 \\ 1 \end{bmatrix} >_{\{1,2\}} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = L_{\mathtt{s}}(L_{\mathtt{p}}(L_{\mathtt{a}}))\] \[L_{\mathtt{p}}(L_{\mathtt{b}}) = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = \begin{bmatrix} 1 \\ 1 \end{bmatrix} >_{\{1,2\}} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 0 \\ 1 \end{bmatrix} = \begin{bmatrix} 1 & 1\\ 1 & 0 \end{bmatrix} \begin{bmatrix} 0 & 1\\ 1 & 1 \end{bmatrix} \begin{bmatrix} 1 \\ 0 \end{bmatrix} = L_{\mathtt{p}}(L_{\mathtt{s}}(L_{\mathtt{b}}))\]

(3) From the second rule, \(\begin{bmatrix} 1 \\ 1 \end{bmatrix} >_{\{1\}} \begin{bmatrix} 1 \\ 0 \end{bmatrix}\) does not hold. No, let \(L_{\mathtt{s}}(X) = M_{\mathtt{s}} X + V_{\mathtt{s}}\) and \(L_{\mathtt{p}}(X) = M_{\mathtt{p}} X + V_{\mathtt{p}}\). For the first rule it will hold \[\begin{aligned} L_{\mathtt{s}}(L_{\mathtt{a}}) &= M_{\mathtt{s}}L_{\mathtt{a}} + V_{\mathtt{s}}\\ L_{\mathtt{s}}(L_{\mathtt{p}}(L_{\mathtt{a}})) &= M_{\mathtt{s}}M_{\mathtt{p}}L_{\mathtt{a}} + M_{\mathtt{s}}V_{\mathtt{p}} + V_{\mathtt{s}}\end{aligned}\] To make \(>_{\{1\}}\) it must therefore hold \[(M_{\mathtt{s}})_{1,1}(L_{\mathtt{a}})_{1,1} + \dots + (M_{\mathtt{s}})_{1,d}(L_{\mathtt{a}})_{1,d} > (M_{\mathtt{p}})_{1,1}((M_{\mathtt{s}})_{1,1}(L_{\mathtt{a}})_{1,1} + \dots + (M_{\mathtt{s}})_{1,d}(L_{\mathtt{a}})_{1,d}) + \dots\] which implies \((M_{\mathtt{p}})_{1,1} = 0\). Similarly, from the second rule, \((M_{\mathtt{s}})_{1,1} = 0\). This implies that no polynomial interpretation with the ordering \(>_{\{1\}}\) can be defined for this TRS, since for any \(m > n\), \((m,0,\dots,0) >_{\{1\}} (n,0,\dots,0)\) but \(L_{\mathtt{s}}(m,0,\dots,0) =_{\{1\}} L_{\mathtt{s}}(n,0,\dots,0)\).

Let \(A \subseteq \mathbb{N}\) and \(\mathtt{P}_{f}\) be respectively the domain and the interpretation, for each function symbol \(f\), of a polynomial interpretation of integers for a TRS *(note: the TRS is therefore terminating)*. Take \(a \in A \setminus \{0\}\).

Define \(\pi_a : T(F,X) \to A\) as the function which maps every variable \(x\) to \(a\) and every term of the form \(f(t_1,\dots,t_n)\) to \(\mathtt{P}_f(\pi_a(t_1),\dots,\pi_a(t_n))\). Prove that \(\pi_a(t)\) is greater or equal to the length of every reduction starting from \(t\).

Show that there exists \(d\) and \(k\) positive integers such that for every \(f \in F\) of arity \(n\) and every \(a_1,\dots,a_n \in A \setminus \{0\}\) it holds \(\mathtt{P}_f(a_1,\dots,a_n) \leq d \prod_{i=1}^n a_i^k\).

From the previous point, pick \(d\) to be also greater or equal than \(a\) and fix \(c \geq k + \log_2(d)\). Prove that \(\pi_a(t) \leq 2^{2^{c|t|}}\).

Consider now any finite TRS and a function symbol \(f\). Prove that there exists an integer \(k\) such that if \(s \to t\) then \(|t|_f \leq k(|s|_f + 1)\), where \(|.|_f\) is the number of \(f\).

Deduce that the TRS \[\{\ \mathtt{a}(\mathtt{0},y) \to \mathtt{s}(y),\ \mathtt{a}(\mathtt{s}(x),\mathtt{0}) \to \mathtt{a}(x,\mathtt{s}(\mathtt{0})),\ \mathtt{a}(\mathtt{s}(x),\mathtt{s}(y)) \to \mathtt{a}(x,\mathtt{a}(\mathtt{s}(x),y))\ \},\] simulating the Ackermann’s function, cannot be proved terminating using a polynomial interpretation over integers.

The proof is by induction on the \(\to\) relation. Let \(t\) be irreducible. Then the length of all its reductions is \(0\) and \(\pi_a(t) \geq 0\) by definition. For the inductive step, suppose \(t \to t^\prime\) s.t. \(t \to t^\prime \to \dots\) is the maximal reduction from \(t\). There exists a context \(C\), a valuation \(\sigma\) and a rewriting rule \(l \to r\) such that \(t = C[l\sigma] \to C[r\sigma] = t^\prime\). W.l.o.g. we can consider just terms of the form \(l\sigma \to r\sigma\). Let \(\mathtt{P}_l\) and \(\mathtt{P}_r\) be the polynomials resulting from the polynomial interpretation, for \(l\) and \(r\) respectively. We have that, for all \(X_1,\dots,X_n\), \(\mathtt{P}_l(X_1,\dots,X_n) > \mathtt{P}_r(X_1,\dots,X_n)\). By inductive hypothesis, \(\pi_a(r\sigma) = \mathtt{P}_r(\pi_a(\sigma(X_1)),\dots,\pi_a(\sigma(X_n)))\) is greater or equal to the length of every reduction starting from \(r\sigma\). It follow that \(\pi_a(l\sigma) = \mathtt{P}_l(\pi_a(\sigma(X_1)),\dots,\pi_a(\sigma(X_n))) \geq \pi_a(r\sigma) + 1\) and therefore \(\pi_a(l\sigma)\) is greater or equal to the length of every reduction starting from \(l\sigma\).

Let \(\{s_0,\dots, s_m\}\) be the coefficient of the polynomial \(\mathtt{P}_f\), let \(d \geq \sum_{i=0}^n s_i\) (so \(d \geq 1\)) and let \(k\geq 1\) be also greater or equal to the degree of \(\mathtt{P}_f\). The thesis can be rewritten as \(\mathtt{P}_f(a_1,\dots,a_n) \leq (\sum_{i=1}^m s_i) \prod_{j=1}^n a_j^k = \sum_{i=1}^m(s_i \prod_{j=1}^n a_j^k)\). Moreover there exists \[k_{1,1}\dots,k_{1,n},k_{2,1},\dots,k_{2,n},\dots,k_{m,1},\dots,k_{m,n}\] such that \(\mathtt{P}_f(a_1,\dots,a_n) = \sum_{i=1}^{m}(s_i \prod_{j=1}^n a_j^{k_{i,j}})\) and for all \(i \in [1,m]\) \(k_{i,1} + \dots + k_{i,n} \leq k\). Moreover \(a_1,\dots,a_n \in A \setminus \{0\}\), and therefore the thesis trivially holds since for all \(i \in [1,m]\) \(s_i \prod_{j=1}^n a_j^{k_{i,j}} \leq s_i \prod_{j=1}^n a_j^{k}\).

By induction of \(t\). If \(t\) is a variable, then \(|t| = 1\) and \(\pi_a(t) = a \leq 2^a \leq 2^{2^{\log_2(d)}} \leq 2^{2^{c|t|}}\). If \(t\) is of the form \(f(t_1,\dots,t_n)\) then \(\pi_a(t) = \mathtt{P}_f(\pi_a(t_1),\dots,\pi_a(t_n))\). By inductive hypothesis, since \(\mathtt{P}_f\) is monotone, \(\pi_a(t) \leq \mathtt{P}_f(2^{2^{c|t_1|}},\dots,2^{2^{c|t_n|}})\). From (2) it follows that \(\mathtt{P}_f(2^{2^{c|t_1|}},\dots,2^{2^{c|t_n|}}) \leq d \prod_{i=1}^n (2^{2^{c|t_i|}})^k = d 2^{{\Sigma}_{i} (k2^{c|t_i|})} = 2^{\log_2(d)} 2^{{\Sigma}_{i} (k2^{c|t_i|})} = 2^{\log_2(d)+ k{\Sigma}_{i} (2^{c|t_i|})} \leq 2^{(\log_2(d)+ k){\Sigma}_{i} (2^{c|t_i|})}\). Since \(d \geq a \geq 1\) and \(k \geq 1\) it holds that \(c \geq 1\) and therefore \(2^{(\log_2(d)+ k){\Sigma}_{i} (2^{c|t_i|})} \leq 2^{c{\Pi}_{i} (2^{c|t_i|})} \leq 2^{2^{c}{\Pi}_{i} (2^{c|t_i|})} \leq 2^{2^{c|t|}}\).

W.l.o.g. consider \(s = l\sigma\) and \(t = r\sigma\) for a rewriting rule \(l \to r\) and a valuation \(\sigma\). The number of occurrences of \(f\) in \(l\sigma\) is \(|l|_f + \sum_{p \in \{p | l|_p \in X\}} |\sigma(l|_p)|_f\) where \(|l|_f\) only depends on the left side of the rewriting rule. Similarly, \(|r\sigma|_f = |r|_f + \sum_{p \in \{p | r|_p \in X\}} |\sigma(r|_p)|_f\) where \(|r|_f\) depends only on the right side of the rewriting rule. Let \(V\) the number of variables in \(r\) (i.e. \(|\{p | r|_p \in X\}|\)). It holds that \(|r\sigma|_f \leq |r|_f + V\max_{p \in \{p | r|_p \in X\}}( |\sigma(r|_p)|_f )\). Since every variable of \(r\) also occurs in \(l\) it must hold that \(|r\sigma|_f \leq |r|_f + V\max_{p \in \{p | l|_p \in X\}}( |\sigma(l|_p)|_f )\). Moreover \(\max_{p \in \{p | l|_p \in X\}}( |\sigma(l|_p)|_f )\) is trivially less or equal that all the occurrences of \(f\) in \(l\sigma\), therefore \(|r\sigma|_f \leq |r|_f + V|l\sigma|_f \leq (|r|_f + V)(|l\sigma|_f + 1)\). \(|r|_f\) and \(V\) only depends on the rule itself. Let \(k\) be greater or equal than the maximum number of occurrences of \(f\) in the right side of each rule of the TRS plus the number of variables in the right side of each rule of the TRS. it holds that \(|r\sigma|_f \leq k(|l\sigma|_f + 1)\).

From the above point, it holds that for all terms \(s\) and \(t\) such that \(s \to t\), \(|t|_\mathtt{s}\leq k(|s|_\mathtt{s}+ 1)\). So at each step of the rewriting system, the number of \(\mathtt{s}\) can at most increase \(k\) times (from the previous proof, for Ackermann this should hold for \(k \geq 5\)). If Ackermann could be proved terminating using a polynomial interpretation over integers then given any term \(t\), the maximum number of steps will be \(\pi_a(t) \leq 2^{2^{c|t|}}\), where \(c\) is fixed (and depends on the polynomial interpretation, see proof (2)). The size of a term of the form \(\mathtt{a}(m,n)\) is \(m+n+3\). We conclude that there must exists \(k\) and \(c\) such that for any \(X,Y\) it should hold \(Ack(X,Y) \leq k * 2^{2^{c(X+Y+3)}}\). This cannot hold since \(Ack(X,Y)\) is not primitive recursive whereas \(k * 2^{2^{c(X+Y+3)}}\) is, and therefore there exists \(X\) and \(Y\) such that \(Ack(X,Y) > k * 2^{2^{c(X+Y+3)}}\).

For next week: well-founded induction, multisets, RPO

Consider exercise on semantic labeling of TD1, where the following rewriting system was defined \[\begin{aligned} \mathsf{f}\ (\mathsf{s}\ X) &\to \mathsf{f}\ (\mathsf{p}\ (\mathsf{s}\ X)) \diamond (\mathsf{s}\ X) & \mathsf{p}\ (\mathsf{s}\ \mathsf{z}) &\to \mathsf{z} \\ \mathsf{p}\ (\mathsf{s}\ (\mathsf{s}\ X)) &\to \mathsf{s}\ (\mathsf{p}\ (\mathsf{s}\ X))\end{aligned}\]

Prove that RPO cannot prove the termination of the system.

Prove that a labeled system can be proved terminating with RPO.

Considering the first rewrite rule, \(\mathsf{f} > \diamond\) is needed. Then we must check that

\(\mathsf{f}\ (\mathsf{s}\ X) >_{\text{rpo}} \mathsf{f}\ (\mathsf{p}\ (\mathsf{s}\ X))\) and

\(\mathsf{f}\ (\mathsf{s}\ X) >_{\text{rpo}} (\mathsf{s}\ X)\).

Second condition is immediate since \(\mathsf{s}\ X \lhd \mathsf{f}\ (\mathsf{s}\ X)\).

First condition needs \(\mathsf{s}\ X >_{rpo} \mathsf{p}\ (\mathsf{s}\ X)\) which is impossible since \(\mathsf{s}\ X <_{rpo} \mathsf{p}\ (\mathsf{s}\ X)\) since \(\mathsf{s}\ X \lhd \mathsf{p}\ (\mathsf{s}\ X)\).

With the following interpretation on \(\mathbb{N}\): \(\mathsf{z} = 0, \mathsf{s}\ X = X + 1\), \(\mathsf{p}\ X = \max(0, X - 1)\), \(\mathsf{lab}(R)\) is the following (infinite) system, for all \(i \in \mathbb{N}\) \[\begin{aligned} \mathsf{f}_{i + 1}\ (\mathsf{s}_i\ X) &\to \mathsf{f}_i\ (\mathsf{p}_{i + 1}\ (\mathsf{s}_i\ X)) \diamond (\mathsf{s}\ X) & \mathsf{p}\ (\mathsf{s}\ \mathsf{z}) &\to \mathsf{z} \\ \mathsf{p}_{i + 2}\ (\mathsf{s}\ (\mathsf{s}\ X)) &\to \mathsf{s}_i\ (\mathsf{p}_{i + 1}\ (\mathsf{s}_i\ X)) \end{aligned}\] If we take \(\mathsf{f}_i > \diamond\), \(\mathsf{f}_{i} > \mathsf{f}_{i+1}\), \(\mathsf{f}_i > \mathsf{p}_{i + 1}\), the first rule is ensured decreasing. The second rule is trivially decreasing. Taking \(\mathsf{p}_{i+2} > \mathsf{s}_i\) and \(\mathsf{p}_{i + 2} > \mathsf{p}_{i + 1}\) makes the last rule decreasing.

We consider the Ackermann’s function \[\begin{aligned} \mathtt{Ack}\ \mathtt{0}\ y &= y + 1\\ \mathtt{Ack}\ x\ 0 &= \mathtt{Ack}\ (x-1)\ 1\\ \mathtt{Ack}\ x\ y &= \mathtt{Ack}\ (x-1)\ (\mathtt{Ack}\ x\ (y-1))\end{aligned}\]

Prove its termination via well-founded induction.

The following rewrite system simulates \(\mathtt{Ack}\) \[\begin{aligned} \mathtt{a}(\mathtt{0},y) &\to \mathtt{s}(y)\\ \mathtt{a}(\mathtt{s}(x),\mathtt{0}) &\to \mathtt{a}(x,\mathtt{s}(\mathtt{0}))\\ \mathtt{a}(\mathtt{s}(x),\mathtt{s}(y)) &\to \mathtt{a}(x,\mathtt{a}(\mathtt{s}(x),y)) \end{aligned}\] Prove its termination using a LPO.

Consider the well-founded domain \((\mathtt{Mult}(\mathbb{N}\times\mathbb{N}), (>_\text{lex})_\text{mul})\). Prove the termination of \(\mathtt{Ack}\) using the following abstraction: \[\begin{aligned} \phi:\ T(\{\mathtt{a},\mathtt{s}\},X) &\to \mathtt{Mult}(\mathbb{N}\times \mathbb{N})\\ t &\to \{\!|\ (|u|,|v|) \mid t|_{p\in \text{Pos}(t)} = \mathtt{a}(u,v)\ |\!\} \end{aligned}\] where \(|\mathtt{0}| = 1\), \(|\mathtt{a}(x,y)| = |x|+|y|+1\) and \(|\mathtt{s}(x)| = |x| + 1\).

Induction on \({(\mathbb{N}\times\mathbb{N}, >_\text{lex})}\). We prove that the calculus of \(\mathtt{Ack}\ u\ v\) terminates by induction \((u,v)\) ordered lexicographically on integers.

Base cases: \(\mathtt{Ack}\) terminates for \((0,n)\), \(n \in \mathbb{N}\);

We need to show that \(\mathtt{Ack}\) terminates for \((n,m)\), \(n > 0\). Induction hypothesis: \(\mathtt{Ack}\) terminates for all \((j,k)\) such that \(j < n\) or (\(j = n\) and \(k < m\)). If \(m = 0\) then by induction hypothesis the function terminates since \((n-1,1) < (n,m)\). Instead, if \(m > 0\), by induction hypothesis the function terminates on input \((n, m - 1)\) with output \(r\) and terminates on input \((n-1,r)\).

Let \(>\) be such that \(\mathtt{a}> \mathtt{s}\) and let \(\mathtt{status}(\mathtt{a}) = \mathtt{status}(\mathtt{s}) = \text{lex}\). It holds:

\(\mathtt{a}(0,t) >_\text{rpo}\mathtt{s}(t)\), since \(\mathtt{a}> \mathtt{s}\) and \(\mathtt{a}(0,t) >_\text{rpo}t\);

\(\mathtt{a}(\mathtt{s}(t),0) >_\text{rpo}\mathtt{a}(t,\mathtt{s}(0))\) since \(\mathtt{a}(\mathtt{s}(t),0) > t\), \(\mathtt{a}(\mathtt{s}(t),0) > \mathtt{s}(0)\) and \((\mathtt{s}(t),0) (>_\text{rpo})_\text{lex} (t,\mathtt{s}(0))\);

\(\mathtt{a}(\mathtt{s}(t),\mathtt{s}(t^\prime)) >_{\text{rpo}} \mathtt{a}(t,\mathtt{a}(\mathtt{s}(t),t^\prime))\) since \[\mathtt{a}(\mathtt{s}(t),\mathtt{s}(t^\prime)) >_{\text{rpo}} t,\ \mathtt{a}(\mathtt{s}(t),\mathtt{s}(t^\prime)) >_{\text{rpo}} \mathtt{a}(\mathtt{s}(t),t^\prime),\ (\mathtt{s}(t),\mathtt{s}(t^\prime)) (>_\text{rpo})_\text{lex}(t,\mathtt{a}(\mathtt{s}(t),t^\prime))\]

We can show that whenever \(s \to t\), then \(\phi(s) < \phi(t)\).

A weight function for a signature \(\Sigma\) is a pair \((w, w_0)\) consisting of a mapping \(w : \Sigma \to \mathbb{N}\) and a constant \(w_0 > 0\) such that \(w(c) \geq w_0\) for all *constant* \(c \in \Sigma\). Let \((w, w_0)\) be a weight function. The weight of a term \(t\) is defined as follows \[w(t) =
\begin{cases}
w_{0} & \text{if } t \text{ is a variable} \\
w(f) + \sum_{i=1}^n w(t_i) & \text{if } t = f(t_1, \dots, t_n)
\end{cases}\] We denote \(|s|_x\) for \(x\) a variable the number of times that \(x\) occurs in \(s\). Let \(>\) be a precedence and \((w, w_{0})\) a weight function. We define the *Knuth-Bendix order* (KBO) \(>_{\text{kbo}}\) on terms inductively as follows: \(s >_{\text{kbo}} t\) if \(|s|_{x} \geq |t|_{x}\) for all variables \(x\) and either

\(w(s) > w(t)\), or

\(w(s) = w(t)\) and one of the following alternatives holds

\(t\) is a variable and \(s = f^{n}(t)\) for some unary function symbol \(f\) and \(n > 0\),

\(s = f(s_1, \dots, s_n), t = f(t_1, \dots, t_n)\) and there is \(i \in \{ 1, \dots, n \}\) such that \(s_j = t_j\) for all \(1 \leq j < i\) and \(s_i >_{\text{kbo}} t_i\), or

\(s = f(s_1, \dots, s_n), t = g(t_1, \dots, t_m)\) and \(f > g\).

Using a KBO, prove the termination of:

\(\{ \mathtt{l}(x) + (y + z) \to x + (\mathtt{l}(\mathtt{l}(y)) + z),\ \mathtt{l}(x) + (y + (z + w)) \to x + (z + (y + w))\ \}\)

\(\{\ \mathtt{r}^n(\mathtt{l}^k(x)) \to \mathtt{l}^k(\mathtt{r}^m(x))\ \}\), where \(n,k > 0\) and \(m \geq 0\).

Let \(\mathtt{l}> +\), \(w(\mathtt{l}) = 0\), \(w(+) = w(x) > 0\) for each variable \(x\). It holds that \(w\) is admissible. For both rules, it holds that the weight does not change after the rewrite step. To prove that \(\mathtt{l}(x) + (y + z) >_\text{kbo}x + (\mathtt{l}(\mathtt{l}(y)) + z)\) we therefore need to prove the third condition, which holds since \(\mathtt{l}(x) >_\text{kbo}x\). Similarly, to prove \(\mathtt{l}(x) + (y + (z + w)) >_\text{kbo}x + (z + (y + w))\), it is sufficient to show that \(\mathtt{l}(x) >_\text{kbo}x\). Notice that it does not holds \((y + (z + w) >_\text{kbo}z + (y + w)\) because of the ordering of the variables.

Let \(\mathtt{r}> \mathtt{l}\), \(w(\mathtt{r}) = 0\) and \(w(\mathtt{l}) = 1\). It holds that \(w\) is admissible. Let \(s \to t\) with \(s = C[\mathtt{r}^n(\mathtt{l}^k(t^\prime))]\) and \(t= C[\mathtt{l}^k(\mathtt{r}^m(t^\prime))]\). From the definition of \(w\), it holds that \(w(s) = w(t)\) since the number of occurrences of the function symbol \(\mathtt{l}\) is the same in \(s\) and \(t\). By applying the definition of \(>_\text{kbo}\), we get that we need to show \(\mathtt{r}^n(\mathtt{l}^k(t^\prime)) >_\text{kbo} \mathtt{l}^k(\mathtt{r}^m(t^\prime))\), which holds since \(\mathtt{r}> \mathtt{l}\).