Certification Problem

Input (TPDB TRS_Standard/AProVE_06/factorial1)

The rewrite relation of the following TRS is considered.

plus(0,x) x (1)
plus(s(x),y) s(plus(p(s(x)),y)) (2)
times(0,y) 0 (3)
times(s(x),y) plus(y,times(p(s(x)),y)) (4)
p(s(0)) 0 (5)
p(s(s(x))) s(p(s(x))) (6)
fac(0,x) x (7)
fac(s(x),y) fac(p(s(x)),times(s(x),y)) (8)
factorial(x) fac(x,s(0)) (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.
plus#(s(x),y) plus#(p(s(x)),y) (10)
plus#(s(x),y) p#(s(x)) (11)
times#(s(x),y) plus#(y,times(p(s(x)),y)) (12)
times#(s(x),y) times#(p(s(x)),y) (13)
times#(s(x),y) p#(s(x)) (14)
p#(s(s(x))) p#(s(x)) (15)
fac#(s(x),y) fac#(p(s(x)),times(s(x),y)) (16)
fac#(s(x),y) p#(s(x)) (17)
fac#(s(x),y) times#(s(x),y) (18)
factorial#(x) fac#(x,s(0)) (19)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.