Certification Problem

Input (TPDB TRS_Standard/CiME_04/list-sum-prod)

The rewrite relation of the following TRS is considered.

+(x,0) x (1)
+(0,x) x (2)
+(s(x),s(y)) s(s(+(x,y))) (3)
*(x,0) 0 (4)
*(0,x) 0 (5)
*(s(x),s(y)) s(+(*(x,y),+(x,y))) (6)
sum(nil) 0 (7)
sum(cons(x,l)) +(x,sum(l)) (8)
prod(nil) s(0) (9)
prod(cons(x,l)) *(x,prod(l)) (10)

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

1.1 R is empty

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