The rewrite relation of the following TRS is considered.
a__eq(0,0) | → | true | (1) |
a__eq(s(X),s(Y)) | → | a__eq(X,Y) | (2) |
a__eq(X,Y) | → | false | (3) |
a__inf(X) | → | cons(X,inf(s(X))) | (4) |
a__take(0,X) | → | nil | (5) |
a__take(s(X),cons(Y,L)) | → | cons(Y,take(X,L)) | (6) |
a__length(nil) | → | 0 | (7) |
a__length(cons(X,L)) | → | s(length(L)) | (8) |
mark(eq(X1,X2)) | → | a__eq(X1,X2) | (9) |
mark(inf(X)) | → | a__inf(mark(X)) | (10) |
mark(take(X1,X2)) | → | a__take(mark(X1),mark(X2)) | (11) |
mark(length(X)) | → | a__length(mark(X)) | (12) |
mark(0) | → | 0 | (13) |
mark(true) | → | true | (14) |
mark(s(X)) | → | s(X) | (15) |
mark(false) | → | false | (16) |
mark(cons(X1,X2)) | → | cons(X1,X2) | (17) |
mark(nil) | → | nil | (18) |
a__eq(X1,X2) | → | eq(X1,X2) | (19) |
a__inf(X) | → | inf(X) | (20) |
a__take(X1,X2) | → | take(X1,X2) | (21) |
a__length(X) | → | length(X) | (22) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
a__eq#(0,0) |
a__eq#(s(z0),s(z1)) |
a__eq#(z0,z1) |
a__eq#(z0,z1) |
a__inf#(z0) |
a__inf#(z0) |
a__take#(0,z0) |
a__take#(s(z0),cons(z1,z2)) |
a__take#(z0,z1) |
a__length#(nil) |
a__length#(cons(z0,z1)) |
a__length#(z0) |
mark#(eq(z0,z1)) |
mark#(inf(z0)) |
mark#(take(z0,z1)) |
mark#(length(z0)) |
mark#(0) |
mark#(true) |
mark#(s(z0)) |
mark#(false) |
mark#(cons(z0,z1)) |
mark#(nil) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__inf(x1)] | = | 1 + 1 · x1 |
[a__take(x1, x2)] | = | 1 + 1 · x2 |
[a__length(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 + 1 · x1 |
[a__eq#(x1, x2)] | = | 0 |
[a__inf#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | 0 |
[a__length#(x1)] | = | 0 |
[mark#(x1)] | = | 1 · x1 + 0 |
[eq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[length(x1)] | = | 1 + 1 · x1 |
[0] | = | 0 |
[true] | = | 0 |
[s(x1)] | = | 0 |
[false] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 |
[nil] | = | 0 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__inf(x1)] | = | 1 + 1 · x1 |
[a__take(x1, x2)] | = | 1 + 1 · x2 |
[a__length(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 + 1 · x1 |
[a__eq#(x1, x2)] | = | 0 |
[a__inf#(x1)] | = | 1 |
[a__take#(x1, x2)] | = | 0 |
[a__length#(x1)] | = | 0 |
[mark#(x1)] | = | 1 · x1 + 0 |
[eq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[length(x1)] | = | 1 + 1 · x1 |
[0] | = | 0 |
[true] | = | 1 |
[s(x1)] | = | 1 |
[false] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 |
[nil] | = | 0 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
mark#(0) | → | c16 | (53) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__inf(x1)] | = | 1 + 1 · x1 |
[a__take(x1, x2)] | = | 1 + 1 · x2 |
[a__length(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 + 1 · x1 |
[a__eq#(x1, x2)] | = | 1 · x1 + 0 |
[a__inf#(x1)] | = | 1 |
[a__take#(x1, x2)] | = | 0 |
[a__length#(x1)] | = | 0 |
[mark#(x1)] | = | 1 · x1 + 0 |
[eq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[length(x1)] | = | 1 · x1 + 0 |
[0] | = | 1 |
[true] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[false] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 |
[nil] | = | 0 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__inf(x1)] | = | 1 + 1 · x1 |
[a__take(x1, x2)] | = | 1 + 1 · x2 |
[a__length(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 + 1 · x1 |
[a__eq#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[a__inf#(x1)] | = | 1 |
[a__take#(x1, x2)] | = | 0 |
[a__length#(x1)] | = | 1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[eq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[length(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
[true] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[false] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 |
[nil] | = | 0 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(nil) | → | c21 | (60) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__inf(x1)] | = | 1 + 1 · x1 |
[a__take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__length(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 + 1 · x1 |
[a__eq#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[a__inf#(x1)] | = | 1 |
[a__take#(x1, x2)] | = | 0 |
[a__length#(x1)] | = | 1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[eq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[length(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
[true] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[false] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 3 + 3 · x1 + 3 · x2 |
[a__inf(x1)] | = | 3 |
[a__take(x1, x2)] | = | 3 |
[a__length(x1)] | = | 3 + 3 · x1 |
[mark(x1)] | = | 3 · x1 + 0 |
[a__eq#(x1, x2)] | = | 3 |
[a__inf#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | 0 |
[a__length#(x1)] | = | 0 |
[mark#(x1)] | = | 2 · x1 + 0 |
[eq(x1, x2)] | = | 2 + 1 · x1 + 1 · x2 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[length(x1)] | = | 1 · x1 + 0 |
[0] | = | 0 |
[true] | = | 3 |
[s(x1)] | = | 0 |
[false] | = | 3 |
[cons(x1, x2)] | = | 1 · x1 + 0 |
[nil] | = | 0 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c14(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16] | = | 0 |
[c17] | = | 0 |
[c18] | = | 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[a__eq(x1, x2)] | = | 1 |
[a__inf(x1)] | = | 1 + 1 · x1 |
[a__take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__length(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 · x1 + 0 |
[a__eq#(x1, x2)] | = | 1 |
[a__inf#(x1)] | = | 1 |
[a__take#(x1, x2)] | = | 1 |
[a__length#(x1)] | = | 1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[eq(x1, x2)] | = | 1 |
[inf(x1)] | = | 1 + 1 · x1 |
[take(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[length(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
[true] | = | 1 |
[s(x1)] | = | 1 |
[false] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 |
[nil] | = | 1 |
a__eq#(0,0) | → | c | (23) |
a__eq#(s(z0),s(z1)) | → | c1(a__eq#(z0,z1)) | (25) |
a__eq#(z0,z1) | → | c2 | (27) |
a__eq#(z0,z1) | → | c3 | (29) |
a__inf#(z0) | → | c4 | (31) |
a__inf#(z0) | → | c5 | (33) |
a__take#(0,z0) | → | c6 | (35) |
a__take#(s(z0),cons(z1,z2)) | → | c7 | (37) |
a__take#(z0,z1) | → | c8 | (39) |
a__length#(nil) | → | c9 | (40) |
a__length#(cons(z0,z1)) | → | c10 | (42) |
a__length#(z0) | → | c11 | (44) |
mark#(eq(z0,z1)) | → | c12(a__eq#(z0,z1)) | (46) |
mark#(inf(z0)) | → | c13(a__inf#(mark(z0)),mark#(z0)) | (48) |
mark#(take(z0,z1)) | → | c14(a__take#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (50) |
mark#(length(z0)) | → | c15(a__length#(mark(z0)),mark#(z0)) | (52) |
mark#(0) | → | c16 | (53) |
mark#(true) | → | c17 | (54) |
mark#(s(z0)) | → | c18 | (56) |
mark#(false) | → | c19 | (57) |
mark#(cons(z0,z1)) | → | c20 | (59) |
mark#(nil) | → | c21 | (60) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).