The relative rewrite relation R/S is considered where R is the following TRS
#equal(@x,@y) | → | #eq(@x,@y) | (1) |
#less(@x,@y) | → | #cklt(#compare(@x,@y)) | (2) |
and(@x,@y) | → | #and(@x,@y) | (3) |
insert(@x,@l) | → | insert#1(@l,@x) | (4) |
insert#1(::(@y,@ys),@x) | → | insert#2(leq(@x,@y),@x,@y,@ys) | (5) |
insert#1(nil,@x) | → | ::(@x,nil) | (6) |
insert#2(#false,@x,@y,@ys) | → | ::(@y,insert(@x,@ys)) | (7) |
insert#2(#true,@x,@y,@ys) | → | ::(@x,::(@y,@ys)) | (8) |
isortlist(@l) | → | isortlist#1(@l) | (9) |
isortlist#1(::(@x,@xs)) | → | insert(@x,isortlist(@xs)) | (10) |
isortlist#1(nil) | → | nil | (11) |
leq(@l1,@l2) | → | leq#1(@l1,@l2) | (12) |
leq#1(::(@x,@xs),@l2) | → | leq#2(@l2,@x,@xs) | (13) |
leq#1(nil,@l2) | → | #true | (14) |
leq#2(::(@y,@ys),@x,@xs) | → | or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) | (15) |
leq#2(nil,@x,@xs) | → | #false | (16) |
or(@x,@y) | → | #or(@x,@y) | (17) |
and S is the following TRS.
#and(#false,#false) | → | #false | (18) |
#and(#false,#true) | → | #false | (19) |
#and(#true,#false) | → | #false | (20) |
#and(#true,#true) | → | #true | (21) |
#cklt(#EQ) | → | #false | (22) |
#cklt(#GT) | → | #false | (23) |
#cklt(#LT) | → | #true | (24) |
#compare(#0,#0) | → | #EQ | (25) |
#compare(#0,#neg(@y)) | → | #GT | (26) |
#compare(#0,#pos(@y)) | → | #LT | (27) |
#compare(#0,#s(@y)) | → | #LT | (28) |
#compare(#neg(@x),#0) | → | #LT | (29) |
#compare(#neg(@x),#neg(@y)) | → | #compare(@y,@x) | (30) |
#compare(#neg(@x),#pos(@y)) | → | #LT | (31) |
#compare(#pos(@x),#0) | → | #GT | (32) |
#compare(#pos(@x),#neg(@y)) | → | #GT | (33) |
#compare(#pos(@x),#pos(@y)) | → | #compare(@x,@y) | (34) |
#compare(#s(@x),#0) | → | #GT | (35) |
#compare(#s(@x),#s(@y)) | → | #compare(@x,@y) | (36) |
#eq(#0,#0) | → | #true | (37) |
#eq(#0,#neg(@y)) | → | #false | (38) |
#eq(#0,#pos(@y)) | → | #false | (39) |
#eq(#0,#s(@y)) | → | #false | (40) |
#eq(#neg(@x),#0) | → | #false | (41) |
#eq(#neg(@x),#neg(@y)) | → | #eq(@x,@y) | (42) |
#eq(#neg(@x),#pos(@y)) | → | #false | (43) |
#eq(#pos(@x),#0) | → | #false | (44) |
#eq(#pos(@x),#neg(@y)) | → | #false | (45) |
#eq(#pos(@x),#pos(@y)) | → | #eq(@x,@y) | (46) |
#eq(#s(@x),#0) | → | #false | (47) |
#eq(#s(@x),#s(@y)) | → | #eq(@x,@y) | (48) |
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) | → | #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) | (49) |
#eq(::(@x_1,@x_2),nil) | → | #false | (50) |
#eq(nil,::(@y_1,@y_2)) | → | #false | (51) |
#eq(nil,nil) | → | #true | (52) |
#or(#false,#false) | → | #false | (53) |
#or(#false,#true) | → | #true | (54) |
#or(#true,#false) | → | #true | (55) |
#or(#true,#true) | → | #true | (56) |
|
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 |
|
||||||||
|
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 |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
#and#(#false,#false) |
#and#(#false,#true) |
#and#(#true,#false) |
#and#(#true,#true) |
#cklt#(#EQ) |
#cklt#(#GT) |
#cklt#(#LT) |
#compare#(#0,#0) |
#compare#(#0,#neg(z0)) |
#compare#(#0,#pos(z0)) |
#compare#(#0,#s(z0)) |
#compare#(#neg(z0),#0) |
#compare#(#neg(z0),#neg(z1)) |
#compare#(#neg(z0),#pos(z1)) |
#compare#(#pos(z0),#0) |
#compare#(#pos(z0),#neg(z1)) |
#compare#(#pos(z0),#pos(z1)) |
#compare#(#s(z0),#0) |
#compare#(#s(z0),#s(z1)) |
#eq#(#0,#0) |
#eq#(#0,#neg(z0)) |
#eq#(#0,#pos(z0)) |
#eq#(#0,#s(z0)) |
#eq#(#neg(z0),#0) |
#eq#(#neg(z0),#neg(z1)) |
#eq#(#neg(z0),#pos(z1)) |
#eq#(#pos(z0),#0) |
#eq#(#pos(z0),#neg(z1)) |
#eq#(#pos(z0),#pos(z1)) |
#eq#(#s(z0),#0) |
#eq#(#s(z0),#s(z1)) |
#eq#(::(z0,z1),::(z2,z3)) |
#eq#(::(z0,z1),nil) |
#eq#(nil,::(z0,z1)) |
#eq#(nil,nil) |
#or#(#false,#false) |
#or#(#false,#true) |
#or#(#true,#false) |
#or#(#true,#true) |
#equal#(z0,z1) |
#less#(z0,z1) |
and#(z0,z1) |
insert#(z0,z1) |
insert#1#(::(z0,z1),z2) |
insert#1#(nil,z0) |
insert#2#(#false,z0,z1,z2) |
insert#2#(#true,z0,z1,z2) |
isortlist#(z0) |
isortlist#1#(::(z0,z1)) |
isortlist#1#(nil) |
leq#(z0,z1) |
leq#1#(::(z0,z1),z2) |
leq#1#(nil,z0) |
leq#2#(::(z0,z1),z2,z3) |
leq#2#(nil,z0,z1) |
or#(z0,z1) |
isortlist#1#(nil) | → | c49 | (77) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#less(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[and(x1, x2)] | = | 1 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 + 1 · x1 |
[isortlist#1(x1)] | = | 1 + 1 · x1 |
[leq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[or(x1, x2)] | = | 1 + 1 · x1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 1 + 1 · x1 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 0 |
[insert#1#(x1, x2)] | = | 0 |
[insert#2#(x1,...,x4)] | = | 0 |
[isortlist#(x1)] | = | 1 |
[isortlist#1#(x1)] | = | 1 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 0 |
[nil] | = | 1 |
[#0] | = | 1 |
[#neg(x1)] | = | 1 + 1 · x1 |
[#pos(x1)] | = | 1 + 1 · x1 |
[#s(x1)] | = | 1 + 1 · x1 |
[#EQ] | = | 1 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#less(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[and(x1, x2)] | = | 1 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 + 1 · x1 |
[isortlist#1(x1)] | = | 1 |
[leq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[or(x1, x2)] | = | 1 + 1 · x1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 1 + 1 · x2 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 0 |
[insert#1#(x1, x2)] | = | 0 |
[insert#2#(x1,...,x4)] | = | 0 |
[isortlist#(x1)] | = | 1 · x1 + 0 |
[isortlist#1#(x1)] | = | 1 · x1 + 0 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 1 |
[#neg(x1)] | = | 1 + 1 · x1 |
[#pos(x1)] | = | 1 + 1 · x1 |
[#s(x1)] | = | 1 + 1 · x1 |
[#EQ] | = | 1 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#less(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[and(x1, x2)] | = | 1 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 + 1 · x1 |
[isortlist#1(x1)] | = | 1 + 1 · x1 |
[leq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[or(x1, x2)] | = | 1 + 1 · x1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 1 + 1 · x1 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 0 |
[insert#1#(x1, x2)] | = | 0 |
[insert#2#(x1,...,x4)] | = | 0 |
[isortlist#(x1)] | = | 1 + 1 · x1 |
[isortlist#1#(x1)] | = | 1 · x1 + 0 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x2 |
[nil] | = | 1 |
[#0] | = | 1 |
[#neg(x1)] | = | 1 + 1 · x1 |
[#pos(x1)] | = | 1 + 1 · x1 |
[#s(x1)] | = | 1 + 1 · x1 |
[#EQ] | = | 1 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#less(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[and(x1, x2)] | = | 1 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 + 1 · x1 |
[isortlist#1(x1)] | = | 1 |
[leq(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[or(x1, x2)] | = | 1 + 1 · x1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 1 + 1 · x2 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 1 + 1 · x1 |
[insert#1#(x1, x2)] | = | 1 + 1 · x2 |
[insert#2#(x1,...,x4)] | = | 1 + 1 · x2 |
[isortlist#(x1)] | = | 1 + 1 · x1 |
[isortlist#1#(x1)] | = | 1 + 1 · x1 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
[#0] | = | 1 |
[#neg(x1)] | = | 1 + 1 · x1 |
[#pos(x1)] | = | 1 + 1 · x1 |
[#s(x1)] | = | 1 + 1 · x1 |
[#EQ] | = | 1 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[insert#1#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[insert#2#(x1,...,x4)] | = | 2 · x2 · x4 + 0 |
[isortlist#(x1)] | = | 1 · x1 · x1 + 0 |
[isortlist#1#(x1)] | = | 1 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 2 · x1 + 0 |
[leq#1#(x1, x2)] | = | 2 · x1 + 0 |
[leq#2#(x1, x2, x3)] | = | 2 · x3 + 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 2 · x2 + 0 |
[insert#1#(x1, x2)] | = | 2 · x1 + 0 |
[insert#2#(x1,...,x4)] | = | 2 · x4 + 0 |
[isortlist#(x1)] | = | 1 · x1 · x1 + 0 |
[isortlist#1#(x1)] | = | 1 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 1 · x2 + 0 |
[insert#1#(x1, x2)] | = | 1 · x1 + 0 |
[insert#2#(x1,...,x4)] | = | 1 · x4 + 0 |
[isortlist#(x1)] | = | 1 · x1 · x1 + 0 |
[isortlist#1#(x1)] | = | 1 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 1 · x2 + 0 |
[leq#1#(x1, x2)] | = | 1 · x2 + 0 |
[leq#2#(x1, x2, x3)] | = | 1 · x1 + 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 1 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[insert#1#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[insert#2#(x1,...,x4)] | = | 2 · x2 · x4 + 0 |
[isortlist#(x1)] | = | 2 + 1 · x1 · x1 |
[isortlist#1#(x1)] | = | 1 + 1 · x1 · x1 |
[leq#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[leq#1#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[leq#2#(x1, x2, x3)] | = | 2 · x1 + 0 + 2 · x1 · x3 |
[or#(x1, x2)] | = | 1 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
leq#1#(nil,z0) | → | c52 | (83) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 2 · x1 + 0 |
[isortlist#1(x1)] | = | 2 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 2 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 1 · x1 · x2 + 0 |
[insert#1#(x1, x2)] | = | 1 · x1 · x2 + 0 |
[insert#2#(x1,...,x4)] | = | 1 · x2 · x4 + 0 |
[isortlist#(x1)] | = | 1 · x1 · x1 + 0 |
[isortlist#1#(x1)] | = | 1 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 1 · x1 + 0 |
[leq#1#(x1, x2)] | = | 1 · x1 + 0 |
[leq#2#(x1, x2, x3)] | = | 1 · x3 + 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 2 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 2 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 1 + 1 · x2 |
[insert#1#(x1, x2)] | = | 1 · x1 + 0 |
[insert#2#(x1,...,x4)] | = | 1 + 1 · x4 |
[isortlist#(x1)] | = | 1 · x1 · x1 + 0 |
[isortlist#1#(x1)] | = | 1 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 2 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 2 |
[#less#(x1, x2)] | = | 1 |
[and#(x1, x2)] | = | 1 |
[insert#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[insert#1#(x1, x2)] | = | 2 · x1 · x2 + 0 |
[insert#2#(x1,...,x4)] | = | 2 · x2 · x4 + 0 |
[isortlist#(x1)] | = | 2 · x1 + 0 + 1 · x1 · x1 |
[isortlist#1#(x1)] | = | 1 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 2 · x1 + 0 + 2 · x1 · x2 |
[leq#1#(x1, x2)] | = | 2 · x1 + 0 + 2 · x1 · x2 |
[leq#2#(x1, x2, x3)] | = | 2 + 2 · x1 + 2 · x1 · x3 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 0 |
[leq#1(x1, x2)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[leq#2(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 2 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 1 · x2 + 0 |
[insert#1#(x1, x2)] | = | 1 · x1 + 0 |
[insert#2#(x1,...,x4)] | = | 1 + 1 · x4 |
[isortlist#(x1)] | = | 2 · x1 + 0 + 1 · x1 · x1 |
[isortlist#1#(x1)] | = | 2 · x1 + 0 + 1 · x1 · x1 |
[leq#(x1, x2)] | = | 0 |
[leq#1#(x1, x2)] | = | 0 |
[leq#2#(x1, x2, x3)] | = | 0 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 0 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 0 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
isortlist#1(nil) | → | nil | (11) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
[c] | = | 0 |
[c1] | = | 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] | = | 0 |
[c14] | = | 0 |
[c15] | = | 0 |
[c16(x1)] | = | 1 · x1 + 0 |
[c17] | = | 0 |
[c18(x1)] | = | 1 · x1 + 0 |
[c19] | = | 0 |
[c20] | = | 0 |
[c21] | = | 0 |
[c22] | = | 0 |
[c23] | = | 0 |
[c24(x1)] | = | 1 · x1 + 0 |
[c25] | = | 0 |
[c26] | = | 0 |
[c27] | = | 0 |
[c28(x1)] | = | 1 · x1 + 0 |
[c29] | = | 0 |
[c30(x1)] | = | 1 · x1 + 0 |
[c31(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 |
[c32] | = | 0 |
[c33] | = | 0 |
[c34] | = | 0 |
[c35] | = | 0 |
[c36] | = | 0 |
[c37] | = | 0 |
[c38] | = | 0 |
[c39(x1)] | = | 1 · x1 + 0 |
[c40(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c41(x1)] | = | 1 · x1 + 0 |
[c42(x1)] | = | 1 · x1 + 0 |
[c43(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c44] | = | 0 |
[c45(x1)] | = | 1 · x1 + 0 |
[c46] | = | 0 |
[c47(x1)] | = | 1 · x1 + 0 |
[c48(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c49] | = | 0 |
[c50(x1)] | = | 1 · x1 + 0 |
[c51(x1)] | = | 1 · x1 + 0 |
[c52] | = | 0 |
[c53(x1,...,x5)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5 |
[c54] | = | 0 |
[c55(x1)] | = | 1 · x1 + 0 |
[#equal(x1, x2)] | = | 0 |
[#less(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#1(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert#2(x1,...,x4)] | = | 2 + 1 · x2 + 1 · x3 + 1 · x4 |
[isortlist(x1)] | = | 1 · x1 + 0 |
[isortlist#1(x1)] | = | 1 · x1 + 0 |
[leq(x1, x2)] | = | 1 · x1 · x2 + 0 |
[leq#1(x1, x2)] | = | 1 · x1 · x2 + 0 |
[leq#2(x1, x2, x3)] | = | 1 · x1 + 0 |
[or(x1, x2)] | = | 1 |
[#and(x1, x2)] | = | 1 |
[#cklt(x1)] | = | 1 |
[#compare(x1, x2)] | = | 0 |
[#eq(x1, x2)] | = | 0 |
[#or(x1, x2)] | = | 1 |
[#and#(x1, x2)] | = | 0 |
[#cklt#(x1)] | = | 0 |
[#compare#(x1, x2)] | = | 0 |
[#eq#(x1, x2)] | = | 0 |
[#or#(x1, x2)] | = | 0 |
[#equal#(x1, x2)] | = | 0 |
[#less#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 1 + 1 · x1 · x2 |
[insert#1#(x1, x2)] | = | 1 + 1 · x1 · x2 |
[insert#2#(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 · x4 |
[isortlist#(x1)] | = | 2 · x1 · x1 + 0 |
[isortlist#1#(x1)] | = | 2 · x1 · x1 + 0 |
[leq#(x1, x2)] | = | 1 + 1 · x1 |
[leq#1#(x1, x2)] | = | 1 · x1 + 0 |
[leq#2#(x1, x2, x3)] | = | 1 + 1 · x3 |
[or#(x1, x2)] | = | 0 |
[#false] | = | 1 |
[#true] | = | 0 |
[::(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
[#0] | = | 0 |
[#neg(x1)] | = | 0 |
[#pos(x1)] | = | 0 |
[#s(x1)] | = | 0 |
[#EQ] | = | 2 |
[#GT] | = | 1 |
[#LT] | = | 1 |
#and#(#false,#false) | → | c | (90) |
#and#(#false,#true) | → | c1 | (91) |
#and#(#true,#false) | → | c2 | (92) |
#and#(#true,#true) | → | c3 | (93) |
#cklt#(#EQ) | → | c4 | (94) |
#cklt#(#GT) | → | c5 | (95) |
#cklt#(#LT) | → | c6 | (96) |
#compare#(#0,#0) | → | c7 | (97) |
#compare#(#0,#neg(z0)) | → | c8 | (99) |
#compare#(#0,#pos(z0)) | → | c9 | (101) |
#compare#(#0,#s(z0)) | → | c10 | (103) |
#compare#(#neg(z0),#0) | → | c11 | (105) |
#compare#(#neg(z0),#neg(z1)) | → | c12(#compare#(z1,z0)) | (107) |
#compare#(#neg(z0),#pos(z1)) | → | c13 | (109) |
#compare#(#pos(z0),#0) | → | c14 | (111) |
#compare#(#pos(z0),#neg(z1)) | → | c15 | (113) |
#compare#(#pos(z0),#pos(z1)) | → | c16(#compare#(z0,z1)) | (115) |
#compare#(#s(z0),#0) | → | c17 | (117) |
#compare#(#s(z0),#s(z1)) | → | c18(#compare#(z0,z1)) | (119) |
#eq#(#0,#0) | → | c19 | (120) |
#eq#(#0,#neg(z0)) | → | c20 | (122) |
#eq#(#0,#pos(z0)) | → | c21 | (124) |
#eq#(#0,#s(z0)) | → | c22 | (126) |
#eq#(#neg(z0),#0) | → | c23 | (128) |
#eq#(#neg(z0),#neg(z1)) | → | c24(#eq#(z0,z1)) | (130) |
#eq#(#neg(z0),#pos(z1)) | → | c25 | (132) |
#eq#(#pos(z0),#0) | → | c26 | (134) |
#eq#(#pos(z0),#neg(z1)) | → | c27 | (136) |
#eq#(#pos(z0),#pos(z1)) | → | c28(#eq#(z0,z1)) | (138) |
#eq#(#s(z0),#0) | → | c29 | (140) |
#eq#(#s(z0),#s(z1)) | → | c30(#eq#(z0,z1)) | (142) |
#eq#(::(z0,z1),::(z2,z3)) | → | c31(#and#(#eq(z0,z2),#eq(z1,z3)),#eq#(z0,z2),#eq#(z1,z3)) | (144) |
#eq#(::(z0,z1),nil) | → | c32 | (146) |
#eq#(nil,::(z0,z1)) | → | c33 | (148) |
#eq#(nil,nil) | → | c34 | (149) |
#or#(#false,#false) | → | c35 | (150) |
#or#(#false,#true) | → | c36 | (151) |
#or#(#true,#false) | → | c37 | (152) |
#or#(#true,#true) | → | c38 | (153) |
#equal#(z0,z1) | → | c39(#eq#(z0,z1)) | (58) |
#less#(z0,z1) | → | c40(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) | (60) |
and#(z0,z1) | → | c41(#and#(z0,z1)) | (62) |
insert#(z0,z1) | → | c42(insert#1#(z1,z0)) | (64) |
insert#1#(::(z0,z1),z2) | → | c43(insert#2#(leq(z2,z0),z2,z0,z1),leq#(z2,z0)) | (66) |
insert#1#(nil,z0) | → | c44 | (68) |
insert#2#(#false,z0,z1,z2) | → | c45(insert#(z0,z2)) | (70) |
insert#2#(#true,z0,z1,z2) | → | c46 | (72) |
isortlist#(z0) | → | c47(isortlist#1#(z0)) | (74) |
isortlist#1#(::(z0,z1)) | → | c48(insert#(z0,isortlist(z1)),isortlist#(z1)) | (76) |
isortlist#1#(nil) | → | c49 | (77) |
leq#(z0,z1) | → | c50(leq#1#(z0,z1)) | (79) |
leq#1#(::(z0,z1),z2) | → | c51(leq#2#(z2,z0,z1)) | (81) |
leq#1#(nil,z0) | → | c52 | (83) |
leq#2#(::(z0,z1),z2,z3) | → | c53(or#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less#(z2,z0),and#(#equal(z2,z0),leq(z3,z1)),#equal#(z2,z0),leq#(z3,z1)) | (85) |
leq#2#(nil,z0,z1) | → | c54 | (87) |
or#(z0,z1) | → | c55(#or#(z0,z1)) | (89) |
#or(#false,#true) | → | #true | (54) |
#or(#true,#false) | → | #true | (55) |
#or(#true,#true) | → | #true | (56) |
leq#1(nil,z0) | → | #true | (82) |
#or(#false,#false) | → | #false | (53) |
isortlist#1(nil) | → | nil | (11) |
leq(z0,z1) | → | leq#1(z0,z1) | (78) |
insert#2(#true,z0,z1,z2) | → | ::(z0,::(z1,z2)) | (71) |
or(z0,z1) | → | #or(z0,z1) | (88) |
leq#1(::(z0,z1),z2) | → | leq#2(z2,z0,z1) | (80) |
isortlist#1(::(z0,z1)) | → | insert(z0,isortlist(z1)) | (75) |
insert#1(::(z0,z1),z2) | → | insert#2(leq(z2,z0),z2,z0,z1) | (65) |
leq#2(nil,z0,z1) | → | #false | (86) |
insert#2(#false,z0,z1,z2) | → | ::(z1,insert(z0,z2)) | (69) |
leq#2(::(z0,z1),z2,z3) | → | or(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))) | (84) |
insert(z0,z1) | → | insert#1(z1,z0) | (63) |
isortlist(z0) | → | isortlist#1(z0) | (73) |
insert#1(nil,z0) | → | ::(z0,nil) | (67) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).