The rewrite relation of the following TRS is considered.
| f_0(x) | → | a | (1) |
| f_1(x) | → | g_1(x,x) | (2) |
| g_1(s(x),y) | → | b(f_0(y),g_1(x,y)) | (3) |
| f_2(x) | → | g_2(x,x) | (4) |
| g_2(s(x),y) | → | b(f_1(y),g_2(x,y)) | (5) |
| f_3(x) | → | g_3(x,x) | (6) |
| g_3(s(x),y) | → | b(f_2(y),g_3(x,y)) | (7) |
| f_4(x) | → | g_4(x,x) | (8) |
| g_4(s(x),y) | → | b(f_3(y),g_4(x,y)) | (9) |
| f_5(x) | → | g_5(x,x) | (10) |
| g_5(s(x),y) | → | b(f_4(y),g_5(x,y)) | (11) |
| prec(g_5) | = | 13 | status(g_5) | = | [2, 1] | list-extension(g_5) | = | Lex | ||
| prec(f_5) | = | 0 | status(f_5) | = | [1] | list-extension(f_5) | = | Lex | ||
| prec(g_4) | = | 9 | status(g_4) | = | [1, 2] | list-extension(g_4) | = | Lex | ||
| prec(f_4) | = | 12 | status(f_4) | = | [1] | list-extension(f_4) | = | Lex | ||
| prec(g_3) | = | 11 | status(g_3) | = | [1, 2] | list-extension(g_3) | = | Lex | ||
| prec(f_3) | = | 0 | status(f_3) | = | [1] | list-extension(f_3) | = | Lex | ||
| prec(g_2) | = | 8 | status(g_2) | = | [2, 1] | list-extension(g_2) | = | Lex | ||
| prec(f_2) | = | 9 | status(f_2) | = | [1] | list-extension(f_2) | = | Lex | ||
| prec(b) | = | 0 | status(b) | = | [2, 1] | list-extension(b) | = | Lex | ||
| prec(s) | = | 0 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
| prec(g_1) | = | 2 | status(g_1) | = | [2, 1] | list-extension(g_1) | = | Lex | ||
| prec(f_1) | = | 4 | status(f_1) | = | [1] | list-extension(f_1) | = | Lex | ||
| prec(a) | = | 0 | status(a) | = | [] | list-extension(a) | = | Lex | ||
| prec(f_0) | = | 1 | status(f_0) | = | [1] | list-extension(f_0) | = | Lex |
| [g_5(x1, x2)] | = | max(2, 2 + 1 · x1, 1 + 1 · x2) |
| [f_5(x1)] | = | 7 + 1 · x1 |
| [g_4(x1, x2)] | = | max(1, 1 + 1 · x1, 1 + 1 · x2) |
| [f_4(x1)] | = | max(0, 1 + 1 · x1) |
| [g_3(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_3(x1)] | = | 1 + 1 · x1 |
| [g_2(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_2(x1)] | = | max(0, 0 + 1 · x1) |
| [b(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [s(x1)] | = | 0 + 1 · x1 |
| [g_1(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_1(x1)] | = | max(0, 0 + 1 · x1) |
| [a] | = | max(0) |
| [f_0(x1)] | = | 0 + 1 · x1 |
| f_0(x) | → | a | (1) |
| f_1(x) | → | g_1(x,x) | (2) |
| g_1(s(x),y) | → | b(f_0(y),g_1(x,y)) | (3) |
| f_2(x) | → | g_2(x,x) | (4) |
| g_2(s(x),y) | → | b(f_1(y),g_2(x,y)) | (5) |
| f_3(x) | → | g_3(x,x) | (6) |
| g_3(s(x),y) | → | b(f_2(y),g_3(x,y)) | (7) |
| f_4(x) | → | g_4(x,x) | (8) |
| g_4(s(x),y) | → | b(f_3(y),g_4(x,y)) | (9) |
| f_5(x) | → | g_5(x,x) | (10) |
| g_5(s(x),y) | → | b(f_4(y),g_5(x,y)) | (11) |
There are no rules in the TRS. Hence, it is terminating.