Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/jones6)

The rewrite relation of the following TRS is considered.

f(a,empty)	→	g(a,empty)	(1)
f(a,cons(x,k))	→	f(cons(x,a),k)	(2)
g(empty,d)	→	d	(3)
g(cons(x,k),d)	→	g(k,cons(x,d))	(4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(a,empty)	→	g^#(a,empty)	(5)
g^#(cons(x,k),d)	→	g^#(k,cons(x,d))	(6)
f^#(a,cons(x,k))	→	f^#(cons(x,a),k)	(7)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair
f^#(a,cons(x,k)) → f^#(cons(x,a),k) (7)

1.1.1 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation

[f(x₁, x₂)] = 0

[f^#(x₁, x₂)] = x₂ + 0

[g^#(x₁, x₂)] = 0

[cons(x₁, x₂)] = x₂ + 1

[empty] = 0

[g(x₁, x₂)] = 0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair
f^#(a,cons(x,k)) → f^#(cons(x,a),k) (7)
could be deleted.
1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.
The 2^nd component contains the pair
g^#(cons(x,k),d) → g^#(k,cons(x,d)) (6)

1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation

[f(x₁, x₂)] = 0

[f^#(x₁, x₂)] = 0

[g^#(x₁, x₂)] = x₁ + 0

[cons(x₁, x₂)] = x₂ + 1

[empty] = 0

[g(x₁, x₂)] = 0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair
g^#(cons(x,k),d) → g^#(k,cons(x,d)) (6)
could be deleted.
1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.