Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann08)

The rewrite relation of the following TRS is considered.

empty(nil) true (1)
empty(cons(x,l)) false (2)
head(cons(x,l)) x (3)
tail(nil) nil (4)
tail(cons(x,l)) l (5)
rev(nil) nil (6)
rev(cons(x,l)) cons(rev1(x,l),rev2(x,l)) (7)
last(x,l) if(empty(l),x,l) (8)
if(true,x,l) x (9)
if(false,x,l) last(head(l),tail(l)) (10)
rev2(x,nil) nil (11)
rev2(x,cons(y,l)) rev(cons(x,rev2(y,l))) (12)

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.
rev#(cons(x,l)) rev2#(x,l) (13)
last#(x,l) if#(empty(l),x,l) (14)
last#(x,l) empty#(l) (15)
if#(false,x,l) last#(head(l),tail(l)) (16)
if#(false,x,l) head#(l) (17)
if#(false,x,l) tail#(l) (18)
rev2#(x,cons(y,l)) rev#(cons(x,rev2(y,l))) (19)
rev2#(x,cons(y,l)) rev2#(y,l) (20)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.