Certification Problem

Input (TPDB TRS_Standard/AProVE_07/otto01)

The rewrite relation of the following TRS is considered.

min(0,y) 0 (1)
min(s(x),0) 0 (2)
min(s(x),s(y)) min(x,y) (3)
len(nil) 0 (4)
len(cons(x,xs)) s(len(xs)) (5)
sum(x,0) x (6)
sum(x,s(y)) s(sum(x,y)) (7)
le(0,x) true (8)
le(s(x),0) false (9)
le(s(x),s(y)) le(x,y) (10)
take(0,cons(y,ys)) y (11)
take(s(x),cons(y,ys)) take(x,ys) (12)
addList(x,y) if(le(0,min(len(x),len(y))),0,x,y,nil) (13)
if(false,c,x,y,z) z (14)
if(true,c,xs,ys,z) if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) (15)

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.
min#(s(x),s(y)) min#(x,y) (16)
len#(cons(x,xs)) len#(xs) (17)
sum#(x,s(y)) sum#(x,y) (18)
le#(s(x),s(y)) le#(x,y) (19)
take#(s(x),cons(y,ys)) take#(x,ys) (20)
addList#(x,y) if#(le(0,min(len(x),len(y))),0,x,y,nil) (21)
addList#(x,y) le#(0,min(len(x),len(y))) (22)
addList#(x,y) min#(len(x),len(y)) (23)
addList#(x,y) len#(x) (24)
addList#(x,y) len#(y) (25)
if#(true,c,xs,ys,z) if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) (26)
if#(true,c,xs,ys,z) le#(s(c),min(len(xs),len(ys))) (27)
if#(true,c,xs,ys,z) min#(len(xs),len(ys)) (28)
if#(true,c,xs,ys,z) len#(xs) (29)
if#(true,c,xs,ys,z) len#(ys) (30)
if#(true,c,xs,ys,z) sum#(take(c,xs),take(c,ys)) (31)
if#(true,c,xs,ys,z) take#(c,xs) (32)
if#(true,c,xs,ys,z) take#(c,ys) (33)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.