Certification Problem

Input (TPDB TRS_Standard/SK90/2.22)

The rewrite relation of the following TRS is considered.

exp(x,0) → s(0) (1)
exp(x,s(y)) → *(x,exp(x,y)) (2)
*(0,y) → 0 (3)
*(s(x),y) → +(y,*(x,y)) (4)
-(0,y) → 0 (5)
-(x,0) → x (6)
-(s(x),s(y)) → -(x,y) (7)

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(-) = 0 status(-) = [1, 2] list-extension(-) = Lex
prec(+) = 0 status(+) = [2, 1] list-extension(+) = Lex
prec(*) = 2 status(*) = [1, 2] list-extension(*) = Lex
prec(s) = 0 status(s) = [1] list-extension(s) = Lex
prec(exp) = 3 status(exp) = [1, 2] list-extension(exp) = Lex
prec(0) = 0 status(0) = [] list-extension(0) = Lex
and the following Max-polynomial interpretation
[-(x1, x2)] = max(1, 0 + 1 · x1, 5 + 1 · x2)
[+(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[*(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[s(x1)] = max(0, 1 + 1 · x1)
[exp(x1, x2)] = 2 + 1 · x1 + 1 · x2
[0] = max(0)
all of the following rules can be deleted.
exp(x,0) → s(0) (1)
exp(x,s(y)) → *(x,exp(x,y)) (2)
*(0,y) → 0 (3)
*(s(x),y) → +(y,*(x,y)) (4)
-(0,y) → 0 (5)
-(x,0) → x (6)
-(s(x),s(y)) → -(x,y) (7)

1.1 R is empty

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