Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/perfect)

The rewrite relation of the following TRS is considered.

perfectp(0) false (1)
perfectp(s(x)) f(x,s(0),s(x),s(x)) (2)
f(0,y,0,u) true (3)
f(0,y,s(z),u) false (4)
f(s(x),0,z,u) f(x,u,minus(z,s(x)),u) (5)
f(s(x),s(y),z,u) if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) (6)

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),s(y),z,u) f#(s(x),minus(y,x),z,u) (7)
f#(s(x),s(y),z,u) f#(x,u,z,u) (8)
perfectp#(s(x)) f#(x,s(0),s(x),s(x)) (9)
f#(s(x),0,z,u) f#(x,u,minus(z,s(x)),u) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.