Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t003)

The rewrite relation of the following TRS is considered.

-(x,0) x (1)
-(s(x),s(y)) -(x,y) (2)
<=(0,y) true (3)
<=(s(x),0) false (4)
<=(s(x),s(y)) <=(x,y) (5)
if(true,x,y) x (6)
if(false,x,y) y (7)
perfectp(0) false (8)
perfectp(s(x)) f(x,s(0),s(x),s(x)) (9)
f(0,y,0,u) true (10)
f(0,y,s(z),u) false (11)
f(s(x),0,z,u) f(x,u,-(z,s(x)),u) (12)
f(s(x),s(y),z,u) if(<=(x,y),f(s(x),-(y,x),z,u),f(x,u,z,u)) (13)

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.
-#(s(x),s(y)) -#(x,y) (14)
<=#(s(x),s(y)) <=#(x,y) (15)
perfectp#(s(x)) f#(x,s(0),s(x),s(x)) (16)
f#(s(x),0,z,u) -#(z,s(x)) (17)
f#(s(x),0,z,u) f#(x,u,-(z,s(x)),u) (18)
f#(s(x),s(y),z,u) f#(x,u,z,u) (19)
f#(s(x),s(y),z,u) -#(y,x) (20)
f#(s(x),s(y),z,u) f#(s(x),-(y,x),z,u) (21)
f#(s(x),s(y),z,u) <=#(x,y) (22)
f#(s(x),s(y),z,u) if#(<=(x,y),f(s(x),-(y,x),z,u),f(x,u,z,u)) (23)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.