The rewrite relation of the following TRS is considered.
U101(tt,M,N) | → | U102(isNatKind(activate(M)),activate(M),activate(N)) | (1) |
U102(tt,M,N) | → | U103(isNat(activate(N)),activate(M),activate(N)) | (2) |
U103(tt,M,N) | → | U104(isNatKind(activate(N)),activate(M),activate(N)) | (3) |
U104(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
U11(tt,V1,V2) | → | U12(isNatKind(activate(V1)),activate(V1),activate(V2)) | (5) |
U12(tt,V1,V2) | → | U13(isNatKind(activate(V2)),activate(V1),activate(V2)) | (6) |
U13(tt,V1,V2) | → | U14(isNatKind(activate(V2)),activate(V1),activate(V2)) | (7) |
U14(tt,V1,V2) | → | U15(isNat(activate(V1)),activate(V2)) | (8) |
U15(tt,V2) | → | U16(isNat(activate(V2))) | (9) |
U16(tt) | → | tt | (10) |
U21(tt,V1) | → | U22(isNatKind(activate(V1)),activate(V1)) | (11) |
U22(tt,V1) | → | U23(isNat(activate(V1))) | (12) |
U23(tt) | → | tt | (13) |
U31(tt,V1,V2) | → | U32(isNatKind(activate(V1)),activate(V1),activate(V2)) | (14) |
U32(tt,V1,V2) | → | U33(isNatKind(activate(V2)),activate(V1),activate(V2)) | (15) |
U33(tt,V1,V2) | → | U34(isNatKind(activate(V2)),activate(V1),activate(V2)) | (16) |
U34(tt,V1,V2) | → | U35(isNat(activate(V1)),activate(V2)) | (17) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
U36(tt) | → | tt | (19) |
U41(tt,V2) | → | U42(isNatKind(activate(V2))) | (20) |
U42(tt) | → | tt | (21) |
U51(tt) | → | tt | (22) |
U61(tt,V2) | → | U62(isNatKind(activate(V2))) | (23) |
U62(tt) | → | tt | (24) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
U72(tt,N) | → | activate(N) | (26) |
U81(tt,M,N) | → | U82(isNatKind(activate(M)),activate(M),activate(N)) | (27) |
U82(tt,M,N) | → | U83(isNat(activate(N)),activate(M),activate(N)) | (28) |
U83(tt,M,N) | → | U84(isNatKind(activate(N)),activate(M),activate(N)) | (29) |
U84(tt,M,N) | → | s(plus(activate(N),activate(M))) | (30) |
U91(tt,N) | → | U92(isNatKind(activate(N))) | (31) |
U92(tt) | → | 0 | (32) |
isNat(n__0) | → | tt | (33) |
isNat(n__plus(V1,V2)) | → | U11(isNatKind(activate(V1)),activate(V1),activate(V2)) | (34) |
isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)),activate(V1)) | (35) |
isNat(n__x(V1,V2)) | → | U31(isNatKind(activate(V1)),activate(V1),activate(V2)) | (36) |
isNatKind(n__0) | → | tt | (37) |
isNatKind(n__plus(V1,V2)) | → | U41(isNatKind(activate(V1)),activate(V2)) | (38) |
isNatKind(n__s(V1)) | → | U51(isNatKind(activate(V1))) | (39) |
isNatKind(n__x(V1,V2)) | → | U61(isNatKind(activate(V1)),activate(V2)) | (40) |
plus(N,0) | → | U71(isNat(N),N) | (41) |
plus(N,s(M)) | → | U81(isNat(M),M,N) | (42) |
x(N,0) | → | U91(isNat(N),N) | (43) |
x(N,s(M)) | → | U101(isNat(M),M,N) | (44) |
0 | → | n__0 | (45) |
plus(X1,X2) | → | n__plus(X1,X2) | (46) |
s(X) | → | n__s(X) | (47) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(n__0) | → | 0 | (49) |
activate(n__plus(X1,X2)) | → | plus(X1,X2) | (50) |
activate(n__s(X)) | → | s(X) | (51) |
activate(n__x(X1,X2)) | → | x(X1,X2) | (52) |
activate(X) | → | X | (53) |
There are 124 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
There are 113 ruless (increase limit for explicit display).
prec(U102#) | = | 15 | stat(U102#) | = | mul | |
prec(tt) | = | 2 | stat(tt) | = | mul | |
prec(U103#) | = | 15 | stat(U103#) | = | mul | |
prec(isNat) | = | 2 | stat(isNat) | = | mul | |
prec(U104#) | = | 15 | stat(U104#) | = | mul | |
prec(isNatKind) | = | 2 | stat(isNatKind) | = | mul | |
prec(plus#) | = | 8 | stat(plus#) | = | mul | |
prec(x) | = | 15 | stat(x) | = | mul | |
prec(0) | = | 0 | stat(0) | = | mul | |
prec(U71#) | = | 3 | stat(U71#) | = | mul | |
prec(U72#) | = | 1 | stat(U72#) | = | mul | |
prec(n__plus) | = | 8 | stat(n__plus) | = | mul | |
prec(U11#) | = | 8 | stat(U11#) | = | mul | |
prec(U12#) | = | 8 | stat(U12#) | = | mul | |
prec(U13#) | = | 8 | stat(U13#) | = | mul | |
prec(U14#) | = | 8 | stat(U14#) | = | mul | |
prec(U41#) | = | 4 | stat(U41#) | = | mul | |
prec(n__x) | = | 15 | stat(n__x) | = | mul | |
prec(x#) | = | 15 | stat(x#) | = | mul | |
prec(U91#) | = | 9 | stat(U91#) | = | lex | |
prec(n__s) | = | 5 | stat(n__s) | = | mul | |
prec(U61#) | = | 10 | stat(U61#) | = | lex | |
prec(U21#) | = | 2 | stat(U21#) | = | lex | |
prec(U22#) | = | 2 | stat(U22#) | = | lex | |
prec(U31#) | = | 13 | stat(U31#) | = | mul | |
prec(U32#) | = | 13 | stat(U32#) | = | mul | |
prec(U33#) | = | 12 | stat(U33#) | = | mul | |
prec(U34#) | = | 11 | stat(U34#) | = | lex | |
prec(s) | = | 5 | stat(s) | = | mul | |
prec(U101#) | = | 15 | stat(U101#) | = | mul | |
prec(U81#) | = | 8 | stat(U81#) | = | mul | |
prec(U82#) | = | 8 | stat(U82#) | = | mul | |
prec(U83#) | = | 8 | stat(U83#) | = | mul | |
prec(U84#) | = | 8 | stat(U84#) | = | mul | |
prec(n__0) | = | 0 | stat(n__0) | = | mul | |
prec(U102) | = | 15 | stat(U102) | = | mul | |
prec(U103) | = | 15 | stat(U103) | = | mul | |
prec(U104) | = | 15 | stat(U104) | = | mul | |
prec(plus) | = | 8 | stat(plus) | = | mul | |
prec(U71) | = | 7 | stat(U71) | = | mul | |
prec(U72) | = | 6 | stat(U72) | = | lex | |
prec(U101) | = | 15 | stat(U101) | = | mul | |
prec(U11) | = | 2 | stat(U11) | = | mul | |
prec(U31) | = | 2 | stat(U31) | = | mul | |
prec(U61) | = | 2 | stat(U61) | = | mul | |
prec(U91) | = | 14 | stat(U91) | = | mul | |
prec(U22) | = | 2 | stat(U22) | = | mul | |
prec(U81) | = | 8 | stat(U81) | = | mul | |
prec(U82) | = | 8 | stat(U82) | = | mul | |
prec(U83) | = | 8 | stat(U83) | = | mul | |
prec(U84) | = | 8 | stat(U84) | = | mul | |
prec(U12) | = | 2 | stat(U12) | = | mul | |
prec(U13) | = | 2 | stat(U13) | = | mul | |
prec(U14) | = | 2 | stat(U14) | = | mul |
π(U102#) | = | [1,2,3] |
π(tt) | = | [] |
π(U103#) | = | [1,2,3] |
π(isNat) | = | [] |
π(activate) | = | 1 |
π(U104#) | = | [1,2,3] |
π(isNatKind) | = | [] |
π(plus#) | = | [1,2] |
π(x) | = | [1,2] |
π(0) | = | [] |
π(U71#) | = | [2] |
π(U72#) | = | [1,2] |
π(activate#) | = | 1 |
π(n__plus) | = | [1,2] |
π(isNat#) | = | 1 |
π(U11#) | = | [2,3] |
π(U12#) | = | [2,3] |
π(U13#) | = | [2,3] |
π(U14#) | = | [2,3] |
π(U15#) | = | 2 |
π(isNatKind#) | = | 1 |
π(U41#) | = | [2] |
π(n__x) | = | [1,2] |
π(x#) | = | [1,2] |
π(U91#) | = | [2] |
π(n__s) | = | [1] |
π(U61#) | = | [1,2] |
π(U21#) | = | [1,2] |
π(U22#) | = | [1,2] |
π(U31#) | = | [2,3] |
π(U32#) | = | [2,3] |
π(U33#) | = | [1,2,3] |
π(U34#) | = | [1,3,2] |
π(U35#) | = | 2 |
π(s) | = | [1] |
π(U101#) | = | [1,2,3] |
π(U81#) | = | [1,2,3] |
π(U82#) | = | [1,2,3] |
π(U83#) | = | [1,2,3] |
π(U84#) | = | [1,2,3] |
π(n__0) | = | [] |
π(U102) | = | [1,2,3] |
π(U103) | = | [1,2,3] |
π(U104) | = | [1,2,3] |
π(plus) | = | [1,2] |
π(U71) | = | [2] |
π(U72) | = | [1,2] |
π(U101) | = | [1,2,3] |
π(U11) | = | [] |
π(U21) | = | 1 |
π(U31) | = | [] |
π(U41) | = | 1 |
π(U51) | = | 1 |
π(U61) | = | [] |
π(U91) | = | [1,2] |
π(U62) | = | 1 |
π(U22) | = | [] |
π(U23) | = | 1 |
π(U32) | = | 1 |
π(U33) | = | 1 |
π(U34) | = | 1 |
π(U35) | = | 1 |
π(U36) | = | 1 |
π(U92) | = | 1 |
π(U81) | = | [1,2,3] |
π(U82) | = | [1,2,3] |
π(U83) | = | [1,2,3] |
π(U84) | = | [1,2,3] |
π(U42) | = | 1 |
π(U12) | = | [] |
π(U13) | = | [] |
π(U14) | = | [] |
π(U15) | = | 1 |
π(U16) | = | 1 |
U104#(tt,M,N) | → | plus#(x(activate(N),activate(M)),activate(N)) | (66) |
plus#(N,0) | → | U71#(isNat(N),N) | (166) |
U71#(tt,N) | → | U72#(isNatKind(activate(N)),activate(N)) | (120) |
U72#(tt,N) | → | activate#(N) | (123) |
plus#(N,0) | → | isNat#(N) | (167) |
U14#(tt,V1,V2) | → | U15#(isNat(activate(V1)),activate(V2)) | (82) |
isNat#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (145) |
isNatKind#(n__plus(V1,V2)) | → | U41#(isNatKind(activate(V1)),activate(V2)) | (155) |
U41#(tt,V2) | → | isNatKind#(activate(V2)) | (115) |
isNatKind#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (156) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V1) | (157) |
x#(N,0) | → | U91#(isNat(N),N) | (170) |
U91#(tt,N) | → | isNatKind#(activate(N)) | (141) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V2) | (158) |
isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | (160) |
isNatKind#(n__s(V1)) | → | activate#(V1) | (161) |
isNatKind#(n__x(V1,V2)) | → | U61#(isNatKind(activate(V1)),activate(V2)) | (162) |
U61#(tt,V2) | → | isNatKind#(activate(V2)) | (118) |
isNatKind#(n__x(V1,V2)) | → | isNatKind#(activate(V1)) | (163) |
isNatKind#(n__x(V1,V2)) | → | activate#(V1) | (164) |
isNatKind#(n__x(V1,V2)) | → | activate#(V2) | (165) |
U61#(tt,V2) | → | activate#(V2) | (119) |
U91#(tt,N) | → | activate#(N) | (142) |
x#(N,0) | → | isNat#(N) | (171) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (146) |
isNat#(n__plus(V1,V2)) | → | activate#(V2) | (147) |
isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)),activate(V1)) | (148) |
U22#(tt,V1) | → | isNat#(activate(V1)) | (93) |
isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | (149) |
isNat#(n__s(V1)) | → | activate#(V1) | (150) |
isNat#(n__x(V1,V2)) | → | U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (151) |
U32#(tt,V1,V2) | → | U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (99) |
U33#(tt,V1,V2) | → | U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (103) |
U34#(tt,V1,V2) | → | U35#(isNat(activate(V1)),activate(V2)) | (107) |
isNat#(n__x(V1,V2)) | → | isNatKind#(activate(V1)) | (152) |
isNat#(n__x(V1,V2)) | → | activate#(V1) | (153) |
isNat#(n__x(V1,V2)) | → | activate#(V2) | (154) |
U34#(tt,V1,V2) | → | isNat#(activate(V1)) | (108) |
U34#(tt,V1,V2) | → | activate#(V1) | (109) |
U34#(tt,V1,V2) | → | activate#(V2) | (110) |
U33#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (104) |
U33#(tt,V1,V2) | → | activate#(V2) | (105) |
U33#(tt,V1,V2) | → | activate#(V1) | (106) |
U32#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (100) |
U32#(tt,V1,V2) | → | activate#(V2) | (101) |
U32#(tt,V1,V2) | → | activate#(V1) | (102) |
U31#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (96) |
U31#(tt,V1,V2) | → | activate#(V1) | (97) |
U31#(tt,V1,V2) | → | activate#(V2) | (98) |
U22#(tt,V1) | → | activate#(V1) | (94) |
U21#(tt,V1) | → | isNatKind#(activate(V1)) | (90) |
U21#(tt,V1) | → | activate#(V1) | (91) |
x#(N,s(M)) | → | U101#(isNat(M),M,N) | (172) |
U102#(tt,M,N) | → | isNat#(activate(N)) | (59) |
U102#(tt,M,N) | → | activate#(N) | (60) |
U102#(tt,M,N) | → | activate#(M) | (61) |
U101#(tt,M,N) | → | isNatKind#(activate(M)) | (55) |
U101#(tt,M,N) | → | activate#(M) | (56) |
U101#(tt,M,N) | → | activate#(N) | (57) |
x#(N,s(M)) | → | isNat#(M) | (173) |
U41#(tt,V2) | → | activate#(V2) | (116) |
U14#(tt,V1,V2) | → | isNat#(activate(V1)) | (83) |
U14#(tt,V1,V2) | → | activate#(V1) | (84) |
U14#(tt,V1,V2) | → | activate#(V2) | (85) |
U13#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (79) |
U13#(tt,V1,V2) | → | activate#(V2) | (80) |
U13#(tt,V1,V2) | → | activate#(V1) | (81) |
U12#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (75) |
U12#(tt,V1,V2) | → | activate#(V2) | (76) |
U12#(tt,V1,V2) | → | activate#(V1) | (77) |
U11#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (71) |
U11#(tt,V1,V2) | → | activate#(V1) | (72) |
U11#(tt,V1,V2) | → | activate#(V2) | (73) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (168) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (137) |
plus#(N,s(M)) | → | isNat#(M) | (169) |
U84#(tt,M,N) | → | activate#(N) | (138) |
U84#(tt,M,N) | → | activate#(M) | (139) |
U83#(tt,M,N) | → | isNatKind#(activate(N)) | (133) |
U83#(tt,M,N) | → | activate#(N) | (134) |
U83#(tt,M,N) | → | activate#(M) | (135) |
U82#(tt,M,N) | → | isNat#(activate(N)) | (129) |
U82#(tt,M,N) | → | activate#(N) | (130) |
U82#(tt,M,N) | → | activate#(M) | (131) |
U81#(tt,M,N) | → | isNatKind#(activate(M)) | (125) |
U81#(tt,M,N) | → | activate#(M) | (126) |
U81#(tt,M,N) | → | activate#(N) | (127) |
U71#(tt,N) | → | isNatKind#(activate(N)) | (121) |
U71#(tt,N) | → | activate#(N) | (122) |
U104#(tt,M,N) | → | x#(activate(N),activate(M)) | (67) |
U104#(tt,M,N) | → | activate#(N) | (68) |
U104#(tt,M,N) | → | activate#(M) | (69) |
U103#(tt,M,N) | → | isNatKind#(activate(N)) | (63) |
U103#(tt,M,N) | → | activate#(N) | (64) |
U103#(tt,M,N) | → | activate#(M) | (65) |
The dependency pairs are split into 0 components.