Certification Problem

Input (TPDB TRS_Standard/GTSSK07/cade13t)

The rewrite relation of the following TRS is considered.

div(x,s(y)) d(x,s(y),0) (1)
d(x,s(y),z) cond(ge(x,z),x,y,z) (2)
cond(true,x,y,z) s(d(x,s(y),plus(s(y),z))) (3)
cond(false,x,y,z) 0 (4)
ge(u,0) true (5)
ge(0,s(v)) false (6)
ge(s(u),s(v)) ge(u,v) (7)
plus(n,0) n (8)
plus(n,s(m)) s(plus(n,m)) (9)

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.
div#(x,s(y)) d#(x,s(y),0) (10)
d#(x,s(y),z) cond#(ge(x,z),x,y,z) (11)
d#(x,s(y),z) ge#(x,z) (12)
cond#(true,x,y,z) d#(x,s(y),plus(s(y),z)) (13)
cond#(true,x,y,z) plus#(s(y),z) (14)
ge#(s(u),s(v)) ge#(u,v) (15)
plus#(n,s(m)) plus#(n,m) (16)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.