Certification Problem

Input (TPDB TRS_Standard/AProVE_04/fac)

The rewrite relation of the following TRS is considered.

plus(x,0) x (1)
plus(x,s(y)) s(plus(x,y)) (2)
times(0,y) 0 (3)
times(x,0) 0 (4)
times(s(x),y) plus(times(x,y),y) (5)
p(s(s(x))) s(p(s(x))) (6)
p(s(0)) 0 (7)
fac(s(x)) times(fac(p(s(x))),s(x)) (8)

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.
plus#(x,s(y)) plus#(x,y) (9)
times#(s(x),y) plus#(times(x,y),y) (10)
times#(s(x),y) times#(x,y) (11)
p#(s(s(x))) p#(s(x)) (12)
fac#(s(x)) times#(fac(p(s(x))),s(x)) (13)
fac#(s(x)) fac#(p(s(x))) (14)
fac#(s(x)) p#(s(x)) (15)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.