Certification Problem

Input (TPDB TRS_Standard/Applicative_05/ReverseLastInit)

The rewrite relation of the following TRS is considered.

app(app(app(compose,f),g),x) → app(g,app(f,x)) (1)
app(reverse,l) → app(app(reverse2,l),nil) (2)
app(app(reverse2,nil),l) → l (3)
app(app(reverse2,app(app(cons,x),xs)),l) → app(app(reverse2,xs),app(app(cons,x),l)) (4)
app(hd,app(app(cons,x),xs)) → x (5)
app(tl,app(app(cons,x),xs)) → xs (6)
last → app(app(compose,hd),reverse) (7)
init → app(app(compose,reverse),app(app(compose,tl),reverse)) (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[nil] =
0 0 0
0 0 0
0 0 0
[last] =
1 0 0
1 0 0
1 0 0
[app(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 0
0 1 0
0 0 1
· x2 +
0 0 0
0 0 0
0 0 0
[reverse2] =
0 0 0
0 0 0
0 0 0
[cons] =
0 0 0
1 0 0
0 0 0
[compose] =
0 0 0
0 0 0
0 0 0
[tl] =
0 0 0
0 0 0
0 0 0
[init] =
1 0 0
0 0 0
1 0 0
[hd] =
1 0 0
1 0 0
0 0 0
[reverse] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
app(hd,app(app(cons,x),xs)) → x (5)
init → app(app(compose,reverse),app(app(compose,tl),reverse)) (8)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(last) = 5 weight(last) = 7
prec(tl) = 6 weight(tl) = 1
prec(hd) = 9 weight(hd) = 1
prec(cons) = 0 weight(cons) = 2
prec(nil) = 1 weight(nil) = 1
prec(reverse2) = 11 weight(reverse2) = 1
prec(reverse) = 8 weight(reverse) = 4
prec(app) = 4 weight(app) = 0
prec(compose) = 10 weight(compose) = 2
all of the following rules can be deleted.
app(app(app(compose,f),g),x) → app(g,app(f,x)) (1)
app(reverse,l) → app(app(reverse2,l),nil) (2)
app(app(reverse2,nil),l) → l (3)
app(app(reverse2,app(app(cons,x),xs)),l) → app(app(reverse2,xs),app(app(cons,x),l)) (4)
app(tl,app(app(cons,x),xs)) → xs (6)
last → app(app(compose,hd),reverse) (7)

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.