Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe03)

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)
sum(plus(cons(0,x),cons(y,l))) pred(sum(cons(s(x),cons(y,l)))) (7)
pred(cons(s(x),nil)) cons(x,nil) (8)
plus(s(x),s(y)) s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) (9)
plus(s(x),x) plus(if(gt(x,x),id(x),id(x)),s(x)) (10)
plus(zero,y) y (11)
plus(id(x),s(y)) s(plus(x,if(gt(s(y),y),y,s(y)))) (12)
id(x) x (13)
if(true,x,y) x (14)
if(false,x,y) y (15)
not(x) if(x,false,true) (16)
gt(s(x),zero) true (17)
gt(zero,y) false (18)
gt(s(x),s(y)) gt(x,y) (19)

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.
app#(cons(x,l),k) app#(l,k) (20)
sum#(cons(x,cons(y,l))) sum#(cons(plus(x,y),l)) (21)
sum#(cons(x,cons(y,l))) plus#(x,y) (22)
sum#(app(l,cons(x,cons(y,k)))) sum#(app(l,sum(cons(x,cons(y,k))))) (23)
sum#(app(l,cons(x,cons(y,k)))) app#(l,sum(cons(x,cons(y,k)))) (24)
sum#(app(l,cons(x,cons(y,k)))) sum#(cons(x,cons(y,k))) (25)
sum#(plus(cons(0,x),cons(y,l))) pred#(sum(cons(s(x),cons(y,l)))) (26)
sum#(plus(cons(0,x),cons(y,l))) sum#(cons(s(x),cons(y,l))) (27)
plus#(s(x),s(y)) plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) (28)
plus#(s(x),s(y)) if#(gt(x,y),x,y) (29)
plus#(s(x),s(y)) gt#(x,y) (30)
plus#(s(x),s(y)) if#(not(gt(x,y)),id(x),id(y)) (31)
plus#(s(x),s(y)) not#(gt(x,y)) (32)
plus#(s(x),s(y)) id#(x) (33)
plus#(s(x),s(y)) id#(y) (34)
plus#(s(x),x) plus#(if(gt(x,x),id(x),id(x)),s(x)) (35)
plus#(s(x),x) if#(gt(x,x),id(x),id(x)) (36)
plus#(s(x),x) gt#(x,x) (37)
plus#(s(x),x) id#(x) (38)
plus#(id(x),s(y)) plus#(x,if(gt(s(y),y),y,s(y))) (39)
plus#(id(x),s(y)) if#(gt(s(y),y),y,s(y)) (40)
plus#(id(x),s(y)) gt#(s(y),y) (41)
not#(x) if#(x,false,true) (42)
gt#(s(x),s(y)) gt#(x,y) (43)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.