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) |
active(U11(X1,X2,X3)) | → | U11(active(X1),X2,X3) | (17) |
active(U12(X1,X2)) | → | U12(active(X1),X2) | (18) |
active(U13(X)) | → | U13(active(X)) | (19) |
active(U21(X1,X2)) | → | U21(active(X1),X2) | (20) |
active(U22(X)) | → | U22(active(X)) | (21) |
active(U31(X1,X2)) | → | U31(active(X1),X2) | (22) |
active(U41(X1,X2,X3)) | → | U41(active(X1),X2,X3) | (23) |
active(s(X)) | → | s(active(X)) | (24) |
active(plus(X1,X2)) | → | plus(active(X1),X2) | (25) |
active(plus(X1,X2)) | → | plus(X1,active(X2)) | (26) |
active(and(X1,X2)) | → | and(active(X1),X2) | (27) |
U11(mark(X1),X2,X3) | → | mark(U11(X1,X2,X3)) | (28) |
U12(mark(X1),X2) | → | mark(U12(X1,X2)) | (29) |
U13(mark(X)) | → | mark(U13(X)) | (30) |
U21(mark(X1),X2) | → | mark(U21(X1,X2)) | (31) |
U22(mark(X)) | → | mark(U22(X)) | (32) |
U31(mark(X1),X2) | → | mark(U31(X1,X2)) | (33) |
U41(mark(X1),X2,X3) | → | mark(U41(X1,X2,X3)) | (34) |
s(mark(X)) | → | mark(s(X)) | (35) |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (38) |
proper(U11(X1,X2,X3)) | → | U11(proper(X1),proper(X2),proper(X3)) | (39) |
proper(tt) | → | ok(tt) | (40) |
proper(U12(X1,X2)) | → | U12(proper(X1),proper(X2)) | (41) |
proper(isNat(X)) | → | isNat(proper(X)) | (42) |
proper(U13(X)) | → | U13(proper(X)) | (43) |
proper(U21(X1,X2)) | → | U21(proper(X1),proper(X2)) | (44) |
proper(U22(X)) | → | U22(proper(X)) | (45) |
proper(U31(X1,X2)) | → | U31(proper(X1),proper(X2)) | (46) |
proper(U41(X1,X2,X3)) | → | U41(proper(X1),proper(X2),proper(X3)) | (47) |
proper(s(X)) | → | s(proper(X)) | (48) |
proper(plus(X1,X2)) | → | plus(proper(X1),proper(X2)) | (49) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (50) |
proper(0) | → | ok(0) | (51) |
proper(isNatKind(X)) | → | isNatKind(proper(X)) | (52) |
U11(ok(X1),ok(X2),ok(X3)) | → | ok(U11(X1,X2,X3)) | (53) |
U12(ok(X1),ok(X2)) | → | ok(U12(X1,X2)) | (54) |
isNat(ok(X)) | → | ok(isNat(X)) | (55) |
U13(ok(X)) | → | ok(U13(X)) | (56) |
U21(ok(X1),ok(X2)) | → | ok(U21(X1,X2)) | (57) |
U22(ok(X)) | → | ok(U22(X)) | (58) |
U31(ok(X1),ok(X2)) | → | ok(U31(X1,X2)) | (59) |
U41(ok(X1),ok(X2),ok(X3)) | → | ok(U41(X1,X2,X3)) | (60) |
s(ok(X)) | → | ok(s(X)) | (61) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (63) |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
top(mark(X)) | → | top(proper(X)) | (65) |
top(ok(X)) | → | top(active(X)) | (66) |
There are 112 ruless (increase limit for explicit display).
The dependency pairs are split into 15 components.
top#(mark(X)) | → | top#(proper(X)) | (85) |
top#(ok(X)) | → | top#(active(X)) | (136) |
π(isNatKind) | = | 1 |
π(top#) | = | 1 |
π(proper) | = | 1 |
π(ok) | = | 1 |
π(isNat) | = | 1 |
π(active) | = | 1 |
π(active#) | = | 1 |
π(U21#) | = | 1 |
π(and#) | = | 2 |
prec(U21) | = | 2 | status(U21) | = | [2, 1] | list-extension(U21) | = | Lex | ||
prec(U11) | = | 2 | status(U11) | = | [3, 1, 2] | list-extension(U11) | = | Lex | ||
prec(s) | = | 3 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(isNat#) | = | 0 | status(isNat#) | = | [] | list-extension(isNat#) | = | Lex | ||
prec(top) | = | 0 | status(top) | = | [] | list-extension(top) | = | Lex | ||
prec(and) | = | 2 | status(and) | = | [1, 2] | list-extension(and) | = | Lex | ||
prec(plus#) | = | 0 | status(plus#) | = | [] | list-extension(plus#) | = | Lex | ||
prec(U13#) | = | 0 | status(U13#) | = | [] | list-extension(U13#) | = | Lex | ||
prec(U12) | = | 1 | status(U12) | = | [1, 2] | list-extension(U12) | = | Lex | ||
prec(U12#) | = | 0 | status(U12#) | = | [2, 1] | list-extension(U12#) | = | Lex | ||
prec(0) | = | 6 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(mark) | = | 0 | status(mark) | = | [1] | list-extension(mark) | = | Lex | ||
prec(proper#) | = | 0 | status(proper#) | = | [] | list-extension(proper#) | = | Lex | ||
prec(plus) | = | 4 | status(plus) | = | [2, 1] | list-extension(plus) | = | Lex | ||
prec(U11#) | = | 0 | status(U11#) | = | [1, 3, 2] | list-extension(U11#) | = | Lex | ||
prec(U31) | = | 2 | status(U31) | = | [2, 1] | list-extension(U31) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [2, 3, 1] | list-extension(U41#) | = | Lex | ||
prec(U22#) | = | 0 | status(U22#) | = | [] | list-extension(U22#) | = | Lex | ||
prec(tt) | = | 1 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U13) | = | 0 | status(U13) | = | [1] | list-extension(U13) | = | Lex | ||
prec(U22) | = | 2 | status(U22) | = | [1] | list-extension(U22) | = | Lex | ||
prec(isNatKind#) | = | 0 | status(isNatKind#) | = | [] | list-extension(isNatKind#) | = | Lex | ||
prec(U41) | = | 4 | status(U41) | = | [2, 3, 1] | list-extension(U41) | = | Lex | ||
prec(U31#) | = | 0 | status(U31#) | = | [2, 1] | list-extension(U31#) | = | Lex |
[U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[plus#(x1, x2)] | = | max(0) |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U12#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[0] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[proper#(x1)] | = | 0 |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U11#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U31(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U41#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | x1 + 0 |
[U22(x1)] | = | x1 + 0 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U31#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
active(U12(X1,X2)) | → | U12(active(X1),X2) | (18) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (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) |
U12(ok(X1),ok(X2)) | → | ok(U12(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) |
active(U22(X)) | → | U22(active(X)) | (21) |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
active(plus(X1,X2)) | → | plus(X1,active(X2)) | (26) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (63) |
active(U13(X)) | → | U13(active(X)) | (19) |
U22(mark(X)) | → | mark(U22(X)) | (32) |
active(U11(X1,X2,X3)) | → | U11(active(X1),X2,X3) | (17) |
U41(ok(X1),ok(X2),ok(X3)) | → | ok(U41(X1,X2,X3)) | (60) |
active(and(X1,X2)) | → | and(active(X1),X2) | (27) |
U41(mark(X1),X2,X3) | → | mark(U41(X1,X2,X3)) | (34) |
active(U31(X1,X2)) | → | U31(active(X1),X2) | (22) |
U11(mark(X1),X2,X3) | → | mark(U11(X1,X2,X3)) | (28) |
proper(U21(X1,X2)) | → | U21(proper(X1),proper(X2)) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
U31(mark(X1),X2) | → | mark(U31(X1,X2)) | (33) |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
proper(U11(X1,X2,X3)) | → | U11(proper(X1),proper(X2),proper(X3)) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
active(U21(X1,X2)) | → | U21(active(X1),X2) | (20) |
active(plus(X1,X2)) | → | plus(active(X1),X2) | (25) |
proper(plus(X1,X2)) | → | plus(proper(X1),proper(X2)) | (49) |
proper(isNatKind(X)) | → | isNatKind(proper(X)) | (52) |
U13(mark(X)) | → | mark(U13(X)) | (30) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U13(ok(X)) | → | ok(U13(X)) | (56) |
U21(mark(X1),X2) | → | mark(U21(X1,X2)) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
proper(U22(X)) | → | U22(proper(X)) | (45) |
active(U41(X1,X2,X3)) | → | U41(active(X1),X2,X3) | (23) |
active(s(X)) | → | s(active(X)) | (24) |
U21(ok(X1),ok(X2)) | → | ok(U21(X1,X2)) | (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) |
proper(0) | → | ok(0) | (51) |
proper(tt) | → | ok(tt) | (40) |
isNat(ok(X)) | → | ok(isNat(X)) | (55) |
U31(ok(X1),ok(X2)) | → | ok(U31(X1,X2)) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (38) |
s(ok(X)) | → | ok(s(X)) | (61) |
U22(ok(X)) | → | ok(U22(X)) | (58) |
proper(s(X)) | → | s(proper(X)) | (48) |
U11(ok(X1),ok(X2),ok(X3)) | → | ok(U11(X1,X2,X3)) | (53) |
proper(U41(X1,X2,X3)) | → | U41(proper(X1),proper(X2),proper(X3)) | (47) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
proper(U12(X1,X2)) | → | U12(proper(X1),proper(X2)) | (41) |
proper(isNat(X)) | → | isNat(proper(X)) | (42) |
proper(U31(X1,X2)) | → | U31(proper(X1),proper(X2)) | (46) |
s(mark(X)) | → | mark(s(X)) | (35) |
U12(mark(X1),X2) | → | mark(U12(X1,X2)) | (29) |
proper(U13(X)) | → | U13(proper(X)) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
top#(mark(X)) | → | top#(proper(X)) | (85) |
The dependency pairs are split into 1 component.
top#(ok(X)) | → | top#(active(X)) | (136) |
[isNatKind(x1)] | = | x1 + 0 |
[U21(x1, x2)] | = | x2 + 1 |
[U11(x1, x2, x3)] | = | x2 + 5744 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 1 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | x1 + 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 1 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 2 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 28805 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 17008 |
[plus(x1, x2)] | = | x2 + 0 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[U31(x1, x2)] | = | x2 + 19188 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 43843 |
[U13(x1)] | = | x1 + 0 |
[U22(x1)] | = | x1 + 41745 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x3 + 1 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
active(U12(X1,X2)) | → | U12(active(X1),X2) | (18) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (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) |
U12(ok(X1),ok(X2)) | → | ok(U12(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) |
active(U22(X)) | → | U22(active(X)) | (21) |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
active(plus(X1,X2)) | → | plus(X1,active(X2)) | (26) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (63) |
active(U13(X)) | → | U13(active(X)) | (19) |
U22(mark(X)) | → | mark(U22(X)) | (32) |
active(U11(X1,X2,X3)) | → | U11(active(X1),X2,X3) | (17) |
U41(ok(X1),ok(X2),ok(X3)) | → | ok(U41(X1,X2,X3)) | (60) |
active(and(X1,X2)) | → | and(active(X1),X2) | (27) |
U41(mark(X1),X2,X3) | → | mark(U41(X1,X2,X3)) | (34) |
active(U31(X1,X2)) | → | U31(active(X1),X2) | (22) |
U11(mark(X1),X2,X3) | → | mark(U11(X1,X2,X3)) | (28) |
proper(U21(X1,X2)) | → | U21(proper(X1),proper(X2)) | (44) |
active(U22(tt)) | → | mark(tt) | (5) |
U31(mark(X1),X2) | → | mark(U31(X1,X2)) | (33) |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
active(isNat(plus(V1,V2))) | → | mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) | (10) |
proper(U11(X1,X2,X3)) | → | U11(proper(X1),proper(X2),proper(X3)) | (39) |
active(U41(tt,M,N)) | → | mark(s(plus(N,M))) | (7) |
active(U21(X1,X2)) | → | U21(active(X1),X2) | (20) |
active(plus(X1,X2)) | → | plus(active(X1),X2) | (25) |
proper(plus(X1,X2)) | → | plus(proper(X1),proper(X2)) | (49) |
proper(isNatKind(X)) | → | isNatKind(proper(X)) | (52) |
U13(mark(X)) | → | mark(U13(X)) | (30) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
active(isNatKind(s(V1))) | → | mark(isNatKind(V1)) | (14) |
U13(ok(X)) | → | ok(U13(X)) | (56) |
U21(mark(X1),X2) | → | mark(U21(X1,X2)) | (31) |
active(isNatKind(0)) | → | mark(tt) | (12) |
proper(U22(X)) | → | U22(proper(X)) | (45) |
active(U41(X1,X2,X3)) | → | U41(active(X1),X2,X3) | (23) |
active(s(X)) | → | s(active(X)) | (24) |
U21(ok(X1),ok(X2)) | → | ok(U21(X1,X2)) | (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) |
proper(0) | → | ok(0) | (51) |
proper(tt) | → | ok(tt) | (40) |
isNat(ok(X)) | → | ok(isNat(X)) | (55) |
U31(ok(X1),ok(X2)) | → | ok(U31(X1,X2)) | (59) |
active(U31(tt,N)) | → | mark(N) | (6) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (38) |
s(ok(X)) | → | ok(s(X)) | (61) |
U22(ok(X)) | → | ok(U22(X)) | (58) |
proper(s(X)) | → | s(proper(X)) | (48) |
U11(ok(X1),ok(X2),ok(X3)) | → | ok(U11(X1,X2,X3)) | (53) |
proper(U41(X1,X2,X3)) | → | U41(proper(X1),proper(X2),proper(X3)) | (47) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
proper(U12(X1,X2)) | → | U12(proper(X1),proper(X2)) | (41) |
proper(isNat(X)) | → | isNat(proper(X)) | (42) |
proper(U31(X1,X2)) | → | U31(proper(X1),proper(X2)) | (46) |
s(mark(X)) | → | mark(s(X)) | (35) |
U12(mark(X1),X2) | → | mark(U12(X1,X2)) | (29) |
proper(U13(X)) | → | U13(proper(X)) | (43) |
active(U12(tt,V2)) | → | mark(U13(isNat(V2))) | (2) |
top#(ok(X)) | → | top#(active(X)) | (136) |
The dependency pairs are split into 0 components.
active#(and(X1,X2)) | → | active#(X1) | (114) |
active#(U11(X1,X2,X3)) | → | active#(X1) | (113) |
active#(U22(X)) | → | active#(X) | (99) |
active#(U21(X1,X2)) | → | active#(X1) | (96) |
active#(plus(X1,X2)) | → | active#(X2) | (151) |
active#(U13(X)) | → | active#(X) | (150) |
active#(U12(X1,X2)) | → | active#(X1) | (88) |
active#(U31(X1,X2)) | → | active#(X1) | (87) |
active#(plus(X1,X2)) | → | active#(X1) | (84) |
active#(s(X)) | → | active#(X) | (78) |
active#(U41(X1,X2,X3)) | → | active#(X1) | (137) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + x2 + 25786 |
[U11(x1, x2, x3)] | = | x1 + x2 + 1 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 32306 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + 21643 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + x2 + 6 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[U31(x1, x2)] | = | x1 + 20055 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 4 |
[U13(x1)] | = | x1 + 21648 |
[U22(x1)] | = | x1 + 25791 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x1 + x3 + 1 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
active#(and(X1,X2)) | → | active#(X1) | (114) |
active#(U11(X1,X2,X3)) | → | active#(X1) | (113) |
active#(U22(X)) | → | active#(X) | (99) |
active#(U21(X1,X2)) | → | active#(X1) | (96) |
active#(plus(X1,X2)) | → | active#(X2) | (151) |
active#(U13(X)) | → | active#(X) | (150) |
active#(U12(X1,X2)) | → | active#(X1) | (88) |
active#(U31(X1,X2)) | → | active#(X1) | (87) |
active#(plus(X1,X2)) | → | active#(X1) | (84) |
active#(s(X)) | → | active#(X) | (78) |
active#(U41(X1,X2,X3)) | → | active#(X1) | (137) |
The dependency pairs are split into 0 components.
proper#(plus(X1,X2)) | → | proper#(X1) | (177) |
proper#(U13(X)) | → | proper#(X) | (174) |
proper#(U12(X1,X2)) | → | proper#(X1) | (171) |
proper#(U21(X1,X2)) | → | proper#(X1) | (117) |
proper#(U21(X1,X2)) | → | proper#(X2) | (111) |
proper#(s(X)) | → | proper#(X) | (110) |
proper#(U12(X1,X2)) | → | proper#(X2) | (165) |
proper#(and(X1,X2)) | → | proper#(X1) | (108) |
proper#(U41(X1,X2,X3)) | → | proper#(X3) | (164) |
proper#(U31(X1,X2)) | → | proper#(X2) | (104) |
proper#(isNat(X)) | → | proper#(X) | (102) |
proper#(plus(X1,X2)) | → | proper#(X2) | (101) |
proper#(U41(X1,X2,X3)) | → | proper#(X1) | (156) |
proper#(and(X1,X2)) | → | proper#(X2) | (95) |
proper#(U11(X1,X2,X3)) | → | proper#(X2) | (153) |
proper#(U11(X1,X2,X3)) | → | proper#(X1) | (94) |
proper#(U11(X1,X2,X3)) | → | proper#(X3) | (91) |
proper#(isNatKind(X)) | → | proper#(X) | (86) |
proper#(U22(X)) | → | proper#(X) | (77) |
proper#(U31(X1,X2)) | → | proper#(X1) | (138) |
proper#(U41(X1,X2,X3)) | → | proper#(X2) | (134) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | x1 + x2 + 1 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + x2 + 1 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 21270 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[proper#(x1)] | = | x1 + 0 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + x2 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 2 |
[U13(x1)] | = | x1 + 1 |
[U22(x1)] | = | x1 + 1 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
proper#(plus(X1,X2)) | → | proper#(X1) | (177) |
proper#(U13(X)) | → | proper#(X) | (174) |
proper#(U12(X1,X2)) | → | proper#(X1) | (171) |
proper#(U21(X1,X2)) | → | proper#(X1) | (117) |
proper#(U21(X1,X2)) | → | proper#(X2) | (111) |
proper#(s(X)) | → | proper#(X) | (110) |
proper#(U12(X1,X2)) | → | proper#(X2) | (165) |
proper#(and(X1,X2)) | → | proper#(X1) | (108) |
proper#(U41(X1,X2,X3)) | → | proper#(X3) | (164) |
proper#(U31(X1,X2)) | → | proper#(X2) | (104) |
proper#(isNat(X)) | → | proper#(X) | (102) |
proper#(plus(X1,X2)) | → | proper#(X2) | (101) |
proper#(U41(X1,X2,X3)) | → | proper#(X1) | (156) |
proper#(and(X1,X2)) | → | proper#(X2) | (95) |
proper#(U11(X1,X2,X3)) | → | proper#(X2) | (153) |
proper#(U11(X1,X2,X3)) | → | proper#(X1) | (94) |
proper#(U11(X1,X2,X3)) | → | proper#(X3) | (91) |
proper#(isNatKind(X)) | → | proper#(X) | (86) |
proper#(U22(X)) | → | proper#(X) | (77) |
proper#(U31(X1,X2)) | → | proper#(X1) | (138) |
proper#(U41(X1,X2,X3)) | → | proper#(X2) | (134) |
The dependency pairs are split into 0 components.
U13#(mark(X)) | → | U13#(X) | (74) |
U13#(ok(X)) | → | U13#(X) | (69) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | x1 + x2 + 1 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | x1 + 0 |
[U12(x1, x2)] | = | x1 + x2 + 1 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + x2 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 2 |
[U13(x1)] | = | x1 + 43672 |
[U22(x1)] | = | x1 + 1 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
U13#(ok(X)) | → | U13#(X) | (69) |
The dependency pairs are split into 1 component.
U13#(mark(X)) | → | U13#(X) | (74) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | x1 + x2 + 1 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | x1 + 0 |
[U12(x1, x2)] | = | x1 + x2 + 1 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 5609 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + x2 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 2 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 2 |
[U13(x1)] | = | x1 + 25292 |
[U22(x1)] | = | x1 + 1 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x1 + x2 + x3 + 31088 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
U13#(mark(X)) | → | U13#(X) | (74) |
The dependency pairs are split into 0 components.
U31#(mark(X1),X2) | → | U31#(X1,X2) | (97) |
U31#(ok(X1),ok(X2)) | → | U31#(X1,X2) | (147) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | x1 + x2 + 1 |
[U11(x1, x2, x3)] | = | x1 + x2 + x3 + 3901 |
[s(x1)] | = | x1 + 28549 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x1 + x2 + 1 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 1 |
[plus(x1, x2)] | = | x1 + x2 + 1 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 2 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 2 |
[U13(x1)] | = | x1 + 34933 |
[U22(x1)] | = | x1 + 1 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[U31#(x1, x2)] | = | x1 + 0 |
[and#(x1, x2)] | = | 0 |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (36) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (62) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (37) |
U31#(mark(X1),X2) | → | U31#(X1,X2) | (97) |
U31#(ok(X1),ok(X2)) | → | U31#(X1,X2) | (147) |
The dependency pairs are split into 0 components.
isNat#(ok(X)) | → | isNat#(X) | (70) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | x2 + 2 |
[s(x1)] | = | 2 |
[isNat#(x1)] | = | x1 + 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 615 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 3 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 24123 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 2 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 31047 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 2 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNat#(ok(X)) | → | isNat#(X) | (70) |
The dependency pairs are split into 0 components.
U12#(ok(X1),ok(X2)) | → | U12#(X1,X2) | (118) |
U12#(mark(X1),X2) | → | U12#(X1,X2) | (144) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 12974 |
[U11(x1, x2, x3)] | = | x2 + 15808 |
[s(x1)] | = | x1 + 4330 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | 2 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 9556 |
[U12#(x1, x2)] | = | x1 + 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 2765 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 2 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 24124 |
[plus(x1, x2)] | = | 19691 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 24292 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 20540 |
[U13(x1)] | = | 13779 |
[U22(x1)] | = | 2526 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 10821 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
U12#(ok(X1),ok(X2)) | → | U12#(X1,X2) | (118) |
U12#(mark(X1),X2) | → | U12#(X1,X2) | (144) |
The dependency pairs are split into 0 components.
U41#(ok(X1),ok(X2),ok(X3)) | → | U41#(X1,X2,X3) | (121) |
U41#(mark(X1),X2,X3) | → | U41#(X1,X2,X3) | (107) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 21653 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 2 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 3 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 32662 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 2 |
[U41#(x1, x2, x3)] | = | x3 + 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 7885 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 2 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
U41#(ok(X1),ok(X2),ok(X3)) | → | U41#(X1,X2,X3) | (121) |
The dependency pairs are split into 1 component.
U41#(mark(X1),X2,X3) | → | U41#(X1,X2,X3) | (107) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 31848 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 8925 |
[0] | = | 36624 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25322 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 22740 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 30144 |
[U41#(x1, x2, x3)] | = | x1 + 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 5437 |
[U22(x1)] | = | 31633 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
U41#(mark(X1),X2,X3) | → | U41#(X1,X2,X3) | (107) |
The dependency pairs are split into 0 components.
s#(ok(X)) | → | s#(X) | (159) |
s#(mark(X)) | → | s#(X) | (93) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 22310 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 13843 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 42765 |
[s#(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 25322 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 22740 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 44873 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 13801 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 11778 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
s#(ok(X)) | → | s#(X) | (159) |
s#(mark(X)) | → | s#(X) | (93) |
The dependency pairs are split into 0 components.
U22#(ok(X)) | → | U22#(X) | (132) |
U22#(mark(X)) | → | U22#(X) | (124) |
[isNatKind(x1)] | = | x1 + 28883 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 17083 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 1131 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 18239 |
[0] | = | 13883 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25322 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 7158 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 12333 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | x1 + 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 16038 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 27469 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
U22#(ok(X)) | → | U22#(X) | (132) |
U22#(mark(X)) | → | U22#(X) | (124) |
The dependency pairs are split into 0 components.
isNatKind#(ok(X)) | → | isNatKind#(X) | (73) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 6465 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 8092 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25322 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 4634 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 12333 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 27743 |
[isNatKind#(x1)] | = | x1 + 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
isNatKind#(ok(X)) | → | isNatKind#(X) | (73) |
The dependency pairs are split into 0 components.
plus#(ok(X1),ok(X2)) | → | plus#(X1,X2) | (115) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (154) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (135) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | x2 + 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25322 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 27808 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 24762 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 29346 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
plus#(ok(X1),ok(X2)) | → | plus#(X1,X2) | (115) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (154) |
The dependency pairs are split into 1 component.
plus#(mark(X1),X2) | → | plus#(X1,X2) | (135) |
[isNatKind(x1)] | = | x1 + 21279 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 5051 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | x1 + 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 26158 |
[0] | = | 20704 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25322 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 30192 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 2138 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 30999 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (135) |
The dependency pairs are split into 0 components.
U11#(ok(X1),ok(X2),ok(X3)) | → | U11#(X1,X2,X3) | (148) |
U11#(mark(X1),X2,X3) | → | U11#(X1,X2,X3) | (82) |
[isNatKind(x1)] | = | x1 + 32465 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 2431 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 22464 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | x2 + 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 2430 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 2430 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 1948 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
U11#(ok(X1),ok(X2),ok(X3)) | → | U11#(X1,X2,X3) | (148) |
The dependency pairs are split into 1 component.
U11#(mark(X1),X2,X3) | → | U11#(X1,X2,X3) | (82) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 25342 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | 421 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 29123 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 10120 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 22464 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | x1 + 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 22284 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 27768 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 15614 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
U11#(mark(X1),X2,X3) | → | U11#(X1,X2,X3) | (82) |
The dependency pairs are split into 0 components.
U21#(mark(X1),X2) | → | U21#(X1,X2) | (75) |
U21#(ok(X1),ok(X2)) | → | U21#(X1,X2) | (71) |
[isNatKind(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 14623 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 2 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 49249 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 10120 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 9765 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 2 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | x1 + 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 3829 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
U21#(mark(X1),X2) | → | U21#(X1,X2) | (75) |
U21#(ok(X1),ok(X2)) | → | U21#(X1,X2) | (71) |
The dependency pairs are split into 0 components.
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (161) |
and#(mark(X1),X2) | → | and#(X1,X2) | (152) |
[isNatKind(x1)] | = | x1 + 26106 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 30352 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[top#(x1)] | = | 0 |
[U13#(x1)] | = | 0 |
[U12(x1, x2)] | = | x2 + 27366 |
[U12#(x1, x2)] | = | 0 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 2 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 10120 |
[proper#(x1)] | = | 0 |
[isNat(x1)] | = | 9765 |
[plus(x1, x2)] | = | 2 |
[U11#(x1, x2, x3)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 2 |
[U41#(x1, x2, x3)] | = | 0 |
[active#(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 0 |
[U13(x1)] | = | 2 |
[U22(x1)] | = | 2 |
[isNatKind#(x1)] | = | 0 |
[U41(x1, x2, x3)] | = | x2 + x3 + 2 |
[U31#(x1, x2)] | = | 0 |
[and#(x1, x2)] | = | x1 + x2 + 0 |
isNatKind(ok(X)) | → | ok(isNatKind(X)) | (64) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (161) |
and#(mark(X1),X2) | → | and#(X1,X2) | (152) |
The dependency pairs are split into 0 components.