Certification Problem

Input (TPDB TRS_Standard/Rubio_04/revlist)

The rewrite relation of the following TRS is considered.

rev1(0,nil) 0 (1)
rev1(s(X),nil) s(X) (2)
rev1(X,cons(Y,L)) rev1(Y,L) (3)
rev(nil) nil (4)
rev(cons(X,L)) cons(rev1(X,L),rev2(X,L)) (5)
rev2(X,nil) nil (6)
rev2(X,cons(Y,L)) rev(cons(X,rev(rev2(Y,L)))) (7)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
rev2#(X,cons(Y,L)) rev#(rev2(Y,L)) (8)
rev1#(X,cons(Y,L)) rev1#(Y,L) (9)
rev#(cons(X,L)) rev2#(X,L) (10)
rev2#(X,cons(Y,L)) rev2#(Y,L) (11)
rev2#(X,cons(Y,L)) rev#(cons(X,rev(rev2(Y,L)))) (12)
rev#(cons(X,L)) rev1#(X,L) (13)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.