Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/sigma)

The rewrite relation of the following TRS is considered.

comp(s,id) → s (1)
cons(one,shift) → id (2)
cons(comp(one,s),comp(shift,s)) → s (3)
comp(one,cons(s,t)) → s (4)
comp(shift,cons(s,t)) → t (5)
comp(abs(s),t) → abs(comp(s,cons(one,comp(t,shift)))) (6)
comp(cons(s,t),u) → cons(comp(s,u),comp(t,u)) (7)
comp(id,s) → s (8)
comp(comp(s,t),u) → comp(s,comp(t,u)) (9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the Weighted Path Order with the following precedence and status
prec(abs) = 0 status(abs) = [1] list-extension(abs) = Lex
prec(cons) = 2 status(cons) = [2, 1] list-extension(cons) = Lex
prec(shift) = 0 status(shift) = [] list-extension(shift) = Lex
prec(one) = 0 status(one) = [] list-extension(one) = Lex
prec(comp) = 3 status(comp) = [1, 2] list-extension(comp) = Lex
prec(id) = 0 status(id) = [] list-extension(id) = Lex
and the following Max-polynomial interpretation
[abs(x1)] = 1 + 1 · x1
[cons(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[shift] = 0
[one] = max(0)
[comp(x1, x2)] = 0 + 1 · x1 + 1 · x2
[id] = max(0)
all of the following rules can be deleted.
comp(s,id) → s (1)
cons(one,shift) → id (2)
cons(comp(one,s),comp(shift,s)) → s (3)
comp(one,cons(s,t)) → s (4)
comp(shift,cons(s,t)) → t (5)
comp(abs(s),t) → abs(comp(s,cons(one,comp(t,shift)))) (6)
comp(cons(s,t),u) → cons(comp(s,u),comp(t,u)) (7)
comp(id,s) → s (8)
comp(comp(s,t),u) → comp(s,comp(t,u)) (9)

1.1 R is empty

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