The rewrite relation of the following TRS is considered.
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
active(U13(tt)) | → | mark(tt) | (3) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(U22(tt)) | → | mark(tt) | (5) |
active(U31(tt,N)) | → | mark(N) | (6) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
active(and(tt,X)) | → | mark(X) | (8) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNatKind(0)) | → | mark(tt) | (12) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
mark(tt) | → | active(tt) | (18) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
mark(0) | → | active(0) | (29) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U13(mark(X)) | → | U13(X) | (43) |
U13(active(X)) | → | U13(X) | (44) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
U22(mark(X)) | → | U22(X) | (49) |
U22(active(X)) | → | U22(X) | (50) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
s(mark(X)) | → | s(X) | (61) |
s(active(X)) | → | s(X) | (62) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
There are 123 ruless (increase limit for explicit display).
The dependency pairs are split into 13 components.
mark#(plus(X1,X2)) | → | mark#(X1) | (193) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
mark#(U41(X1,X2,X3)) | → | active#(U41(mark(X1),X2,X3)) | (142) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
active#(U41(tt,M,N)) | → | mark#(s(plus(N,M))) | (134) |
mark#(U13(X)) | → | active#(U13(mark(X))) | (128) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (185) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (126) |
mark#(plus(X1,X2)) | → | mark#(X2) | (124) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
mark#(U31(X1,X2)) | → | mark#(X1) | (179) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U13(X)) | → | mark#(X) | (116) |
active#(U31(tt,N)) | → | mark#(N) | (171) |
mark#(U22(X)) | → | mark#(X) | (109) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
mark#(U22(X)) | → | active#(U22(mark(X))) | (102) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
active#(and(tt,X)) | → | mark#(X) | (100) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (163) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(s(X)) | → | active#(s(mark(X))) | (89) |
active#(plus(N,0)) | → | mark#(U31(and(isNat(N),isNatKind(N)),N)) | (86) |
active#(plus(N,s(M))) | → | mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (87) |
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
mark#(s(X)) | → | mark#(X) | (153) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
[isNatKind(x1)] | = | 2 |
[U21(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | 2 |
[s(x1)] | = | 1 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | 2 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 4 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 3 |
[isNat(x1)] | = | 2 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | 2 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 7 |
[U13(x1)] | = | 1 |
[U22(x1)] | = | 1 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U22(active(X)) | → | U22(X) | (50) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
s(active(X)) | → | s(X) | (62) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
U13(mark(X)) | → | U13(X) | (43) |
mark#(U13(X)) | → | active#(U13(mark(X))) | (128) |
mark#(U22(X)) | → | active#(U22(mark(X))) | (102) |
mark#(s(X)) | → | active#(s(mark(X))) | (89) |
The dependency pairs are split into 1 component.
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
active#(plus(N,0)) | → | mark#(U31(and(isNat(N),isNatKind(N)),N)) | (86) |
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
active#(plus(N,s(M))) | → | mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (87) |
mark#(U13(X)) | → | mark#(X) | (116) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(plus(X1,X2)) | → | mark#(X2) | (124) |
mark#(plus(X1,X2)) | → | mark#(X1) | (193) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (126) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
active#(U41(tt,M,N)) | → | mark#(s(plus(N,M))) | (134) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (185) |
mark#(U41(X1,X2,X3)) | → | active#(U41(mark(X1),X2,X3)) | (142) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
mark#(U22(X)) | → | mark#(X) | (109) |
mark#(U31(X1,X2)) | → | mark#(X1) | (179) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (163) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
active#(U31(tt,N)) | → | mark#(N) | (171) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + 0 |
[U11(x1, x2, x3)] | = | x1 + 0 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 0 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 0 |
[plus(x1, x2)] | = | x1 + x2 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | x1 + 0 |
[U22(x1)] | = | x1 + 0 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x1 + x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
mark(tt) | → | active(tt) | (18) |
U22(active(X)) | → | U22(X) | (50) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(and(tt,X)) | → | mark(X) | (8) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U13(tt)) | → | mark(tt) | (3) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
s(active(X)) | → | s(X) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
mark(0) | → | active(0) | (29) |
U13(mark(X)) | → | U13(X) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
active#(plus(N,0)) | → | mark#(U31(and(isNat(N),isNatKind(N)),N)) | (86) |
mark#(s(X)) | → | mark#(X) | (153) |
mark#(plus(X1,X2)) | → | mark#(X2) | (124) |
mark#(plus(X1,X2)) | → | mark#(X1) | (193) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (185) |
mark#(U31(X1,X2)) | → | mark#(X1) | (179) |
active#(U31(tt,N)) | → | mark#(N) | (171) |
The dependency pairs are split into 1 component.
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
active#(plus(N,s(M))) | → | mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (87) |
mark#(U13(X)) | → | mark#(X) | (116) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (126) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
active#(U41(tt,M,N)) | → | mark#(s(plus(N,M))) | (134) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
mark#(U41(X1,X2,X3)) | → | active#(U41(mark(X1),X2,X3)) | (142) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
mark#(U22(X)) | → | mark#(X) | (109) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (163) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + 0 |
[U11(x1, x2, x3)] | = | x1 + 0 |
[s(x1)] | = | 4187 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 0 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 52442 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 0 |
[plus(x1, x2)] | = | x1 + x2 + 3044 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | x1 + 0 |
[U22(x1)] | = | x1 + 0 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x3 + 4187 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
mark(tt) | → | active(tt) | (18) |
U22(active(X)) | → | U22(X) | (50) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(and(tt,X)) | → | mark(X) | (8) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U13(tt)) | → | mark(tt) | (3) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
s(active(X)) | → | s(X) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
mark(0) | → | active(0) | (29) |
U13(mark(X)) | → | U13(X) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
active#(plus(N,s(M))) | → | mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (87) |
The dependency pairs are split into 1 component.
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
mark#(U13(X)) | → | mark#(X) | (116) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (126) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
active#(U41(tt,M,N)) | → | mark#(s(plus(N,M))) | (134) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
mark#(U41(X1,X2,X3)) | → | active#(U41(mark(X1),X2,X3)) | (142) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
mark#(U22(X)) | → | mark#(X) | (109) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (163) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + 0 |
[U11(x1, x2, x3)] | = | x1 + 0 |
[s(x1)] | = | 1 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 0 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 0 |
[plus(x1, x2)] | = | x1 + x2 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | x1 + 0 |
[U22(x1)] | = | x1 + 0 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
mark(tt) | → | active(tt) | (18) |
U22(active(X)) | → | U22(X) | (50) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(and(tt,X)) | → | mark(X) | (8) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U13(tt)) | → | mark(tt) | (3) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
s(active(X)) | → | s(X) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
mark(0) | → | active(0) | (29) |
U13(mark(X)) | → | U13(X) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
active#(U41(tt,M,N)) | → | mark#(s(plus(N,M))) | (134) |
The dependency pairs are split into 1 component.
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
mark#(U13(X)) | → | mark#(X) | (116) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (126) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
mark#(U41(X1,X2,X3)) | → | active#(U41(mark(X1),X2,X3)) | (142) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
mark#(U22(X)) | → | mark#(X) | (109) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (163) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
[isNatKind(x1)] | = | 21096 |
[U21(x1, x2)] | = | 21096 |
[U11(x1, x2, x3)] | = | 21096 |
[s(x1)] | = | 1 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | 21096 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 21096 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 21096 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 1 |
[isNat(x1)] | = | 21096 |
[plus(x1, x2)] | = | 21095 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 13825 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 1 |
[U13(x1)] | = | 1 |
[U22(x1)] | = | 1 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | 14022 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
mark(tt) | → | active(tt) | (18) |
U22(active(X)) | → | U22(X) | (50) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(and(tt,X)) | → | mark(X) | (8) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U13(tt)) | → | mark(tt) | (3) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
s(active(X)) | → | s(X) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
mark(0) | → | active(0) | (29) |
U13(mark(X)) | → | U13(X) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (126) |
mark#(U41(X1,X2,X3)) | → | active#(U41(mark(X1),X2,X3)) | (142) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (163) |
The dependency pairs are split into 1 component.
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
mark#(U13(X)) | → | mark#(X) | (116) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
mark#(U22(X)) | → | mark#(X) | (109) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + x2 + 94958 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 101744 |
[s(x1)] | = | x1 + 54225 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + x2 + 61009 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | x1 + 40734 |
[plus(x1, x2)] | = | x1 + x2 + 61011 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x2 + 32157 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | x1 + 11453 |
[U22(x1)] | = | x1 + 30249 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 115236 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
mark(tt) | → | active(tt) | (18) |
U22(active(X)) | → | U22(X) | (50) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(and(tt,X)) | → | mark(X) | (8) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U13(tt)) | → | mark(tt) | (3) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
s(active(X)) | → | s(X) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
mark(0) | → | active(0) | (29) |
U13(mark(X)) | → | U13(X) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
active#(U21(tt,V1)) | → | mark#(U22(isNat(V1))) | (152) |
active#(U11(tt,V1,V2)) | → | mark#(U12(isNat(V1),V2)) | (119) |
mark#(U13(X)) | → | mark#(X) | (116) |
mark#(U12(X1,X2)) | → | mark#(X1) | (135) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (176) |
mark#(U21(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (167) |
mark#(U22(X)) | → | mark#(X) | (109) |
active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1),V1)) | (141) |
active#(U12(tt,V2)) | → | mark#(U13(isNat(V2))) | (184) |
The dependency pairs are split into 1 component.
active#(and(tt,X)) | → | mark#(X) | (100) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
[isNatKind(x1)] | = | 86817 |
[U21(x1, x2)] | = | 28891 |
[U11(x1, x2, x3)] | = | 31545 |
[s(x1)] | = | 39365 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | 86817 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 86816 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 86817 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 28889 |
[plus(x1, x2)] | = | 39361 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x2 + 39363 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 86820 |
[U13(x1)] | = | 86818 |
[U22(x1)] | = | 28893 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 39363 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U22(active(X)) | → | U22(X) | (50) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
s(active(X)) | → | s(X) | (62) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
U13(mark(X)) | → | U13(X) | (43) |
mark#(U12(X1,X2)) | → | active#(U12(mark(X1),X2)) | (165) |
mark#(U11(X1,X2,X3)) | → | active#(U11(mark(X1),X2,X3)) | (78) |
mark#(U21(X1,X2)) | → | active#(U21(mark(X1),X2)) | (98) |
mark#(isNat(X)) | → | active#(isNat(X)) | (107) |
The dependency pairs are split into 1 component.
active#(and(tt,X)) | → | mark#(X) | (100) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
[isNatKind(x1)] | = | x1 + 13259 |
[U21(x1, x2)] | = | x2 + 3 |
[U11(x1, x2, x3)] | = | x2 + x3 + 16844 |
[s(x1)] | = | x1 + 2 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 28312 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + x2 + 16840 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + x2 + 41573 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x2 + 3699 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 1 |
[U13(x1)] | = | x1 + 3137 |
[U22(x1)] | = | x1 + 2 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 41575 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
mark(tt) | → | active(tt) | (18) |
U22(active(X)) | → | U22(X) | (50) |
active(U21(tt,V1)) | → | mark(U22(isNat(V1))) | (4) |
active(plus(N,0)) | → | mark(U31(and(isNat(N),isNatKind(N)),N)) | (15) |
active(and(tt,X)) | → | mark(X) | (8) |
U31(X1,active(X2)) | → | U31(X1,X2) | (54) |
active(U11(tt,V1,V2)) | → | mark(U12(isNat(V1),V2)) | (1) |
active(U13(tt)) | → | mark(tt) | (3) |
active(plus(N,s(M))) | → | mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) | (16) |
mark(U13(X)) | → | active(U13(mark(X))) | (21) |
U11(X1,X2,active(X3)) | → | U11(X1,X2,X3) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (68) |
mark(s(X)) | → | active(s(mark(X))) | (26) |
plus(mark(X1),X2) | → | plus(X1,X2) | (63) |
mark(U12(X1,X2)) | → | active(U12(mark(X1),X2)) | (19) |
U11(X1,mark(X2),X3) | → | U11(X1,X2,X3) | (32) |
mark(U11(X1,X2,X3)) | → | active(U11(mark(X1),X2,X3)) | (17) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (60) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (27) |
U11(active(X1),X2,X3) | → | U11(X1,X2,X3) | (34) |
mark(U21(X1,X2)) | → | active(U21(mark(X1),X2)) | (22) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (28) |
plus(active(X1),X2) | → | plus(X1,X2) | (65) |
U13(active(X)) | → | U13(X) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
isNatKind(active(X)) | → | isNatKind(X) | (72) |
U11(X1,X2,mark(X3)) | → | U11(X1,X2,X3) | (33) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
U12(active(X1),X2) | → | U12(X1,X2) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
mark(isNat(X)) | → | active(isNat(X)) | (20) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (25) |
U22(mark(X)) | → | U22(X) | (49) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (52) |
mark(isNatKind(X)) | → | active(isNatKind(X)) | (30) |
s(active(X)) | → | s(X) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (56) |
U11(mark(X1),X2,X3) | → | U11(X1,X2,X3) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
and(active(X1),X2) | → | and(X1,X2) | (69) |
U21(mark(X1),X2) | → | U21(X1,X2) | (45) |
mark(U22(X)) | → | active(U22(mark(X))) | (23) |
and(X1,active(X2)) | → | and(X1,X2) | (70) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (24) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (57) |
active(isNat(s(V1))) | → | mark(U21(isNatKind(V1),V1)) | (11) |
active(isNat(0)) | → | mark(tt) | (9) |
active(isNatKind(plus(V1,V2))) | → | mark(and(isNatKind(V1),isNatKind(V2))) | (13) |
U31(mark(X1),X2) | → | U31(X1,X2) | (51) |
U12(X1,active(X2)) | → | U12(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (67) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (55) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
U12(X1,mark(X2)) | → | U12(X1,X2) | (38) |
s(mark(X)) | → | s(X) | (61) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (58) |
U21(X1,active(X2)) | → | U21(X1,X2) | (48) |
isNatKind(mark(X)) | → | isNatKind(X) | (71) |
U31(active(X1),X2) | → | U31(X1,X2) | (53) |
U21(active(X1),X2) | → | U21(X1,X2) | (47) |
U12(mark(X1),X2) | → | U12(X1,X2) | (37) |
isNat(mark(X)) | → | isNat(X) | (41) |
isNat(active(X)) | → | isNat(X) | (42) |
U21(X1,mark(X2)) | → | U21(X1,X2) | (46) |
plus(X1,active(X2)) | → | plus(X1,X2) | (66) |
U11(X1,active(X2),X3) | → | U11(X1,X2,X3) | (35) |
mark(0) | → | active(0) | (29) |
U13(mark(X)) | → | U13(X) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
active#(and(tt,X)) | → | mark#(X) | (100) |
mark#(and(X1,X2)) | → | mark#(X1) | (90) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (93) |
mark#(isNatKind(X)) | → | active#(isNatKind(X)) | (143) |
active#(isNatKind(s(V1))) | → | mark#(isNatKind(V1)) | (80) |
active#(isNatKind(plus(V1,V2))) | → | mark#(and(isNatKind(V1),isNatKind(V2))) | (144) |
The dependency pairs are split into 0 components.
U21#(X1,active(X2)) | → | U21#(X1,X2) | (188) |
U21#(active(X1),X2) | → | U21#(X1,X2) | (131) |
U21#(X1,mark(X2)) | → | U21#(X1,X2) | (186) |
U21#(mark(X1),X2) | → | U21#(X1,X2) | (84) |
[isNatKind(x1)] | = | 40 |
[U21(x1, x2)] | = | 43720 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | 29098 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 2 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 3079 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 32023 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | x1 + x2 + 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 50 |
[U13(x1)] | = | x1 + 3137 |
[U22(x1)] | = | x1 + 43721 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 29096 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U21#(X1,active(X2)) | → | U21#(X1,X2) | (188) |
U21#(active(X1),X2) | → | U21#(X1,X2) | (131) |
U21#(X1,mark(X2)) | → | U21#(X1,X2) | (186) |
U21#(mark(X1),X2) | → | U21#(X1,X2) | (84) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (169) |
s#(active(X)) | → | s#(X) | (94) |
[isNatKind(x1)] | = | 9999 |
[U21(x1, x2)] | = | 72906 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 23720 |
[s(x1)] | = | 30877 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 39183 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 97687 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 31936 |
[s#(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 42027 |
[plus(x1, x2)] | = | x1 + 30873 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 51342 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 73965 |
[U13(x1)] | = | x1 + 55662 |
[U22(x1)] | = | x1 + 30881 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 30875 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
s#(mark(X)) | → | s#(X) | (169) |
s#(active(X)) | → | s#(X) | (94) |
The dependency pairs are split into 0 components.
and#(X1,mark(X2)) | → | and#(X1,X2) | (120) |
and#(mark(X1),X2) | → | and#(X1,X2) | (162) |
and#(X1,active(X2)) | → | and#(X1,X2) | (85) |
and#(active(X1),X2) | → | and#(X1,X2) | (81) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 15703 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | 5 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 2 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 7 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 8 |
[U22(x1)] | = | x1 + 15704 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 3 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | x1 + 0 |
and#(mark(X1),X2) | → | and#(X1,X2) | (162) |
and#(active(X1),X2) | → | and#(X1,X2) | (81) |
The dependency pairs are split into 1 component.
and#(X1,mark(X2)) | → | and#(X1,X2) | (120) |
and#(X1,active(X2)) | → | and#(X1,X2) | (85) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 9 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | 6 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 3 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 11458 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 19274 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 20210 |
[U22(x1)] | = | x1 + 10 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 4 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | x2 + 0 |
and#(X1,mark(X2)) | → | and#(X1,X2) | (120) |
and#(X1,active(X2)) | → | and#(X1,X2) | (85) |
The dependency pairs are split into 0 components.
isNatKind#(mark(X)) | → | isNatKind#(X) | (138) |
isNatKind#(active(X)) | → | isNatKind#(X) | (108) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 12767 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 52235 |
[s(x1)] | = | 12764 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 4380 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 52241 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 12760 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 19274 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 52242 |
[U22(x1)] | = | x1 + 12768 |
[isNatKind#(x1)] | = | x1 + 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 12762 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind#(mark(X)) | → | isNatKind#(X) | (138) |
isNatKind#(active(X)) | → | isNatKind#(X) | (108) |
The dependency pairs are split into 0 components.
isNat#(active(X)) | → | isNat#(X) | (114) |
isNat#(mark(X)) | → | isNat#(X) | (150) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 13869 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 29798 |
[s(x1)] | = | 13866 |
[isNat#(x1)] | = | x1 + 0 |
[and(x1, x2)] | = | x1 + 16074 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 29804 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 13862 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 17747 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 29805 |
[U22(x1)] | = | x1 + 13870 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 13864 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNat#(active(X)) | → | isNat#(X) | (114) |
isNat#(mark(X)) | → | isNat#(X) | (150) |
The dependency pairs are split into 0 components.
U22#(active(X)) | → | U22#(X) | (177) |
U22#(mark(X)) | → | U22#(X) | (112) |
[isNatKind(x1)] | = | 13020 |
[U21(x1, x2)] | = | 8 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 50843 |
[s(x1)] | = | 5 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 2 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 104972 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 54124 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 12072 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | x1 + 0 |
[tt] | = | 54127 |
[U13(x1)] | = | x1 + 104973 |
[U22(x1)] | = | x1 + 9 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 3 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U22#(active(X)) | → | U22#(X) | (177) |
U22#(mark(X)) | → | U22#(X) | (112) |
The dependency pairs are split into 0 components.
U12#(X1,mark(X2)) | → | U12#(X1,X2) | (195) |
U12#(X1,active(X2)) | → | U12#(X1,X2) | (123) |
U12#(mark(X1),X2) | → | U12#(X1,X2) | (115) |
U12#(active(X1),X2) | → | U12#(X1,X2) | (105) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 27133 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 7325 |
[s(x1)] | = | 27130 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 23724 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 7331 |
[U12#(x1, x2)] | = | x1 + x2 + 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 25567 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 7332 |
[U22(x1)] | = | x1 + 27134 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 27128 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U12#(X1,mark(X2)) | → | U12#(X1,X2) | (195) |
U12#(X1,active(X2)) | → | U12#(X1,X2) | (123) |
U12#(mark(X1),X2) | → | U12#(X1,X2) | (115) |
U12#(active(X1),X2) | → | U12#(X1,X2) | (105) |
The dependency pairs are split into 0 components.
plus#(active(X1),X2) | → | plus#(X1,X2) | (122) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (110) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (160) |
plus#(X1,active(X2)) | → | plus#(X1,X2) | (148) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 54766 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | 22169 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 2 |
[plus#(x1, x2)] | = | x1 + x2 + 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 7 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 32621 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 7335 |
[U22(x1)] | = | x1 + 54767 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 22167 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
plus#(active(X1),X2) | → | plus#(X1,X2) | (122) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (110) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (160) |
plus#(X1,active(X2)) | → | plus#(X1,X2) | (148) |
The dependency pairs are split into 0 components.
U31#(X1,mark(X2)) | → | U31#(X1,X2) | (194) |
U31#(mark(X1),X2) | → | U31#(X1,X2) | (121) |
U31#(active(X1),X2) | → | U31#(X1,X2) | (113) |
U31#(X1,active(X2)) | → | U31#(X1,X2) | (97) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 28595 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | 15811 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 24632 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 7 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 32621 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 8 |
[U22(x1)] | = | x1 + 28596 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 15809 |
[U31#(x1, x2)] | = | x2 + 0 |
[and#(x1, x2)] | = | 0 |
U31#(X1,mark(X2)) | → | U31#(X1,X2) | (194) |
U31#(X1,active(X2)) | → | U31#(X1,X2) | (97) |
The dependency pairs are split into 1 component.
U31#(mark(X1),X2) | → | U31#(X1,X2) | (121) |
U31#(active(X1),X2) | → | U31#(X1,X2) | (113) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 7883 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | 7526 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 2 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 33009 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 33003 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 32621 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 33006 |
[U13(x1)] | = | x1 + 33010 |
[U22(x1)] | = | x1 + 7884 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 7524 |
[U31#(x1, x2)] | = | x1 + 0 |
[and#(x1, x2)] | = | 0 |
U31#(mark(X1),X2) | → | U31#(X1,X2) | (121) |
U31#(active(X1),X2) | → | U31#(X1,X2) | (113) |
The dependency pairs are split into 0 components.
U11#(active(X1),X2,X3) | → | U11#(X1,X2,X3) | (183) |
U11#(X1,active(X2),X3) | → | U11#(X1,X2,X3) | (104) |
U11#(mark(X1),X2,X3) | → | U11#(X1,X2,X3) | (159) |
U11#(X1,X2,active(X3)) | → | U11#(X1,X2,X3) | (83) |
U11#(X1,X2,mark(X3)) | → | U11#(X1,X2,X3) | (79) |
U11#(X1,mark(X2),X3) | → | U11#(X1,X2,X3) | (74) |
[isNatKind(x1)] | = | 1 |
[U21(x1, x2)] | = | 8 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 16516 |
[s(x1)] | = | 5 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 31609 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 22122 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 41193 |
[U22(x1)] | = | x1 + 9 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 3 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U11#(active(X1),X2,X3) | → | U11#(X1,X2,X3) | (183) |
U11#(X1,active(X2),X3) | → | U11#(X1,X2,X3) | (104) |
U11#(mark(X1),X2,X3) | → | U11#(X1,X2,X3) | (159) |
U11#(X1,X2,active(X3)) | → | U11#(X1,X2,X3) | (83) |
U11#(X1,X2,mark(X3)) | → | U11#(X1,X2,X3) | (79) |
U11#(X1,mark(X2),X3) | → | U11#(X1,X2,X3) | (74) |
The dependency pairs are split into 0 components.
U13#(mark(X)) | → | U13#(X) | (191) |
U13#(active(X)) | → | U13#(X) | (129) |
[isNatKind(x1)] | = | 2 |
[U21(x1, x2)] | = | 31639 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 5436 |
[s(x1)] | = | 31636 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 22740 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | x1 + 0 |
[U12(x1, x2)] | = | 5442 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 29716 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 5443 |
[U22(x1)] | = | x1 + 31640 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 31634 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U13#(mark(X)) | → | U13#(X) | (191) |
U13#(active(X)) | → | U13#(X) | (129) |
The dependency pairs are split into 0 components.
U41#(X1,X2,active(X3)) | → | U41#(X1,X2,X3) | (136) |
U41#(X1,mark(X2),X3) | → | U41#(X1,X2,X3) | (127) |
U41#(active(X1),X2,X3) | → | U41#(X1,X2,X3) | (181) |
U41#(mark(X1),X2,X3) | → | U41#(X1,X2,X3) | (180) |
U41#(X1,X2,mark(X3)) | → | U41#(X1,X2,X3) | (155) |
U41#(X1,active(X2),X3) | → | U41#(X1,X2,X3) | (146) |
[isNatKind(x1)] | = | 2 |
[U21(x1, x2)] | = | 8 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 5874 |
[s(x1)] | = | 5 |
[isNat#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 2 |
[plus#(x1, x2)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 33606 |
[U12#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 33607 |
[U22(x1)] | = | x1 + 17241 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 3 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U41#(X1,X2,active(X3)) | → | U41#(X1,X2,X3) | (136) |
U41#(X1,mark(X2),X3) | → | U41#(X1,X2,X3) | (127) |
U41#(active(X1),X2,X3) | → | U41#(X1,X2,X3) | (181) |
U41#(mark(X1),X2,X3) | → | U41#(X1,X2,X3) | (180) |
U41#(X1,X2,mark(X3)) | → | U41#(X1,X2,X3) | (155) |
U41#(X1,active(X2),X3) | → | U41#(X1,X2,X3) | (146) |
The dependency pairs are split into 0 components.