Certification Problem

Input (TPDB TRS_Standard/AG01/#3.53)

The rewrite relation of the following TRS is considered.

minus(x,0) x (1)
minus(s(x),s(y)) minus(x,y) (2)
quot(0,s(y)) 0 (3)
quot(s(x),s(y)) s(quot(minus(x,y),s(y))) (4)
app(nil,y) y (5)
app(add(n,x),y) add(n,app(x,y)) (6)
reverse(nil) nil (7)
reverse(add(n,x)) app(reverse(x),add(n,nil)) (8)
shuffle(nil) nil (9)
shuffle(add(n,x)) add(n,shuffle(reverse(x))) (10)
concat(leaf,y) y (11)
concat(cons(u,v),y) cons(u,concat(v,y)) (12)
less_leaves(x,leaf) false (13)
less_leaves(leaf,cons(w,z)) true (14)
less_leaves(cons(u,v),cons(w,z)) less_leaves(concat(u,v),concat(w,z)) (15)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
minus#(s(x),s(y)) minus#(x,y) (16)
quot#(s(x),s(y)) minus#(x,y) (17)
quot#(s(x),s(y)) quot#(minus(x,y),s(y)) (18)
app#(add(n,x),y) app#(x,y) (19)
reverse#(add(n,x)) reverse#(x) (20)
reverse#(add(n,x)) app#(reverse(x),add(n,nil)) (21)
shuffle#(add(n,x)) reverse#(x) (22)
shuffle#(add(n,x)) shuffle#(reverse(x)) (23)
concat#(cons(u,v),y) concat#(v,y) (24)
less_leaves#(cons(u,v),cons(w,z)) concat#(w,z) (25)
less_leaves#(cons(u,v),cons(w,z)) concat#(u,v) (26)
less_leaves#(cons(u,v),cons(w,z)) less_leaves#(concat(u,v),concat(w,z)) (27)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.