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) |
| f_6(x) | → | g_6(x,x) | (12) |
| g_6(s(x),y) | → | b(f_5(y),g_6(x,y)) | (13) |
| f_7(x) | → | g_7(x,x) | (14) |
| g_7(s(x),y) | → | b(f_6(y),g_7(x,y)) | (15) |
| f_8(x) | → | g_8(x,x) | (16) |
| g_8(s(x),y) | → | b(f_7(y),g_8(x,y)) | (17) |
| f_9(x) | → | g_9(x,x) | (18) |
| g_9(s(x),y) | → | b(f_8(y),g_9(x,y)) | (19) |
| f_10(x) | → | g_10(x,x) | (20) |
| g_10(s(x),y) | → | b(f_9(y),g_10(x,y)) | (21) |
| prec(g_10) | = | 9 | status(g_10) | = | [2, 1] | list-extension(g_10) | = | Lex | ||
| prec(f_10) | = | 10 | status(f_10) | = | [1] | list-extension(f_10) | = | Lex | ||
| prec(g_9) | = | 31 | status(g_9) | = | [1, 2] | list-extension(g_9) | = | Lex | ||
| prec(f_9) | = | 0 | status(f_9) | = | [1] | list-extension(f_9) | = | Lex | ||
| prec(g_8) | = | 29 | status(g_8) | = | [2, 1] | list-extension(g_8) | = | Lex | ||
| prec(f_8) | = | 30 | status(f_8) | = | [1] | list-extension(f_8) | = | Lex | ||
| prec(g_7) | = | 27 | status(g_7) | = | [2, 1] | list-extension(g_7) | = | Lex | ||
| prec(f_7) | = | 28 | status(f_7) | = | [1] | list-extension(f_7) | = | Lex | ||
| prec(g_6) | = | 24 | status(g_6) | = | [2, 1] | list-extension(g_6) | = | Lex | ||
| prec(f_6) | = | 26 | status(f_6) | = | [1] | list-extension(f_6) | = | Lex | ||
| prec(g_5) | = | 20 | status(g_5) | = | [1, 2] | list-extension(g_5) | = | Lex | ||
| prec(f_5) | = | 21 | status(f_5) | = | [1] | list-extension(f_5) | = | Lex | ||
| prec(g_4) | = | 16 | status(g_4) | = | [1, 2] | list-extension(g_4) | = | Lex | ||
| prec(f_4) | = | 18 | status(f_4) | = | [1] | list-extension(f_4) | = | Lex | ||
| prec(g_3) | = | 8 | status(g_3) | = | [1, 2] | list-extension(g_3) | = | Lex | ||
| prec(f_3) | = | 9 | status(f_3) | = | [1] | list-extension(f_3) | = | Lex | ||
| prec(g_2) | = | 6 | status(g_2) | = | [1, 2] | list-extension(g_2) | = | Lex | ||
| prec(f_2) | = | 7 | 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) | = | 4 | status(g_1) | = | [1, 2] | list-extension(g_1) | = | Lex | ||
| prec(f_1) | = | 5 | status(f_1) | = | [1] | list-extension(f_1) | = | Lex | ||
| prec(a) | = | 0 | status(a) | = | [] | list-extension(a) | = | Lex | ||
| prec(f_0) | = | 2 | status(f_0) | = | [1] | list-extension(f_0) | = | Lex |
| [g_10(x1, x2)] | = | max(0, 6 + 1 · x1, 2 + 1 · x2) |
| [f_10(x1)] | = | max(0, 6 + 1 · x1) |
| [g_9(x1, x2)] | = | max(1, 0 + 1 · x1, 0 + 1 · x2) |
| [f_9(x1)] | = | 2 + 1 · x1 |
| [g_8(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_8(x1)] | = | max(0, 0 + 1 · x1) |
| [g_7(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_7(x1)] | = | max(0, 0 + 1 · x1) |
| [g_6(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_6(x1)] | = | 0 + 1 · x1 |
| [g_5(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_5(x1)] | = | max(0, 0 + 1 · x1) |
| [g_4(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_4(x1)] | = | max(0, 0 + 1 · x1) |
| [g_3(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [f_3(x1)] | = | max(0, 0 + 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)] | = | max(0, 2 + 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)] | = | max(2, 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) |
| f_6(x) | → | g_6(x,x) | (12) |
| g_6(s(x),y) | → | b(f_5(y),g_6(x,y)) | (13) |
| f_7(x) | → | g_7(x,x) | (14) |
| g_7(s(x),y) | → | b(f_6(y),g_7(x,y)) | (15) |
| f_8(x) | → | g_8(x,x) | (16) |
| g_8(s(x),y) | → | b(f_7(y),g_8(x,y)) | (17) |
| f_9(x) | → | g_9(x,x) | (18) |
| g_9(s(x),y) | → | b(f_8(y),g_9(x,y)) | (19) |
| f_10(x) | → | g_10(x,x) | (20) |
| g_10(s(x),y) | → | b(f_9(y),g_10(x,y)) | (21) |
There are no rules in the TRS. Hence, it is terminating.