Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/reverse)

The rewrite relation of the following TRS is considered.

isEmpty(nil) true (1)
isEmpty(cons(x,xs)) false (2)
last(cons(x,nil)) x (3)
last(cons(x,cons(y,ys))) last(cons(y,ys)) (4)
dropLast(nil) nil (5)
dropLast(cons(x,nil)) nil (6)
dropLast(cons(x,cons(y,ys))) cons(x,dropLast(cons(y,ys))) (7)
append(nil,ys) ys (8)
append(cons(x,xs),ys) cons(x,append(xs,ys)) (9)
reverse(xs) rev(xs,nil) (10)
rev(xs,ys) if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys) (11)
if(true,xs,ys,zs) zs (12)
if(false,xs,ys,zs) rev(xs,ys) (13)

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.
last#(cons(x,cons(y,ys))) last#(cons(y,ys)) (14)
dropLast#(cons(x,cons(y,ys))) dropLast#(cons(y,ys)) (15)
append#(cons(x,xs),ys) append#(xs,ys) (16)
reverse#(xs) rev#(xs,nil) (17)
rev#(xs,ys) last#(xs) (18)
rev#(xs,ys) append#(ys,last(xs)) (19)
rev#(xs,ys) dropLast#(xs) (20)
rev#(xs,ys) isEmpty#(xs) (21)
rev#(xs,ys) if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys) (22)
if#(false,xs,ys,zs) rev#(xs,ys) (23)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.