The rewrite relation of the following TRS is considered.
There are 133 ruless (increase limit for explicit display).
There are 207 ruless (increase limit for explicit display).
The dependency pairs are split into 23 components.
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (199) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (139) |
mark#(cons(X1,X2)) | → | mark#(X1) | (201) |
mark#(zeros) | → | active#(zeros) | (198) |
active#(zeros) | → | mark#(cons(0,zeros)) | (134) |
mark#(U11(X)) | → | active#(U11(mark(X))) | (203) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (143) |
mark#(U11(X)) | → | mark#(X) | (205) |
mark#(U21(X)) | → | active#(U21(mark(X))) | (207) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (147) |
mark#(U21(X)) | → | mark#(X) | (209) |
mark#(U31(X)) | → | active#(U31(mark(X))) | (210) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (151) |
mark#(U31(X)) | → | mark#(X) | (212) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (213) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (154) |
mark#(U41(X1,X2)) | → | mark#(X1) | (215) |
mark#(U42(X)) | → | active#(U42(mark(X))) | (216) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (158) |
mark#(U42(X)) | → | mark#(X) | (218) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (219) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (161) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (220) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (164) |
mark#(U51(X1,X2)) | → | mark#(X1) | (222) |
mark#(U52(X)) | → | active#(U52(mark(X))) | (223) |
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (168) |
mark#(U52(X)) | → | mark#(X) | (225) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (226) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (171) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (227) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (174) |
mark#(U61(X1,X2)) | → | mark#(X1) | (229) |
mark#(U62(X)) | → | active#(U62(mark(X))) | (230) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (178) |
mark#(U62(X)) | → | mark#(X) | (232) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (233) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (182) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (235) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (236) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (185) |
mark#(U72(X1,X2)) | → | mark#(X1) | (238) |
mark#(isNat(X)) | → | active#(isNat(X)) | (239) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (189) |
mark#(s(X)) | → | active#(s(mark(X))) | (240) |
active#(take(0,IL)) | → | mark#(U81(isNatIList(IL))) | (192) |
mark#(s(X)) | → | mark#(X) | (242) |
mark#(length(X)) | → | active#(length(mark(X))) | (243) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (195) |
mark#(length(X)) | → | mark#(X) | (245) |
mark#(U81(X)) | → | active#(U81(mark(X))) | (246) |
mark#(U81(X)) | → | mark#(X) | (248) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (250) |
mark#(U91(X1,X2,X3,X4)) | → | mark#(X1) | (252) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (253) |
mark#(U92(X1,X2,X3,X4)) | → | mark#(X1) | (255) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (256) |
mark#(U93(X1,X2,X3,X4)) | → | mark#(X1) | (258) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (259) |
mark#(take(X1,X2)) | → | mark#(X1) | (261) |
mark#(take(X1,X2)) | → | mark#(X2) | (262) |
[active#(x1)] | = | -1 + x1 |
[U11(x1)] | = | 0 |
[U21(x1)] | = | -2 |
[U31(x1)] | = | -2 |
[U41(x1, x2)] | = | 2 |
[U42(x1)] | = | -2 |
[U51(x1, x2)] | = | 2 |
[U52(x1)] | = | 0 |
[U61(x1, x2)] | = | 2 |
[U62(x1)] | = | -2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[U81(x1)] | = | -2 |
[U91(x1,...,x4)] | = | 2 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | 2 |
[cons(x1, x2)] | = | -2 |
[length(x1)] | = | 2 |
[s(x1)] | = | 0 |
[take(x1, x2)] | = | 2 |
[mark(x1)] | = | -2 |
[active(x1)] | = | 2 · x1 |
[zeros] | = | 2 |
[0] | = | 1 |
[tt] | = | 1 |
[isNatIList(x1)] | = | 2 |
[isNatList(x1)] | = | 2 |
[isNat(x1)] | = | 2 |
[nil] | = | 1 |
[mark#(x1)] | = | 1 |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
U11(active(X)) | → | U11(X) | (61) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
U62(active(X)) | → | U62(X) | (87) |
U62(mark(X)) | → | U62(X) | (86) |
U31(active(X)) | → | U31(X) | (65) |
U31(mark(X)) | → | U31(X) | (64) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U81(active(X)) | → | U81(X) | (105) |
U81(mark(X)) | → | U81(X) | (104) |
U91(X1,mark(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (107) |
U91(mark(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (106) |
U91(X1,X2,mark(X3),X4) | → | U91(X1,X2,X3,X4) | (108) |
U91(X1,X2,X3,mark(X4)) | → | U91(X1,X2,X3,X4) | (109) |
U91(active(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (110) |
U91(X1,active(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (111) |
U91(X1,X2,active(X3),X4) | → | U91(X1,X2,X3,X4) | (112) |
U91(X1,X2,X3,active(X4)) | → | U91(X1,X2,X3,X4) | (113) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (199) |
mark#(U11(X)) | → | active#(U11(mark(X))) | (203) |
mark#(U21(X)) | → | active#(U21(mark(X))) | (207) |
mark#(U31(X)) | → | active#(U31(mark(X))) | (210) |
mark#(U42(X)) | → | active#(U42(mark(X))) | (216) |
mark#(U52(X)) | → | active#(U52(mark(X))) | (223) |
mark#(U62(X)) | → | active#(U62(mark(X))) | (230) |
mark#(s(X)) | → | active#(s(mark(X))) | (240) |
mark#(U81(X)) | → | active#(U81(mark(X))) | (246) |
[active#(x1)] | = | 1 · x1 |
[U41(x1, x2)] | = | 1 · x1 |
[tt] | = | 0 |
[mark#(x1)] | = | 1 · x1 |
[U42(x1)] | = | 1 · x1 |
[isNatIList(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 · x1 + 1 · x2 |
[zeros] | = | 0 |
[0] | = | 0 |
[U51(x1, x2)] | = | 1 · x1 |
[U52(x1)] | = | 1 · x1 |
[isNatList(x1)] | = | 0 |
[U11(x1)] | = | 1 · x1 |
[U61(x1, x2)] | = | 1 · x1 |
[U62(x1)] | = | 1 · x1 |
[U21(x1)] | = | 1 · x1 |
[U71(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 |
[U72(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[isNat(x1)] | = | 0 |
[U31(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[s(x1)] | = | 1 · x1 |
[length(x1)] | = | 1 + 1 · x1 |
[U91(x1,...,x4)] | = | 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 |
[U92(x1,...,x4)] | = | 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 |
[U93(x1,...,x4)] | = | 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 |
[take(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U81(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[nil] | = | 0 |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (235) |
mark#(U72(X1,X2)) | → | mark#(X1) | (238) |
mark#(length(X)) | → | mark#(X) | (245) |
[active#(x1)] | = | 2 · x1 |
[mark#(x1)] | = | 2 · x1 |
[U42(x1)] | = | 2 · x1 |
[U62(x1)] | = | 2 · x1 |
[U81(x1)] | = | x1 |
[U91(x1,...,x4)] | = | 2 + 2 · x1 + x3 + 2 · x4 |
[isNatIList(x1)] | = | 0 |
[active(x1)] | = | x1 |
[mark(x1)] | = | x1 |
[U41(x1, x2)] | = | x1 |
[U51(x1, x2)] | = | 2 · x1 |
[U61(x1, x2)] | = | 2 · x1 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[U92(x1,...,x4)] | = | 2 + 2 · x1 + 2 · x4 |
[U93(x1,...,x4)] | = | 2 + x1 + 2 · x4 |
[length(x1)] | = | 2 |
[take(x1, x2)] | = | 1 + 2 · x1 + x2 |
[U11(x1)] | = | x1 |
[U31(x1)] | = | 2 · x1 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 2 · x1 |
[isNat(x1)] | = | 0 |
[cons(x1, x2)] | = | 2 + 2 · x1 |
[zeros] | = | 2 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[nil] | = | 0 |
mark#(cons(X1,X2)) | → | mark#(X1) | (201) |
active#(take(0,IL)) | → | mark#(U81(isNatIList(IL))) | (192) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (195) |
mark#(U91(X1,X2,X3,X4)) | → | mark#(X1) | (252) |
mark#(U92(X1,X2,X3,X4)) | → | mark#(X1) | (255) |
mark#(U93(X1,X2,X3,X4)) | → | mark#(X1) | (258) |
mark#(take(X1,X2)) | → | mark#(X1) | (261) |
mark#(take(X1,X2)) | → | mark#(X2) | (262) |
The dependency pairs are split into 1 component.
mark#(U11(X)) | → | mark#(X) | (205) |
mark#(U21(X)) | → | mark#(X) | (209) |
mark#(U31(X)) | → | mark#(X) | (212) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (213) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (139) |
mark#(U41(X1,X2)) | → | mark#(X1) | (215) |
mark#(U42(X)) | → | mark#(X) | (218) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (219) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (143) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (220) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (147) |
mark#(U51(X1,X2)) | → | mark#(X1) | (222) |
mark#(U52(X)) | → | mark#(X) | (225) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (226) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (151) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (227) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (154) |
mark#(U61(X1,X2)) | → | mark#(X1) | (229) |
mark#(U62(X)) | → | mark#(X) | (232) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (233) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (158) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (236) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (161) |
mark#(isNat(X)) | → | active#(isNat(X)) | (239) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (164) |
mark#(s(X)) | → | mark#(X) | (242) |
mark#(length(X)) | → | active#(length(mark(X))) | (243) |
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (168) |
mark#(U81(X)) | → | mark#(X) | (248) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (250) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (171) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (253) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (174) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (256) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (178) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (259) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (182) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (185) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (189) |
[active#(x1)] | = | -2 |
[U41(x1, x2)] | = | 1 + 2 · x1 |
[U51(x1, x2)] | = | 1 + x1 |
[U61(x1, x2)] | = | 1 + 2 · x1 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[U91(x1,...,x4)] | = | 2 + x1 + x2 + 2 · x3 + 2 · x4 |
[U92(x1,...,x4)] | = | -2 |
[U93(x1,...,x4)] | = | 0 |
[length(x1)] | = | 0 |
[take(x1, x2)] | = | 0 |
[mark(x1)] | = | 1 + x1 |
[cons(x1, x2)] | = | 0 |
[active(x1)] | = | 1 + 2 · x1 |
[zeros] | = | 1 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 1 + 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 1 + x1 |
[U52(x1)] | = | 1 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 1 + x1 |
[U62(x1)] | = | 1 + 2 · x1 |
[U31(x1)] | = | 1 + x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + 2 · x1 |
[U81(x1)] | = | 2 + x1 |
[nil] | = | 1 |
[mark#(x1)] | = | -1 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U62(active(X)) | → | U62(X) | (87) |
U62(mark(X)) | → | U62(X) | (86) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U11(active(X)) | → | U11(X) | (61) |
U11(mark(X)) | → | U11(X) | (60) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
U31(active(X)) | → | U31(X) | (65) |
U31(mark(X)) | → | U31(X) | (64) |
mark#(U81(X)) | → | mark#(X) | (248) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (250) |
[active#(x1)] | = | -2 + x1 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | 2 |
[U61(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | 2 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | 2 |
[length(x1)] | = | 2 |
[take(x1, x2)] | = | -2 |
[mark(x1)] | = | -2 + x1 |
[cons(x1, x2)] | = | -2 + 2 · x2 |
[active(x1)] | = | 1 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 2 |
[U42(x1)] | = | -2 + x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | -1 + x1 |
[U52(x1)] | = | -2 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | -1 + x1 |
[U62(x1)] | = | -2 + x1 |
[U31(x1)] | = | -2 + x1 |
[isNat(x1)] | = | 2 |
[s(x1)] | = | -2 + x1 |
[U91(x1,...,x4)] | = | 2 · x1 + 2 · x2 + 2 · x3 + x4 |
[U81(x1)] | = | -2 + x1 |
[nil] | = | 0 |
[mark#(x1)] | = | -2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (158) |
[active#(x1)] | = | -2 + 2 · x1 |
[U41(x1, x2)] | = | 2 |
[U51(x1, x2)] | = | 2 |
[U61(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | 2 |
[length(x1)] | = | 2 |
[take(x1, x2)] | = | 0 |
[mark(x1)] | = | -2 |
[cons(x1, x2)] | = | 2 |
[active(x1)] | = | -2 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | -2 |
[isNatIList(x1)] | = | 2 |
[U11(x1)] | = | -2 + 2 · x1 |
[U52(x1)] | = | -2 + x1 |
[isNatList(x1)] | = | 2 |
[U21(x1)] | = | -2 + x1 |
[U62(x1)] | = | -2 |
[U31(x1)] | = | -2 + x1 |
[isNat(x1)] | = | 2 |
[s(x1)] | = | 0 |
[U91(x1,...,x4)] | = | -2 + x1 + x3 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (259) |
[active#(x1)] | = | 2 |
[U41(x1, x2)] | = | 2 · x1 |
[U51(x1, x2)] | = | 2 · x1 |
[U61(x1, x2)] | = | x1 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[U92(x1,...,x4)] | = | 1 |
[U93(x1,...,x4)] | = | -2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 · x1 |
[cons(x1, x2)] | = | x2 |
[active(x1)] | = | 2 + x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 1 |
[U42(x1)] | = | 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | x1 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | x1 |
[U62(x1)] | = | 2 · x1 |
[U31(x1)] | = | x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 2 · x1 |
[U91(x1,...,x4)] | = | x3 + x4 |
[take(x1, x2)] | = | -2 |
[U81(x1)] | = | 1 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U62(active(X)) | → | U62(X) | (87) |
U62(mark(X)) | → | U62(X) | (86) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U11(active(X)) | → | U11(X) | (61) |
U11(mark(X)) | → | U11(X) | (60) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
U31(active(X)) | → | U31(X) | (65) |
U31(mark(X)) | → | U31(X) | (64) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (253) |
[active#(x1)] | = | -2 + 2 · x1 |
[U41(x1, x2)] | = | 2 |
[U51(x1, x2)] | = | 2 |
[U61(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[U93(x1,...,x4)] | = | 2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | 2 |
[cons(x1, x2)] | = | -2 + x1 |
[active(x1)] | = | -2 |
[zeros] | = | 0 |
[0] | = | 2 |
[tt] | = | 2 |
[U42(x1)] | = | -2 + x1 |
[isNatIList(x1)] | = | 2 |
[U11(x1)] | = | -2 + 2 · x1 |
[U52(x1)] | = | -2 |
[isNatList(x1)] | = | 2 |
[U21(x1)] | = | 2 |
[U62(x1)] | = | -2 |
[U31(x1)] | = | -2 |
[isNat(x1)] | = | 2 |
[s(x1)] | = | 2 |
[U91(x1,...,x4)] | = | -2 + 2 · x2 + 2 · x4 |
[U92(x1,...,x4)] | = | 2 + 2 · x1 + 2 · x2 + x3 + x4 |
[take(x1, x2)] | = | -2 + x1 |
[U81(x1)] | = | 2 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (161) |
[active#(x1)] | = | -2 |
[U41(x1, x2)] | = | 1 + x1 |
[U51(x1, x2)] | = | 1 + x1 |
[U61(x1, x2)] | = | 1 + x1 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[U93(x1,...,x4)] | = | 2 + x2 + 2 · x3 + 2 · x4 |
[length(x1)] | = | 0 |
[mark(x1)] | = | 2 + x1 |
[cons(x1, x2)] | = | -2 |
[active(x1)] | = | 2 + 2 · x1 |
[zeros] | = | 2 |
[0] | = | 2 |
[tt] | = | 2 |
[U42(x1)] | = | 1 + 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 1 + 2 · x1 |
[U52(x1)] | = | 1 + x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 1 + x1 |
[U62(x1)] | = | 1 + x1 |
[U31(x1)] | = | 1 + x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + x1 |
[U91(x1,...,x4)] | = | 2 + 2 · x2 + x4 |
[U92(x1,...,x4)] | = | -2 |
[take(x1, x2)] | = | -2 + x1 |
[U81(x1)] | = | 2 + 2 · x1 |
[nil] | = | 2 |
[mark#(x1)] | = | -1 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U62(active(X)) | → | U62(X) | (87) |
U62(mark(X)) | → | U62(X) | (86) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U11(active(X)) | → | U11(X) | (61) |
U11(mark(X)) | → | U11(X) | (60) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
U31(active(X)) | → | U31(X) | (65) |
U31(mark(X)) | → | U31(X) | (64) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (256) |
[active#(x1)] | = | x1 |
[U41(x1, x2)] | = | 2 |
[U51(x1, x2)] | = | 2 |
[U61(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | 2 + 2 · x1 |
[cons(x1, x2)] | = | -2 + x1 |
[active(x1)] | = | -2 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 2 |
[U42(x1)] | = | 2 |
[isNatIList(x1)] | = | 2 |
[U11(x1)] | = | -2 |
[U52(x1)] | = | -2 |
[isNatList(x1)] | = | 2 |
[U21(x1)] | = | -2 |
[U62(x1)] | = | -1 + x1 |
[U31(x1)] | = | 2 |
[isNat(x1)] | = | 2 |
[s(x1)] | = | -2 + x1 |
[U91(x1,...,x4)] | = | -2 + 2 · x4 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | -1 + 2 · x1 |
[take(x1, x2)] | = | -2 + x1 + x2 |
[U81(x1)] | = | 1 + x1 |
[nil] | = | 2 |
[mark#(x1)] | = | 2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (164) |
[active#(x1)] | = | x1 |
[U41(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U51(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U61(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[U71(x1, x2, x3)] | = | x2 + 2 · x3 |
[U72(x1, x2)] | = | x2 |
[length(x1)] | = | x1 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x1 + x2 |
[active(x1)] | = | x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | x1 |
[isNatIList(x1)] | = | 1 + 2 · x1 |
[U11(x1)] | = | x1 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 2 · x1 |
[U21(x1)] | = | x1 |
[U62(x1)] | = | x1 |
[U31(x1)] | = | x1 |
[isNat(x1)] | = | 2 · x1 |
[s(x1)] | = | x1 |
[U91(x1,...,x4)] | = | 2 + x2 + 2 · x3 + 2 · x4 |
[U92(x1,...,x4)] | = | 2 + x2 + 2 · x3 + 2 · x4 |
[U93(x1,...,x4)] | = | 2 + x2 + 2 · x3 + 2 · x4 |
[take(x1, x2)] | = | 2 + 2 · x1 + x2 |
[U81(x1)] | = | 2 |
[nil] | = | 2 |
[mark#(x1)] | = | x1 |
mark#(U41(X1,X2)) | → | mark#(X1) | (215) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (147) |
mark#(U61(X1,X2)) | → | mark#(X1) | (229) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (174) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (185) |
[active#(x1)] | = | 0 |
[U41(x1, x2)] | = | 0 |
[U51(x1, x2)] | = | 1 + 2 · x1 |
[U61(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | 0 |
[length(x1)] | = | 0 |
[mark(x1)] | = | 2 · x1 |
[cons(x1, x2)] | = | 2 + x1 + 2 · x2 |
[active(x1)] | = | 2 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 1 + 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 1 + 2 · x1 |
[U52(x1)] | = | 1 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 1 + x1 |
[U62(x1)] | = | 2 + x1 |
[U31(x1)] | = | 2 + x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + 2 · x1 |
[U91(x1,...,x4)] | = | -2 + x1 + x2 + x4 |
[U92(x1,...,x4)] | = | 2 + x1 + 2 · x2 + 2 · x3 |
[U93(x1,...,x4)] | = | 2 + 2 · x2 + x3 |
[take(x1, x2)] | = | -2 + 2 · x1 + x2 |
[U81(x1)] | = | 2 + x1 |
[nil] | = | 0 |
[mark#(x1)] | = | -1 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U11(active(X)) | → | U11(X) | (61) |
U11(mark(X)) | → | U11(X) | (60) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
mark#(U31(X)) | → | mark#(X) | (212) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (227) |
mark#(U62(X)) | → | mark#(X) | (232) |
[active#(x1)] | = | x1 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U71(x1, x2, x3)] | = | 1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 1 + 2 · x2 |
[length(x1)] | = | 1 + 2 · x1 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x1 + x2 |
[active(x1)] | = | x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 2 + x1 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 2 · x1 |
[U21(x1)] | = | x1 |
[U61(x1, x2)] | = | 2 |
[U62(x1)] | = | 0 |
[U31(x1)] | = | -2 |
[isNat(x1)] | = | 2 · x1 |
[s(x1)] | = | x1 |
[U91(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U92(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U93(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[take(x1, x2)] | = | 2 + x2 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | x1 |
mark#(U11(X)) | → | mark#(X) | (205) |
[active#(x1)] | = | 2 + 2 · x1 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | 1 + 2 · x1 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | 0 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | -2 |
[active(x1)] | = | x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | -2 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 1 |
[U21(x1)] | = | x1 |
[U61(x1, x2)] | = | -2 |
[U62(x1)] | = | -2 |
[U31(x1)] | = | -2 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | x1 |
[U91(x1,...,x4)] | = | -2 |
[U92(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | -2 |
[take(x1, x2)] | = | -2 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 + 2 · x1 |
mark#(U51(X1,X2)) | → | mark#(X1) | (222) |
[active#(x1)] | = | -2 + 2 · x1 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 · x1 |
[cons(x1, x2)] | = | -2 + x1 |
[active(x1)] | = | 2 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 1 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 2 |
[U21(x1)] | = | x1 |
[U61(x1, x2)] | = | -2 + 2 · x1 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | -2 |
[isNat(x1)] | = | 2 |
[s(x1)] | = | x1 |
[U91(x1,...,x4)] | = | 2 + x2 + x3 |
[U92(x1,...,x4)] | = | -2 + 2 · x1 + 2 · x3 + x4 |
[U93(x1,...,x4)] | = | -2 + 2 · x2 |
[take(x1, x2)] | = | -2 + x1 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U11(active(X)) | → | U11(X) | (61) |
U11(mark(X)) | → | U11(X) | (60) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (168) |
[active#(x1)] | = | -2 + x1 |
[U41(x1, x2)] | = | 0 |
[U51(x1, x2)] | = | -2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 + x1 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[active(x1)] | = | 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 2 |
[U42(x1)] | = | 2 + x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | -2 + x1 |
[U52(x1)] | = | 2 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 2 + x1 |
[U61(x1, x2)] | = | 2 + x1 |
[U62(x1)] | = | 2 + 2 · x1 |
[U31(x1)] | = | 2 |
[isNat(x1)] | = | 2 + 2 · x1 |
[s(x1)] | = | 2 + 2 · x1 |
[U91(x1,...,x4)] | = | -2 + 2 · x3 |
[U92(x1,...,x4)] | = | -2 + 2 · x4 |
[U93(x1,...,x4)] | = | 2 |
[take(x1, x2)] | = | -2 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | -2 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U21(active(X)) | → | U21(X) | (63) |
U21(mark(X)) | → | U21(X) | (62) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (171) |
[active#(x1)] | = | -2 + 2 · x1 |
[U41(x1, x2)] | = | 2 |
[U51(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | 2 |
[cons(x1, x2)] | = | -2 + 2 · x2 |
[active(x1)] | = | -2 + x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 2 |
[U42(x1)] | = | -2 + 2 · x1 |
[isNatIList(x1)] | = | 2 |
[U11(x1)] | = | 0 |
[U52(x1)] | = | -2 |
[isNatList(x1)] | = | 2 |
[U21(x1)] | = | -2 |
[U61(x1, x2)] | = | 2 + x1 + x2 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | 1 + x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | -2 |
[U91(x1,...,x4)] | = | -2 + 2 · x1 + 2 · x4 |
[U92(x1,...,x4)] | = | 2 + 2 · x1 + x4 |
[U93(x1,...,x4)] | = | -2 + x2 + x3 + 2 · x4 |
[take(x1, x2)] | = | 2 |
[U81(x1)] | = | 1 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
isNat(active(X)) | → | isNat(X) | (99) |
isNat(mark(X)) | → | isNat(X) | (98) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(isNat(X)) | → | active#(isNat(X)) | (239) |
[active#(x1)] | = | -2 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | -2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | 0 |
[mark(x1)] | = | 2 + 2 · x1 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[active(x1)] | = | 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 1 + x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 0 |
[U52(x1)] | = | 1 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 2 + 2 · x1 |
[U61(x1, x2)] | = | -2 + x2 |
[U62(x1)] | = | 2 + x1 |
[U31(x1)] | = | 2 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + 2 · x1 |
[U91(x1,...,x4)] | = | 2 |
[U92(x1,...,x4)] | = | -2 + x2 + 2 · x3 |
[U93(x1,...,x4)] | = | 2 |
[take(x1, x2)] | = | -2 + x1 |
[U81(x1)] | = | 2 |
[nil] | = | 1 |
[mark#(x1)] | = | -1 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(U21(X)) | → | mark#(X) | (209) |
[active#(x1)] | = | 2 + x1 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | 2 · x2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | 0 |
[mark(x1)] | = | 2 + 2 · x1 |
[cons(x1, x2)] | = | 1 + x2 |
[active(x1)] | = | 2 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 2 + 2 · x1 |
[U52(x1)] | = | x1 |
[isNatList(x1)] | = | 2 · x1 |
[U21(x1)] | = | -2 |
[U61(x1, x2)] | = | -2 + 2 · x1 |
[U62(x1)] | = | -2 |
[U31(x1)] | = | -2 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | x1 |
[U91(x1,...,x4)] | = | -2 + 2 · x2 + 2 · x3 + 2 · x4 |
[U92(x1,...,x4)] | = | -2 + 2 · x2 |
[U93(x1,...,x4)] | = | 2 + x2 |
[take(x1, x2)] | = | -2 + 2 · x2 |
[U81(x1)] | = | 0 |
[nil] | = | 1 |
[mark#(x1)] | = | 2 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (182) |
[active#(x1)] | = | -2 + 2 · x1 |
[U41(x1, x2)] | = | 2 |
[U51(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | 2 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[active(x1)] | = | -2 + 2 · x1 |
[zeros] | = | 2 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | -2 |
[isNatIList(x1)] | = | 2 |
[U11(x1)] | = | 1 + x1 |
[U52(x1)] | = | -2 + x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 2 |
[U61(x1, x2)] | = | 2 + x2 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | 2 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 2 |
[U91(x1,...,x4)] | = | -1 + x3 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | 2 + 2 · x1 + x2 + 2 · x3 |
[take(x1, x2)] | = | -2 + 2 · x1 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (226) |
[active#(x1)] | = | -2 |
[U41(x1, x2)] | = | -2 |
[U51(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 0 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 + 2 · x1 |
[cons(x1, x2)] | = | -2 |
[active(x1)] | = | 2 + x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 2 |
[U42(x1)] | = | 1 + 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | -2 |
[U52(x1)] | = | 1 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | 2 |
[U61(x1, x2)] | = | -2 + 2 · x2 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | -2 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + x1 |
[U91(x1,...,x4)] | = | -2 + x2 + x3 |
[U92(x1,...,x4)] | = | 2 + x1 + x2 + x3 + x4 |
[U93(x1,...,x4)] | = | 2 + x1 + x3 + 2 · x4 |
[take(x1, x2)] | = | 0 |
[U81(x1)] | = | -2 |
[nil] | = | 2 |
[mark#(x1)] | = | -1 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
isNatList(active(X)) | → | isNatList(X) | (81) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U52(active(X)) | → | U52(X) | (79) |
U52(mark(X)) | → | U52(X) | (78) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (220) |
[active#(x1)] | = | -2 + x1 |
[U41(x1, x2)] | = | -2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | -2 + 2 · x1 |
[cons(x1, x2)] | = | -2 + 2 · x2 |
[active(x1)] | = | 2 |
[zeros] | = | 2 |
[0] | = | 0 |
[tt] | = | 2 |
[U42(x1)] | = | -2 + 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 2 + x1 |
[U51(x1, x2)] | = | 2 + 2 · x1 |
[U52(x1)] | = | -2 + 2 · x1 |
[isNatList(x1)] | = | 2 + 2 · x1 |
[U21(x1)] | = | 2 |
[U61(x1, x2)] | = | -2 + 2 · x1 |
[U62(x1)] | = | -2 + 2 · x1 |
[U31(x1)] | = | -2 + x1 |
[isNat(x1)] | = | 2 · x1 |
[s(x1)] | = | 0 |
[U91(x1,...,x4)] | = | -1 + 2 · x2 + x3 + 2 · x4 |
[U92(x1,...,x4)] | = | -2 + x2 + 2 · x3 |
[U93(x1,...,x4)] | = | 2 + 2 · x1 + x3 |
[take(x1, x2)] | = | 2 + 2 · x1 |
[U81(x1)] | = | x1 |
[nil] | = | 2 |
[mark#(x1)] | = | -2 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (143) |
[active#(x1)] | = | -2 |
[U41(x1, x2)] | = | -2 |
[U71(x1, x2, x3)] | = | 1 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 · x1 |
[cons(x1, x2)] | = | -2 + 2 · x2 |
[active(x1)] | = | x1 |
[zeros] | = | 2 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 1 + x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 1 |
[U51(x1, x2)] | = | -2 + x1 |
[U52(x1)] | = | 2 + 2 · x1 |
[isNatList(x1)] | = | 2 |
[U21(x1)] | = | -2 + 2 · x1 |
[U61(x1, x2)] | = | 2 + 2 · x1 |
[U62(x1)] | = | -2 + x1 |
[U31(x1)] | = | 1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + x1 |
[U91(x1,...,x4)] | = | 2 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | 2 + 2 · x3 + 2 · x4 |
[take(x1, x2)] | = | -2 + 2 · x1 |
[U81(x1)] | = | x1 |
[nil] | = | 0 |
[mark#(x1)] | = | -2 + 2 · x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(U52(X)) | → | mark#(X) | (225) |
[active#(x1)] | = | -1 + x1 |
[U41(x1, x2)] | = | 2 + 2 · x2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[active(x1)] | = | 2 + x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 1 + x1 |
[isNatIList(x1)] | = | 1 + 2 · x1 |
[U11(x1)] | = | -2 + x1 |
[U51(x1, x2)] | = | -2 + x2 |
[U52(x1)] | = | -2 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | -2 + x1 |
[U61(x1, x2)] | = | -1 + x1 |
[U62(x1)] | = | -2 + 2 · x1 |
[U31(x1)] | = | x1 |
[isNat(x1)] | = | 2 · x1 |
[s(x1)] | = | 1 + 2 · x1 |
[U91(x1,...,x4)] | = | -1 + 2 · x4 |
[U92(x1,...,x4)] | = | -2 + x1 + x2 + 2 · x4 |
[U93(x1,...,x4)] | = | 1 + 2 · x2 + 2 · x3 |
[take(x1, x2)] | = | 0 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | -1 + x1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (178) |
[active#(x1)] | = | -1 + x1 |
[U41(x1, x2)] | = | 2 |
[U71(x1, x2, x3)] | = | 2 |
[U72(x1, x2)] | = | 2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | -2 + x1 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[active(x1)] | = | -2 + 2 · x1 |
[zeros] | = | 2 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 0 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | -2 + x1 |
[U51(x1, x2)] | = | -2 + x2 |
[U52(x1)] | = | -2 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | -2 + x1 |
[U61(x1, x2)] | = | 2 + x1 + 2 · x2 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | -2 + x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | -2 |
[U91(x1,...,x4)] | = | -2 + 2 · x1 + 2 · x2 + x3 |
[U92(x1,...,x4)] | = | -2 + x1 + 2 · x4 |
[U93(x1,...,x4)] | = | -2 + x1 + x2 |
[take(x1, x2)] | = | -2 |
[U81(x1)] | = | -2 + 2 · x1 |
[nil] | = | 0 |
[mark#(x1)] | = | 1 |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (219) |
[active#(x1)] | = | -2 |
[U41(x1, x2)] | = | 2 + x2 |
[U71(x1, x2, x3)] | = | -2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | 0 |
[mark(x1)] | = | 2 + x1 |
[cons(x1, x2)] | = | -2 + x2 |
[active(x1)] | = | x1 |
[zeros] | = | 1 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 2 · x1 |
[isNatIList(x1)] | = | 0 |
[U11(x1)] | = | 2 |
[U51(x1, x2)] | = | -2 + x1 |
[U52(x1)] | = | -2 + x1 |
[isNatList(x1)] | = | 0 |
[U21(x1)] | = | -2 + 2 · x1 |
[U61(x1, x2)] | = | 2 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | -2 + 2 · x1 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | x1 |
[U91(x1,...,x4)] | = | 2 + x3 + 2 · x4 |
[U92(x1,...,x4)] | = | 2 + 2 · x3 |
[U93(x1,...,x4)] | = | 2 |
[take(x1, x2)] | = | 2 |
[U81(x1)] | = | -2 |
[nil] | = | 0 |
[mark#(x1)] | = | x1 |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U42(active(X)) | → | U42(X) | (71) |
U42(mark(X)) | → | U42(X) | (70) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (213) |
[mark#(x1)] | = | -2 |
[U42(x1)] | = | -2 + x1 |
[active#(x1)] | = | -2 + x1 |
[U71(x1, x2, x3)] | = | -2 |
[active(x1)] | = | 2 |
[U72(x1, x2)] | = | -2 |
[length(x1)] | = | 2 |
[mark(x1)] | = | -2 |
[U62(x1)] | = | -2 |
[U81(x1)] | = | 2 |
[U91(x1,...,x4)] | = | -2 + x2 |
[isNatIList(x1)] | = | 0 |
[U21(x1)] | = | 2 + 2 · x1 |
[U41(x1, x2)] | = | 1 + 2 · x1 |
[U51(x1, x2)] | = | 2 + 2 · x2 |
[U61(x1, x2)] | = | 2 + 2 · x2 |
[U92(x1,...,x4)] | = | -2 + 2 · x4 |
[U93(x1,...,x4)] | = | -2 + 2 · x2 + x3 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 0 |
[cons(x1, x2)] | = | -1 + x1 + 2 · x2 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 2 |
[U11(x1)] | = | 1 |
[U52(x1)] | = | -2 + 2 · x1 |
[isNatList(x1)] | = | 0 |
[U31(x1)] | = | 2 |
[take(x1, x2)] | = | 0 |
[nil] | = | 0 |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (139) |
[mark#(x1)] | = | -2 + 2 · x1 |
[U72(x1, x2)] | = | -2 |
[active#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 1 |
[active(x1)] | = | 2 · x1 |
[mark(x1)] | = | 2 · x1 |
[length(x1)] | = | 0 |
[U21(x1)] | = | 2 |
[U41(x1, x2)] | = | 2 |
[U51(x1, x2)] | = | -2 + x1 + 2 · x2 |
[U61(x1, x2)] | = | 2 + x2 |
[U92(x1,...,x4)] | = | 2 |
[U93(x1,...,x4)] | = | 2 + 2 · x2 + x3 |
[isNat(x1)] | = | 0 |
[s(x1)] | = | 1 + x1 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | 2 + 2 · x1 |
[isNatIList(x1)] | = | 1 + 2 · x1 |
[U11(x1)] | = | 2 |
[U52(x1)] | = | -2 + x1 |
[isNatList(x1)] | = | 1 + x1 |
[U62(x1)] | = | 2 |
[U31(x1)] | = | 2 |
[U91(x1,...,x4)] | = | -1 + x1 + x2 + 2 · x4 |
[take(x1, x2)] | = | 2 |
[U81(x1)] | = | 1 |
[nil] | = | 0 |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(U42(X)) | → | mark#(X) | (218) |
[active#(x1)] | = |
|
||||||||||||||||||||
[U71(x1, x2, x3)] | = |
|
||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||
[mark#(x1)] | = |
|
||||||||||||||||||||
[U72(x1, x2)] | = |
|
||||||||||||||||||||
[isNat(x1)] | = |
|
||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||
[length(x1)] | = |
|
||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||
[isNatList(x1)] | = |
|
||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||
[0] | = |
|
||||||||||||||||||||
[U41(x1, x2)] | = |
|
||||||||||||||||||||
[U42(x1)] | = |
|
||||||||||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||
[U51(x1, x2)] | = |
|
||||||||||||||||||||
[U52(x1)] | = |
|
||||||||||||||||||||
[U21(x1)] | = |
|
||||||||||||||||||||
[U61(x1, x2)] | = |
|
||||||||||||||||||||
[U62(x1)] | = |
|
||||||||||||||||||||
[U31(x1)] | = |
|
||||||||||||||||||||
[U91(x1,...,x4)] | = |
|
||||||||||||||||||||
[U92(x1,...,x4)] | = |
|
||||||||||||||||||||
[U93(x1,...,x4)] | = |
|
||||||||||||||||||||
[take(x1, x2)] | = |
|
||||||||||||||||||||
[U81(x1)] | = |
|
||||||||||||||||||||
[nil] | = |
|
mark#(s(X)) | → | mark#(X) | (242) |
[mark#(x1)] | = | 2 + x1 |
[U72(x1, x2)] | = | 0 |
[active#(x1)] | = | 2 |
[U71(x1, x2, x3)] | = | -2 |
[active(x1)] | = | 2 |
[mark(x1)] | = | -2 + 2 · x1 |
[length(x1)] | = | 2 |
[U21(x1)] | = | 2 + 2 · x1 |
[U41(x1, x2)] | = | -2 + 2 · x1 |
[U51(x1, x2)] | = | -2 + x1 |
[U61(x1, x2)] | = | -2 + 2 · x2 |
[U92(x1,...,x4)] | = | -2 + 2 · x3 + 2 · x4 |
[U93(x1,...,x4)] | = | -2 + x1 + x2 |
[isNat(x1)] | = | x1 |
[s(x1)] | = | -2 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[U42(x1)] | = | -2 + 2 · x1 |
[isNatIList(x1)] | = | 2 · x1 |
[U11(x1)] | = | 1 + 2 · x1 |
[U52(x1)] | = | 2 + 2 · x1 |
[isNatList(x1)] | = | 2 |
[U62(x1)] | = | -2 + 2 · x1 |
[U31(x1)] | = | -2 + 2 · x1 |
[U91(x1,...,x4)] | = | -2 + 2 · x3 + 2 · x4 |
[take(x1, x2)] | = | -2 + x1 |
[U81(x1)] | = | 2 |
[nil] | = | 0 |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
mark#(length(X)) | → | active#(length(mark(X))) | (243) |
prec(U71) | = | 3 | weight(U71) | = | 3 | ||||
prec(U72) | = | 1 | weight(U72) | = | 2 | ||||
prec(s) | = | 0 | weight(s) | = | 1 | ||||
prec(length) | = | 2 | weight(length) | = | 4 |
π(active#) | = | 1 |
π(U71) | = | [] |
π(mark#) | = | 1 |
π(U72) | = | [] |
π(s) | = | [] |
π(length) | = | [] |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
s(active(X)) | → | s(X) | (101) |
s(mark(X)) | → | s(X) | (100) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (151) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (154) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (189) |
The dependency pairs are split into 0 components.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (264) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (263) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (265) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (266) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[cons#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (264) |
1 | ≥ | 1 | |
2 | > | 2 | |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (263) |
1 | > | 1 | |
2 | ≥ | 2 | |
cons#(active(X1),X2) | → | cons#(X1,X2) | (265) |
1 | > | 1 | |
2 | ≥ | 2 | |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (266) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U11#(active(X)) | → | U11#(X) | (268) |
U11#(mark(X)) | → | U11#(X) | (267) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U11#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U11#(active(X)) | → | U11#(X) | (268) |
1 | > | 1 | |
U11#(mark(X)) | → | U11#(X) | (267) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U21#(active(X)) | → | U21#(X) | (270) |
U21#(mark(X)) | → | U21#(X) | (269) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U21#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U21#(active(X)) | → | U21#(X) | (270) |
1 | > | 1 | |
U21#(mark(X)) | → | U21#(X) | (269) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U31#(active(X)) | → | U31#(X) | (272) |
U31#(mark(X)) | → | U31#(X) | (271) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U31#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U31#(active(X)) | → | U31#(X) | (272) |
1 | > | 1 | |
U31#(mark(X)) | → | U31#(X) | (271) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (274) |
U41#(mark(X1),X2) | → | U41#(X1,X2) | (273) |
U41#(active(X1),X2) | → | U41#(X1,X2) | (275) |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (276) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U41#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (274) |
1 | ≥ | 1 | |
2 | > | 2 | |
U41#(mark(X1),X2) | → | U41#(X1,X2) | (273) |
1 | > | 1 | |
2 | ≥ | 2 | |
U41#(active(X1),X2) | → | U41#(X1,X2) | (275) |
1 | > | 1 | |
2 | ≥ | 2 | |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (276) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U42#(active(X)) | → | U42#(X) | (278) |
U42#(mark(X)) | → | U42#(X) | (277) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U42#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U42#(active(X)) | → | U42#(X) | (278) |
1 | > | 1 | |
U42#(mark(X)) | → | U42#(X) | (277) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
isNatIList#(active(X)) | → | isNatIList#(X) | (280) |
isNatIList#(mark(X)) | → | isNatIList#(X) | (279) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[isNatIList#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
isNatIList#(active(X)) | → | isNatIList#(X) | (280) |
1 | > | 1 | |
isNatIList#(mark(X)) | → | isNatIList#(X) | (279) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U51#(X1,mark(X2)) | → | U51#(X1,X2) | (282) |
U51#(mark(X1),X2) | → | U51#(X1,X2) | (281) |
U51#(active(X1),X2) | → | U51#(X1,X2) | (283) |
U51#(X1,active(X2)) | → | U51#(X1,X2) | (284) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U51#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U51#(X1,mark(X2)) | → | U51#(X1,X2) | (282) |
1 | ≥ | 1 | |
2 | > | 2 | |
U51#(mark(X1),X2) | → | U51#(X1,X2) | (281) |
1 | > | 1 | |
2 | ≥ | 2 | |
U51#(active(X1),X2) | → | U51#(X1,X2) | (283) |
1 | > | 1 | |
2 | ≥ | 2 | |
U51#(X1,active(X2)) | → | U51#(X1,X2) | (284) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U52#(active(X)) | → | U52#(X) | (286) |
U52#(mark(X)) | → | U52#(X) | (285) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U52#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U52#(active(X)) | → | U52#(X) | (286) |
1 | > | 1 | |
U52#(mark(X)) | → | U52#(X) | (285) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
isNatList#(active(X)) | → | isNatList#(X) | (288) |
isNatList#(mark(X)) | → | isNatList#(X) | (287) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[isNatList#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
isNatList#(active(X)) | → | isNatList#(X) | (288) |
1 | > | 1 | |
isNatList#(mark(X)) | → | isNatList#(X) | (287) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U61#(X1,mark(X2)) | → | U61#(X1,X2) | (290) |
U61#(mark(X1),X2) | → | U61#(X1,X2) | (289) |
U61#(active(X1),X2) | → | U61#(X1,X2) | (291) |
U61#(X1,active(X2)) | → | U61#(X1,X2) | (292) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U61#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U61#(X1,mark(X2)) | → | U61#(X1,X2) | (290) |
1 | ≥ | 1 | |
2 | > | 2 | |
U61#(mark(X1),X2) | → | U61#(X1,X2) | (289) |
1 | > | 1 | |
2 | ≥ | 2 | |
U61#(active(X1),X2) | → | U61#(X1,X2) | (291) |
1 | > | 1 | |
2 | ≥ | 2 | |
U61#(X1,active(X2)) | → | U61#(X1,X2) | (292) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U62#(active(X)) | → | U62#(X) | (294) |
U62#(mark(X)) | → | U62#(X) | (293) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U62#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U62#(active(X)) | → | U62#(X) | (294) |
1 | > | 1 | |
U62#(mark(X)) | → | U62#(X) | (293) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U71#(X1,mark(X2),X3) | → | U71#(X1,X2,X3) | (296) |
U71#(mark(X1),X2,X3) | → | U71#(X1,X2,X3) | (295) |
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (297) |
U71#(active(X1),X2,X3) | → | U71#(X1,X2,X3) | (298) |
U71#(X1,active(X2),X3) | → | U71#(X1,X2,X3) | (299) |
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (300) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U71#(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U71#(X1,mark(X2),X3) | → | U71#(X1,X2,X3) | (296) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
U71#(mark(X1),X2,X3) | → | U71#(X1,X2,X3) | (295) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (297) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
U71#(active(X1),X2,X3) | → | U71#(X1,X2,X3) | (298) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
U71#(X1,active(X2),X3) | → | U71#(X1,X2,X3) | (299) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (300) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U72#(X1,mark(X2)) | → | U72#(X1,X2) | (302) |
U72#(mark(X1),X2) | → | U72#(X1,X2) | (301) |
U72#(active(X1),X2) | → | U72#(X1,X2) | (303) |
U72#(X1,active(X2)) | → | U72#(X1,X2) | (304) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U72#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U72#(X1,mark(X2)) | → | U72#(X1,X2) | (302) |
1 | ≥ | 1 | |
2 | > | 2 | |
U72#(mark(X1),X2) | → | U72#(X1,X2) | (301) |
1 | > | 1 | |
2 | ≥ | 2 | |
U72#(active(X1),X2) | → | U72#(X1,X2) | (303) |
1 | > | 1 | |
2 | ≥ | 2 | |
U72#(X1,active(X2)) | → | U72#(X1,X2) | (304) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
isNat#(active(X)) | → | isNat#(X) | (306) |
isNat#(mark(X)) | → | isNat#(X) | (305) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[isNat#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
isNat#(active(X)) | → | isNat#(X) | (306) |
1 | > | 1 | |
isNat#(mark(X)) | → | isNat#(X) | (305) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
s#(active(X)) | → | s#(X) | (308) |
s#(mark(X)) | → | s#(X) | (307) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[s#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
s#(active(X)) | → | s#(X) | (308) |
1 | > | 1 | |
s#(mark(X)) | → | s#(X) | (307) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
length#(active(X)) | → | length#(X) | (310) |
length#(mark(X)) | → | length#(X) | (309) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[length#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
length#(active(X)) | → | length#(X) | (310) |
1 | > | 1 | |
length#(mark(X)) | → | length#(X) | (309) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U81#(active(X)) | → | U81#(X) | (312) |
U81#(mark(X)) | → | U81#(X) | (311) |
[active(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[U81#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U81#(active(X)) | → | U81#(X) | (312) |
1 | > | 1 | |
U81#(mark(X)) | → | U81#(X) | (311) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U91#(X1,mark(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (314) |
U91#(mark(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (313) |
U91#(X1,X2,mark(X3),X4) | → | U91#(X1,X2,X3,X4) | (315) |
U91#(X1,X2,X3,mark(X4)) | → | U91#(X1,X2,X3,X4) | (316) |
U91#(active(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (317) |
U91#(X1,active(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (318) |
U91#(X1,X2,active(X3),X4) | → | U91#(X1,X2,X3,X4) | (319) |
U91#(X1,X2,X3,active(X4)) | → | U91#(X1,X2,X3,X4) | (320) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U91#(x1,...,x4)] | = | 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U91#(X1,mark(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (314) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U91#(mark(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (313) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U91#(X1,X2,mark(X3),X4) | → | U91#(X1,X2,X3,X4) | (315) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
4 | ≥ | 4 | |
U91#(X1,X2,X3,mark(X4)) | → | U91#(X1,X2,X3,X4) | (316) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | > | 4 | |
U91#(active(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (317) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U91#(X1,active(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (318) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U91#(X1,X2,active(X3),X4) | → | U91#(X1,X2,X3,X4) | (319) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
4 | ≥ | 4 | |
U91#(X1,X2,X3,active(X4)) | → | U91#(X1,X2,X3,X4) | (320) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | > | 4 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U92#(X1,mark(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (322) |
U92#(mark(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (321) |
U92#(X1,X2,mark(X3),X4) | → | U92#(X1,X2,X3,X4) | (323) |
U92#(X1,X2,X3,mark(X4)) | → | U92#(X1,X2,X3,X4) | (324) |
U92#(active(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (325) |
U92#(X1,active(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (326) |
U92#(X1,X2,active(X3),X4) | → | U92#(X1,X2,X3,X4) | (327) |
U92#(X1,X2,X3,active(X4)) | → | U92#(X1,X2,X3,X4) | (328) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U92#(x1,...,x4)] | = | 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U92#(X1,mark(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (322) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U92#(mark(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (321) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U92#(X1,X2,mark(X3),X4) | → | U92#(X1,X2,X3,X4) | (323) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
4 | ≥ | 4 | |
U92#(X1,X2,X3,mark(X4)) | → | U92#(X1,X2,X3,X4) | (324) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | > | 4 | |
U92#(active(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (325) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U92#(X1,active(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (326) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U92#(X1,X2,active(X3),X4) | → | U92#(X1,X2,X3,X4) | (327) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
4 | ≥ | 4 | |
U92#(X1,X2,X3,active(X4)) | → | U92#(X1,X2,X3,X4) | (328) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | > | 4 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U93#(X1,mark(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (330) |
U93#(mark(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (329) |
U93#(X1,X2,mark(X3),X4) | → | U93#(X1,X2,X3,X4) | (331) |
U93#(X1,X2,X3,mark(X4)) | → | U93#(X1,X2,X3,X4) | (332) |
U93#(active(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (333) |
U93#(X1,active(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (334) |
U93#(X1,X2,active(X3),X4) | → | U93#(X1,X2,X3,X4) | (335) |
U93#(X1,X2,X3,active(X4)) | → | U93#(X1,X2,X3,X4) | (336) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[U93#(x1,...,x4)] | = | 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U93#(X1,mark(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (330) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U93#(mark(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (329) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U93#(X1,X2,mark(X3),X4) | → | U93#(X1,X2,X3,X4) | (331) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
4 | ≥ | 4 | |
U93#(X1,X2,X3,mark(X4)) | → | U93#(X1,X2,X3,X4) | (332) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | > | 4 | |
U93#(active(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (333) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U93#(X1,active(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (334) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
4 | ≥ | 4 | |
U93#(X1,X2,active(X3),X4) | → | U93#(X1,X2,X3,X4) | (335) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
4 | ≥ | 4 | |
U93#(X1,X2,X3,active(X4)) | → | U93#(X1,X2,X3,X4) | (336) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
4 | > | 4 |
As there is no critical graph in the transitive closure, there are no infinite chains.
take#(X1,mark(X2)) | → | take#(X1,X2) | (338) |
take#(mark(X1),X2) | → | take#(X1,X2) | (337) |
take#(active(X1),X2) | → | take#(X1,X2) | (339) |
take#(X1,active(X2)) | → | take#(X1,X2) | (340) |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 1 · x1 |
[take#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
take#(X1,mark(X2)) | → | take#(X1,X2) | (338) |
1 | ≥ | 1 | |
2 | > | 2 | |
take#(mark(X1),X2) | → | take#(X1,X2) | (337) |
1 | > | 1 | |
2 | ≥ | 2 | |
take#(active(X1),X2) | → | take#(X1,X2) | (339) |
1 | > | 1 | |
2 | ≥ | 2 | |
take#(X1,active(X2)) | → | take#(X1,X2) | (340) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.