Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/perfect2)

The rewrite relation of the following TRS is considered.

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

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

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.