Certification Problem

Input (TPDB TRS_Standard/AG01/#3.17a)

The rewrite relation of the following TRS is considered.

app(nil,k) k (1)
app(l,nil) l (2)
app(cons(x,l),k) cons(x,app(l,k)) (3)
sum(cons(x,nil)) cons(x,nil) (4)
sum(cons(x,cons(y,l))) sum(cons(plus(x,y),l)) (5)
sum(app(l,cons(x,cons(y,k)))) sum(app(l,sum(cons(x,cons(y,k))))) (6)
plus(0,y) y (7)
plus(s(x),y) s(plus(x,y)) (8)
sum(plus(cons(0,x),cons(y,l))) pred(sum(cons(s(x),cons(y,l)))) (9)
pred(cons(s(x),nil)) cons(x,nil) (10)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
sum#(app(l,cons(x,cons(y,k)))) app#(l,sum(cons(x,cons(y,k)))) (11)
sum#(cons(x,cons(y,l))) sum#(cons(plus(x,y),l)) (12)
plus#(s(x),y) plus#(x,y) (13)
sum#(cons(x,cons(y,l))) plus#(x,y) (14)
sum#(plus(cons(0,x),cons(y,l))) sum#(cons(s(x),cons(y,l))) (15)
sum#(app(l,cons(x,cons(y,k)))) sum#(cons(x,cons(y,k))) (16)
sum#(app(l,cons(x,cons(y,k)))) sum#(app(l,sum(cons(x,cons(y,k))))) (17)
app#(cons(x,l),k) app#(l,k) (18)
sum#(plus(cons(0,x),cons(y,l))) pred#(sum(cons(s(x),cons(y,l)))) (19)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.