# Rewriting Techniques, 2: termination, interpretation

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}))\ \}$$.

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

2. 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}$

3. 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\}$$.

1. 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$$.

2. 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$$.

3. 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}

1. Prove that RPO cannot prove the termination of the system.

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

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

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

2. $$\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)$$.

2. 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}

1. Prove its termination via well-founded induction.

2. 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.

3. 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$$.

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)$$.

2. 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))$

3. 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

1. $$w(s) > w(t)$$, or

2. $$w(s) = w(t)$$ and one of the following alternatives holds

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

2. $$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

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

Using a KBO, prove the termination of:

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

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

1. 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.

2. 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}$$.