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 AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
perfectp#(s(x)) f#(x,s(0),s(x),s(x)) (7)
f#(s(x),0,z,u) f#(x,u,minus(z,s(x)),u) (8)
f#(s(x),s(y),z,u) f#(s(x),minus(y,x),z,u) (9)
f#(s(x),s(y),z,u) f#(x,u,z,u) (10)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.