Certification Problem

Input (TPDB TRS_Standard/SK90/4.57)

The rewrite relation of the following TRS is considered.

f(x,y,z) g(<=(x,y),x,y,z) (1)
g(true,x,y,z) z (2)
g(false,x,y,z) f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y)) (3)
p(0) 0 (4)
p(s(x)) x (5)

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.
g#(false,x,y,z) f#(p(x),y,z) (6)
g#(false,x,y,z) f#(p(z),x,y) (7)
g#(false,x,y,z) p#(z) (8)
g#(false,x,y,z) p#(y) (9)
g#(false,x,y,z) p#(x) (10)
g#(false,x,y,z) f#(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y)) (11)
f#(x,y,z) g#(<=(x,y),x,y,z) (12)
g#(false,x,y,z) f#(p(y),z,x) (13)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.