Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/beans)

The rewrite relation of the following TRS is considered.

f(x,f(s(s(y)),f(z,w)))	→	f(s(x),f(y,f(s(z),w)))	(1)
L(f(s(s(y)),f(z,w)))	→	L(f(s(0),f(y,f(s(z),w))))	(2)
f(x,f(s(s(y)),nil))	→	f(s(x),f(y,f(s(0),nil)))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(x,f(s(s(y)),f(z,w)))	→	f^#(s(x),f(y,f(s(z),w)))	(4)
f^#(x,f(s(s(y)),f(z,w)))	→	f^#(y,f(s(z),w))	(5)
f^#(x,f(s(s(y)),f(z,w)))	→	f^#(s(z),w)	(6)
L^#(f(s(s(y)),f(z,w)))	→	L^#(f(s(0),f(y,f(s(z),w))))	(7)
L^#(f(s(s(y)),f(z,w)))	→	f^#(s(0),f(y,f(s(z),w)))	(8)
L^#(f(s(s(y)),f(z,w)))	→	f^#(y,f(s(z),w))	(9)
L^#(f(s(s(y)),f(z,w)))	→	f^#(s(z),w)	(10)
f^#(x,f(s(s(y)),nil))	→	f^#(s(x),f(y,f(s(0),nil)))	(11)
f^#(x,f(s(s(y)),nil))	→	f^#(y,f(s(0),nil))	(12)
f^#(x,f(s(s(y)),nil))	→	f^#(s(0),nil)	(13)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair
L^#(f(s(s(y)),f(z,w))) → L^#(f(s(0),f(y,f(s(z),w)))) (7)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[f(x₁, x₂)] = 1 · x₁ + 1 · x₂

[s(x₁)] = 1 · x₁

[nil] = 0

[0] = 0

[L^#(x₁)] = 1 · x₁

together with the usable rules

f(x,f(s(s(y)),nil)) → f(s(x),f(y,f(s(0),nil))) (3)

f(x,f(s(s(y)),f(z,w))) → f(s(x),f(y,f(s(z),w))) (1)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals

[L^#(x₁)] = -1 + x₁

[f(x₁, x₂)] = -1 + x₁ + x₂

[s(x₁)] = 2 + x₁

[nil] = 0

[0] = 0

the pair
L^#(f(s(s(y)),f(z,w))) → L^#(f(s(0),f(y,f(s(z),w)))) (7)
could be deleted.
1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

f^#(x,f(s(s(y)),f(z,w)))	→	f^#(y,f(s(z),w))	(5)
f^#(x,f(s(s(y)),f(z,w)))	→	f^#(s(x),f(y,f(s(z),w)))	(4)
f^#(x,f(s(s(y)),f(z,w)))	→	f^#(s(z),w)	(6)
f^#(x,f(s(s(y)),nil))	→	f^#(s(x),f(y,f(s(0),nil)))	(11)

1.1.2 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[f(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[s(x₁)]	=	1 · x₁
[nil]	=	0
[0]	=	0
[f^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂

together with the usable rules

f(x,f(s(s(y)),nil))	→	f(s(x),f(y,f(s(0),nil)))	(3)
f(x,f(s(s(y)),f(z,w)))	→	f(s(x),f(y,f(s(z),w)))	(1)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.2.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[f(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[s(x₁)]	=	1 + 1 · x₁
[nil]	=	0
[0]	=	0
[f^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂

the pairs

f^#(x,f(s(s(y)),f(z,w)))	→	f^#(y,f(s(z),w))	(5)
f^#(x,f(s(s(y)),f(z,w)))	→	f^#(s(x),f(y,f(s(z),w)))	(4)
f^#(x,f(s(s(y)),f(z,w)))	→	f^#(s(z),w)	(6)
f^#(x,f(s(s(y)),nil))	→	f^#(s(x),f(y,f(s(0),nil)))	(11)

and no rules could be deleted.

1.1.2.1.1 P is empty

There are no pairs anymore.