The rewrite relation of the following TRS is considered.
a__and(true,X) | → | mark(X) | (1) |
a__and(false,Y) | → | false | (2) |
a__if(true,X,Y) | → | mark(X) | (3) |
a__if(false,X,Y) | → | mark(Y) | (4) |
a__add(0,X) | → | mark(X) | (5) |
a__add(s(X),Y) | → | s(add(X,Y)) | (6) |
a__first(0,X) | → | nil | (7) |
a__first(s(X),cons(Y,Z)) | → | cons(Y,first(X,Z)) | (8) |
a__from(X) | → | cons(X,from(s(X))) | (9) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (10) |
mark(if(X1,X2,X3)) | → | a__if(mark(X1),X2,X3) | (11) |
mark(add(X1,X2)) | → | a__add(mark(X1),X2) | (12) |
mark(first(X1,X2)) | → | a__first(mark(X1),mark(X2)) | (13) |
mark(from(X)) | → | a__from(X) | (14) |
mark(true) | → | true | (15) |
mark(false) | → | false | (16) |
mark(0) | → | 0 | (17) |
mark(s(X)) | → | s(X) | (18) |
mark(nil) | → | nil | (19) |
mark(cons(X1,X2)) | → | cons(X1,X2) | (20) |
a__and(X1,X2) | → | and(X1,X2) | (21) |
a__if(X1,X2,X3) | → | if(X1,X2,X3) | (22) |
a__add(X1,X2) | → | add(X1,X2) | (23) |
a__first(X1,X2) | → | first(X1,X2) | (24) |
a__from(X) | → | from(X) | (25) |
|
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 |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
a__and#(true,z0) |
a__and#(false,z0) |
a__and#(z0,z1) |
a__if#(true,z0,z1) |
a__if#(false,z0,z1) |
a__if#(z0,z1,z2) |
a__add#(0,z0) |
a__add#(s(z0),z1) |
a__add#(z0,z1) |
a__first#(0,z0) |
a__first#(s(z0),cons(z1,z2)) |
a__first#(z0,z1) |
a__from#(z0) |
a__from#(z0) |
mark#(and(z0,z1)) |
mark#(if(z0,z1,z2)) |
mark#(add(z0,z1)) |
mark#(first(z0,z1)) |
mark#(from(z0)) |
mark#(true) |
mark#(false) |
mark#(0) |
mark#(s(z0)) |
mark#(nil) |
mark#(cons(z0,z1)) |
a__from#(z0) | → | c12 | (51) |
a__from#(z0) | → | c13 | (53) |
mark#(and(z0,z1)) | → | c14(a__and#(mark(z0),z1),mark#(z0)) | (55) |
mark#(if(z0,z1,z2)) | → | c15(a__if#(mark(z0),z1,z2),mark#(z0)) | (57) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12] | = | 0 |
[c13] | = | 0 |
[c14(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c17(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24] | = | 0 |
[a__and(x1, x2)] | = | 3 + 3 · x2 |
[a__if(x1, x2, x3)] | = | 3 + 3 · x2 + 3 · x3 |
[a__add(x1, x2)] | = | 3 + 3 · x2 |
[a__first(x1, x2)] | = | 3 + 3 · x1 + 3 · x2 |
[a__from(x1)] | = | 3 + 3 · x1 |
[mark(x1)] | = | 3 · x1 + 0 |
[a__and#(x1, x2)] | = | 1 · x2 + 0 |
[a__if#(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 |
[a__add#(x1, x2)] | = | 1 · x2 + 0 |
[a__first#(x1, x2)] | = | 0 |
[a__from#(x1)] | = | 2 + 1 · x1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[add(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[first(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[from(x1)] | = | 2 + 1 · x1 |
[true] | = | 0 |
[false] | = | 0 |
[0] | = | 0 |
[s(x1)] | = | 0 |
[nil] | = | 0 |
[cons(x1, x2)] | = | 1 · x1 + 0 |
a__and#(true,z0) | → | c(mark#(z0)) | (27) |
a__and#(false,z0) | → | c1 | (29) |
a__and#(z0,z1) | → | c2 | (31) |
a__if#(true,z0,z1) | → | c3(mark#(z0)) | (33) |
a__if#(false,z0,z1) | → | c4(mark#(z1)) | (35) |
a__if#(z0,z1,z2) | → | c5 | (37) |
a__add#(0,z0) | → | c6(mark#(z0)) | (39) |
a__add#(s(z0),z1) | → | c7 | (41) |
a__add#(z0,z1) | → | c8 | (43) |
a__first#(0,z0) | → | c9 | (45) |
a__first#(s(z0),cons(z1,z2)) | → | c10 | (47) |
a__first#(z0,z1) | → | c11 | (49) |
a__from#(z0) | → | c12 | (51) |
a__from#(z0) | → | c13 | (53) |
mark#(and(z0,z1)) | → | c14(a__and#(mark(z0),z1),mark#(z0)) | (55) |
mark#(if(z0,z1,z2)) | → | c15(a__if#(mark(z0),z1,z2),mark#(z0)) | (57) |
mark#(add(z0,z1)) | → | c16(a__add#(mark(z0),z1),mark#(z0)) | (59) |
mark#(first(z0,z1)) | → | c17(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (61) |
mark#(from(z0)) | → | c18(a__from#(z0)) | (63) |
mark#(true) | → | c19 | (64) |
mark#(false) | → | c20 | (65) |
mark#(0) | → | c21 | (66) |
mark#(s(z0)) | → | c22 | (68) |
mark#(nil) | → | c23 | (69) |
mark#(cons(z0,z1)) | → | c24 | (71) |
a__add#(0,z0) | → | c6(mark#(z0)) | (39) |
a__add#(s(z0),z1) | → | c7 | (41) |
a__add#(z0,z1) | → | c8 | (43) |
mark#(first(z0,z1)) | → | c17(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (61) |
mark#(true) | → | c19 | (64) |
mark#(false) | → | c20 | (65) |
mark#(0) | → | c21 | (66) |
mark#(s(z0)) | → | c22 | (68) |
mark#(nil) | → | c23 | (69) |
mark#(cons(z0,z1)) | → | c24 | (71) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12] | = | 0 |
[c13] | = | 0 |
[c14(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c17(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24] | = | 0 |
[a__and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[a__add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__first(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__from(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 · x1 + 0 |
[a__and#(x1, x2)] | = | 1 · x2 + 0 |
[a__if#(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 |
[a__add#(x1, x2)] | = | 1 + 1 · x2 |
[a__first#(x1, x2)] | = | 0 |
[a__from#(x1)] | = | 1 + 1 · x1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[first(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[from(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
[false] | = | 1 |
[0] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[nil] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
a__and#(true,z0) | → | c(mark#(z0)) | (27) |
a__and#(false,z0) | → | c1 | (29) |
a__and#(z0,z1) | → | c2 | (31) |
a__if#(true,z0,z1) | → | c3(mark#(z0)) | (33) |
a__if#(false,z0,z1) | → | c4(mark#(z1)) | (35) |
a__if#(z0,z1,z2) | → | c5 | (37) |
a__add#(0,z0) | → | c6(mark#(z0)) | (39) |
a__add#(s(z0),z1) | → | c7 | (41) |
a__add#(z0,z1) | → | c8 | (43) |
a__first#(0,z0) | → | c9 | (45) |
a__first#(s(z0),cons(z1,z2)) | → | c10 | (47) |
a__first#(z0,z1) | → | c11 | (49) |
a__from#(z0) | → | c12 | (51) |
a__from#(z0) | → | c13 | (53) |
mark#(and(z0,z1)) | → | c14(a__and#(mark(z0),z1),mark#(z0)) | (55) |
mark#(if(z0,z1,z2)) | → | c15(a__if#(mark(z0),z1,z2),mark#(z0)) | (57) |
mark#(add(z0,z1)) | → | c16(a__add#(mark(z0),z1),mark#(z0)) | (59) |
mark#(first(z0,z1)) | → | c17(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (61) |
mark#(from(z0)) | → | c18(a__from#(z0)) | (63) |
mark#(true) | → | c19 | (64) |
mark#(false) | → | c20 | (65) |
mark#(0) | → | c21 | (66) |
mark#(s(z0)) | → | c22 | (68) |
mark#(nil) | → | c23 | (69) |
mark#(cons(z0,z1)) | → | c24 | (71) |
mark#(add(z0,z1)) | → | c16(a__add#(mark(z0),z1),mark#(z0)) | (59) |
mark#(from(z0)) | → | c18(a__from#(z0)) | (63) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12] | = | 0 |
[c13] | = | 0 |
[c14(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c17(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24] | = | 0 |
[a__and(x1, x2)] | = | 1 · x1 + 0 + 3 · x2 |
[a__if(x1, x2, x3)] | = | 1 · x1 + 0 + 3 · x2 + 3 · x3 |
[a__add(x1, x2)] | = | 3 + 1 · x1 + 3 · x2 |
[a__first(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[a__from(x1)] | = | 2 + 3 · x1 |
[mark(x1)] | = | 3 · x1 + 0 |
[a__and#(x1, x2)] | = | 1 · x2 + 0 |
[a__if#(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 |
[a__add#(x1, x2)] | = | 1 · x2 + 0 |
[a__first#(x1, x2)] | = | 0 |
[a__from#(x1)] | = | 1 · x1 + 0 |
[mark#(x1)] | = | 1 · x1 + 0 |
[and(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[first(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[from(x1)] | = | 1 + 1 · x1 |
[true] | = | 0 |
[false] | = | 0 |
[0] | = | 0 |
[s(x1)] | = | 1 + 1 · x1 |
[nil] | = | 0 |
[cons(x1, x2)] | = | 1 · x1 + 0 |
a__and#(true,z0) | → | c(mark#(z0)) | (27) |
a__and#(false,z0) | → | c1 | (29) |
a__and#(z0,z1) | → | c2 | (31) |
a__if#(true,z0,z1) | → | c3(mark#(z0)) | (33) |
a__if#(false,z0,z1) | → | c4(mark#(z1)) | (35) |
a__if#(z0,z1,z2) | → | c5 | (37) |
a__add#(0,z0) | → | c6(mark#(z0)) | (39) |
a__add#(s(z0),z1) | → | c7 | (41) |
a__add#(z0,z1) | → | c8 | (43) |
a__first#(0,z0) | → | c9 | (45) |
a__first#(s(z0),cons(z1,z2)) | → | c10 | (47) |
a__first#(z0,z1) | → | c11 | (49) |
a__from#(z0) | → | c12 | (51) |
a__from#(z0) | → | c13 | (53) |
mark#(and(z0,z1)) | → | c14(a__and#(mark(z0),z1),mark#(z0)) | (55) |
mark#(if(z0,z1,z2)) | → | c15(a__if#(mark(z0),z1,z2),mark#(z0)) | (57) |
mark#(add(z0,z1)) | → | c16(a__add#(mark(z0),z1),mark#(z0)) | (59) |
mark#(first(z0,z1)) | → | c17(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (61) |
mark#(from(z0)) | → | c18(a__from#(z0)) | (63) |
mark#(true) | → | c19 | (64) |
mark#(false) | → | c20 | (65) |
mark#(0) | → | c21 | (66) |
mark#(s(z0)) | → | c22 | (68) |
mark#(nil) | → | c23 | (69) |
mark#(cons(z0,z1)) | → | c24 | (71) |
a__and#(true,z0) | → | c(mark#(z0)) | (27) |
a__and#(false,z0) | → | c1 | (29) |
a__and#(z0,z1) | → | c2 | (31) |
a__if#(true,z0,z1) | → | c3(mark#(z0)) | (33) |
a__if#(false,z0,z1) | → | c4(mark#(z1)) | (35) |
a__if#(z0,z1,z2) | → | c5 | (37) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12] | = | 0 |
[c13] | = | 0 |
[c14(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c17(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24] | = | 0 |
[a__and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[a__add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__first(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__from(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 · x1 + 0 |
[a__and#(x1, x2)] | = | 1 + 1 · x2 |
[a__if#(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[a__add#(x1, x2)] | = | 1 + 1 · x2 |
[a__first#(x1, x2)] | = | 0 |
[a__from#(x1)] | = | 1 + 1 · x1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[first(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[from(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
[false] | = | 1 |
[0] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[nil] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
a__and#(true,z0) | → | c(mark#(z0)) | (27) |
a__and#(false,z0) | → | c1 | (29) |
a__and#(z0,z1) | → | c2 | (31) |
a__if#(true,z0,z1) | → | c3(mark#(z0)) | (33) |
a__if#(false,z0,z1) | → | c4(mark#(z1)) | (35) |
a__if#(z0,z1,z2) | → | c5 | (37) |
a__add#(0,z0) | → | c6(mark#(z0)) | (39) |
a__add#(s(z0),z1) | → | c7 | (41) |
a__add#(z0,z1) | → | c8 | (43) |
a__first#(0,z0) | → | c9 | (45) |
a__first#(s(z0),cons(z1,z2)) | → | c10 | (47) |
a__first#(z0,z1) | → | c11 | (49) |
a__from#(z0) | → | c12 | (51) |
a__from#(z0) | → | c13 | (53) |
mark#(and(z0,z1)) | → | c14(a__and#(mark(z0),z1),mark#(z0)) | (55) |
mark#(if(z0,z1,z2)) | → | c15(a__if#(mark(z0),z1,z2),mark#(z0)) | (57) |
mark#(add(z0,z1)) | → | c16(a__add#(mark(z0),z1),mark#(z0)) | (59) |
mark#(first(z0,z1)) | → | c17(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (61) |
mark#(from(z0)) | → | c18(a__from#(z0)) | (63) |
mark#(true) | → | c19 | (64) |
mark#(false) | → | c20 | (65) |
mark#(0) | → | c21 | (66) |
mark#(s(z0)) | → | c22 | (68) |
mark#(nil) | → | c23 | (69) |
mark#(cons(z0,z1)) | → | c24 | (71) |
a__first#(0,z0) | → | c9 | (45) |
a__first#(s(z0),cons(z1,z2)) | → | c10 | (47) |
a__first#(z0,z1) | → | c11 | (49) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10] | = | 0 |
[c11] | = | 0 |
[c12] | = | 0 |
[c13] | = | 0 |
[c14(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c15(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c16(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c17(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24] | = | 0 |
[a__and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[a__add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__first(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__from(x1)] | = | 1 + 1 · x1 |
[mark(x1)] | = | 1 · x1 + 0 |
[a__and#(x1, x2)] | = | 1 + 1 · x2 |
[a__if#(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[a__add#(x1, x2)] | = | 1 + 1 · x2 |
[a__first#(x1, x2)] | = | 1 |
[a__from#(x1)] | = | 1 + 1 · x1 |
[mark#(x1)] | = | 1 · x1 + 0 |
[and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[add(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[first(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[from(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
[false] | = | 1 |
[0] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[nil] | = | 1 |
[cons(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
a__and#(true,z0) | → | c(mark#(z0)) | (27) |
a__and#(false,z0) | → | c1 | (29) |
a__and#(z0,z1) | → | c2 | (31) |
a__if#(true,z0,z1) | → | c3(mark#(z0)) | (33) |
a__if#(false,z0,z1) | → | c4(mark#(z1)) | (35) |
a__if#(z0,z1,z2) | → | c5 | (37) |
a__add#(0,z0) | → | c6(mark#(z0)) | (39) |
a__add#(s(z0),z1) | → | c7 | (41) |
a__add#(z0,z1) | → | c8 | (43) |
a__first#(0,z0) | → | c9 | (45) |
a__first#(s(z0),cons(z1,z2)) | → | c10 | (47) |
a__first#(z0,z1) | → | c11 | (49) |
a__from#(z0) | → | c12 | (51) |
a__from#(z0) | → | c13 | (53) |
mark#(and(z0,z1)) | → | c14(a__and#(mark(z0),z1),mark#(z0)) | (55) |
mark#(if(z0,z1,z2)) | → | c15(a__if#(mark(z0),z1,z2),mark#(z0)) | (57) |
mark#(add(z0,z1)) | → | c16(a__add#(mark(z0),z1),mark#(z0)) | (59) |
mark#(first(z0,z1)) | → | c17(a__first#(mark(z0),mark(z1)),mark#(z0),mark#(z1)) | (61) |
mark#(from(z0)) | → | c18(a__from#(z0)) | (63) |
mark#(true) | → | c19 | (64) |
mark#(false) | → | c20 | (65) |
mark#(0) | → | c21 | (66) |
mark#(s(z0)) | → | c22 | (68) |
mark#(nil) | → | c23 | (69) |
mark#(cons(z0,z1)) | → | c24 | (71) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).