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,y),z) | → | +(x,+(y,z)) | (4) |
| *(x,0) | → | 0 | (5) |
| *(0,x) | → | 0 | (6) |
| *(s(x),s(y)) | → | s(+(*(x,y),+(x,y))) | (7) |
| *(*(x,y),z) | → | *(x,*(y,z)) | (8) |
| app(nil,l) | → | l | (9) |
| app(cons(x,l1),l2) | → | cons(x,app(l1,l2)) | (10) |
| sum(nil) | → | 0 | (11) |
| sum(cons(x,l)) | → | +(x,sum(l)) | (12) |
| sum(app(l1,l2)) | → | +(sum(l1),sum(l2)) | (13) |
| prod(nil) | → | s(0) | (14) |
| prod(cons(x,l)) | → | *(x,prod(l)) | (15) |
| prod(app(l1,l2)) | → | *(prod(l1),prod(l2)) | (16) |
| prec(prod) | = | 4 | status(prod) | = | [1] | list-extension(prod) | = | Lex | ||
| prec(sum) | = | 3 | status(sum) | = | [1] | list-extension(sum) | = | Lex | ||
| prec(cons) | = | 0 | status(cons) | = | [1, 2] | list-extension(cons) | = | Lex | ||
| prec(app) | = | 1 | status(app) | = | [1, 2] | list-extension(app) | = | Lex | ||
| prec(nil) | = | 12 | 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(+) | = | 2 | status(+) | = | [1, 2] | list-extension(+) | = | Lex | ||
| prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex |
| [prod(x1)] | = | 0 + 1 · x1 |
| [sum(x1)] | = | max(0, 0 + 1 · x1) |
| [cons(x1, x2)] | = | max(0, 4 + 1 · x1, 0 + 1 · x2) |
| [app(x1, x2)] | = | max(0, 6 + 1 · x1, 0 + 1 · x2) |
| [nil] | = | 0 |
| [*(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [s(x1)] | = | max(0, 0 + 1 · x1) |
| [+(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [0] | = | max(0) |
| +(x,0) | → | x | (1) |
| +(0,x) | → | x | (2) |
| +(s(x),s(y)) | → | s(s(+(x,y))) | (3) |
| +(+(x,y),z) | → | +(x,+(y,z)) | (4) |
| *(x,0) | → | 0 | (5) |
| *(0,x) | → | 0 | (6) |
| *(s(x),s(y)) | → | s(+(*(x,y),+(x,y))) | (7) |
| *(*(x,y),z) | → | *(x,*(y,z)) | (8) |
| app(nil,l) | → | l | (9) |
| app(cons(x,l1),l2) | → | cons(x,app(l1,l2)) | (10) |
| sum(nil) | → | 0 | (11) |
| sum(cons(x,l)) | → | +(x,sum(l)) | (12) |
| sum(app(l1,l2)) | → | +(sum(l1),sum(l2)) | (13) |
| prod(nil) | → | s(0) | (14) |
| prod(cons(x,l)) | → | *(x,prod(l)) | (15) |
| prod(app(l1,l2)) | → | *(prod(l1),prod(l2)) | (16) |
There are no rules in the TRS. Hence, it is terminating.