Certification Problem

Input (TPDB TRS_Standard/AG01/#3.22)

The rewrite relation of the following TRS is considered.

times(x,plus(y,s(z))) plus(times(x,plus(y,times(s(z),0))),times(x,s(z))) (1)
times(x,0) 0 (2)
times(x,s(y)) plus(times(x,y),x) (3)
plus(x,0) x (4)
plus(x,s(y)) s(plus(x,y)) (5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
times#(x,plus(y,s(z))) plus#(times(x,plus(y,times(s(z),0))),times(x,s(z))) (6)
times#(x,plus(y,s(z))) times#(x,plus(y,times(s(z),0))) (7)
times#(x,plus(y,s(z))) plus#(y,times(s(z),0)) (8)
times#(x,plus(y,s(z))) times#(s(z),0) (9)
times#(x,plus(y,s(z))) times#(x,s(z)) (10)
times#(x,s(y)) plus#(times(x,y),x) (11)
times#(x,s(y)) times#(x,y) (12)
plus#(x,s(y)) plus#(x,y) (13)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.