Certification Problem

Input (TPDB TRS_Standard/AProVE_06/sizeChange)

The rewrite relation of the following TRS is considered.

r(xs,ys,zs,nil) → xs (1)
r(xs,nil,zs,cons(w,ws)) → r(xs,xs,cons(succ(zero),zs),ws) (2)
r(xs,cons(y,ys),nil,cons(w,ws)) → r(xs,xs,cons(succ(zero),nil),ws) (3)
r(xs,cons(y,ys),cons(z,zs),cons(w,ws)) → r(ys,cons(y,ys),zs,cons(succ(zero),cons(w,ws))) (4)

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.
r#(xs,nil,zs,cons(w,ws)) → r#(xs,xs,cons(succ(zero),zs),ws) (5)
r#(xs,cons(y,ys),nil,cons(w,ws)) → r#(xs,xs,cons(succ(zero),nil),ws) (6)
r#(xs,cons(y,ys),cons(z,zs),cons(w,ws)) → r#(ys,cons(y,ys),zs,cons(succ(zero),cons(w,ws))) (7)

1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

r#(xs,nil,zs,cons(w,ws)) → r#(xs,xs,cons(succ(zero),zs),ws) (5)
4 > 4
1 ≥ 2
1 ≥ 1
r#(xs,cons(y,ys),nil,cons(w,ws)) → r#(xs,xs,cons(succ(zero),nil),ws) (6)
4 > 4
1 ≥ 2
1 ≥ 1
r#(xs,cons(y,ys),cons(z,zs),cons(w,ws)) → r#(ys,cons(y,ys),zs,cons(succ(zero),cons(w,ws))) (7)
3 > 3
2 ≥ 2
2 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.