Certification Problem

Input (TPDB TRS_Standard/SK90/2.26)

The rewrite relation of the following TRS is considered.

f(0) 0 (1)
f(s(0)) s(0) (2)
f(s(s(x))) p(h(g(x))) (3)
g(0) pair(s(0),s(0)) (4)
g(s(x)) h(g(x)) (5)
h(x) pair(+(p(x),q(x)),p(x)) (6)
p(pair(x,y)) x (7)
q(pair(x,y)) y (8)
+(x,0) x (9)
+(x,s(y)) s(+(x,y)) (10)
f(s(s(x))) +(p(g(x)),q(g(x))) (11)
g(s(x)) pair(+(p(g(x)),q(g(x))),p(g(x))) (12)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(s(s(x))) g#(x) (13)
f#(s(s(x))) h#(g(x)) (14)
f#(s(s(x))) p#(h(g(x))) (15)
g#(s(x)) g#(x) (16)
g#(s(x)) h#(g(x)) (17)
h#(x) q#(x) (18)
h#(x) p#(x) (19)
h#(x) +#(p(x),q(x)) (20)
+#(x,s(y)) +#(x,y) (21)
f#(s(s(x))) q#(g(x)) (22)
f#(s(s(x))) p#(g(x)) (23)
f#(s(s(x))) +#(p(g(x)),q(g(x))) (24)
g#(s(x)) q#(g(x)) (25)
g#(s(x)) p#(g(x)) (26)
g#(s(x)) +#(p(g(x)),q(g(x))) (27)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.