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 142 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
There are 131 ruless (increase limit for explicit display).
[0#] | = | 0 |
[U72#(x1, x2)] | = | max(x2 + 0, 0) |
[U32#(x1, x2, x3)] | = | max(x1 + 73501, x2 + 73501, x3 + 73502, 0) |
[isNatKind(x1)] | = | 28940 |
[U16(x1)] | = | 1 |
[U21(x1, x2)] | = | max(x1 + 36404, 0) |
[U83#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 86825, x2 + 1, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | x1 + 0 |
[U42(x1)] | = | 0 |
[U91(x1, x2)] | = | max(x2 + 12831, 0) |
[U35#(x1, x2)] | = | max(x2 + 15620, 0) |
[U101#(x1, x2, x3)] | = | max(x2 + 102442, x3 + 131383, 0) |
[activate(x1)] | = | x1 + 0 |
[U82#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U104#(x1, x2, x3)] | = | max(x1 + 102443, x2 + 102442, x3 + 131383, 0) |
[U71(x1, x2)] | = | max(x2 + 0, 0) |
[U81#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U92#(x1)] | = | 0 |
[plus#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U101(x1, x2, x3)] | = | max(x2 + 102442, x3 + 131383, 0) |
[activate#(x1)] | = | x1 + 0 |
[U103(x1, x2, x3)] | = | max(x2 + 102442, x3 + 131383, 0) |
[U23#(x1)] | = | 0 |
[U84(x1, x2, x3)] | = | max(x2 + 115764, x3 + 0, 0) |
[U23(x1)] | = | 0 |
[U35(x1, x2)] | = | max(x1 + 16023, 0) |
[U72(x1, x2)] | = | max(x2 + 0, 0) |
[U13#(x1, x2, x3)] | = | max(x1 + 28946, x2 + 0, x3 + 28945, 0) |
[U34(x1, x2, x3)] | = | max(x2 + 16023, x3 + 2, 0) |
[U103#(x1, x2, x3)] | = | max(x2 + 102442, x3 + 131383, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 86827, x2 + 86826, 0) |
[U33#(x1, x2, x3)] | = | max(x1 + 44561, x2 + 44561, x3 + 44562, 0) |
[x(x1, x2)] | = | max(x1 + 131383, x2 + 102442, 0) |
[U16#(x1)] | = | 0 |
[n__s(x1)] | = | x1 + 0 |
[U104(x1, x2, x3)] | = | max(x1 + 102441, x2 + 102442, x3 + 131383, 0) |
[U42#(x1)] | = | 0 |
[U12#(x1, x2, x3)] | = | max(x1 + 57885, x2 + 0, x3 + 57886, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x2 + 115764, x3 + 0, 0) |
[0] | = | 0 |
[U14#(x1, x2, x3)] | = | max(x1 + 4, x2 + 0, x3 + 28945, 0) |
[U36#(x1)] | = | 0 |
[U36(x1)] | = | 1 |
[U102#(x1, x2, x3)] | = | max(x1 + 102443, x2 + 102442, x3 + 131383, 0) |
[x#(x1, x2)] | = | max(x1 + 131383, x2 + 102442, 0) |
[s#(x1)] | = | 0 |
[U62(x1)] | = | 0 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 115764, 0) |
[U15#(x1, x2)] | = | max(x2 + 3, 0) |
[U32(x1, x2, x3)] | = | max(x1 + 25984, 0) |
[U33(x1, x2, x3)] | = | max(x1 + 1, 0) |
[n__0] | = | 0 |
[U34#(x1, x2, x3)] | = | max(x1 + 15621, x2 + 15621, x3 + 15621, 0) |
[U14(x1, x2, x3)] | = | max(x1 + 57888, x2 + 86828, 0) |
[isNat(x1)] | = | x1 + 0 |
[n__x(x1, x2)] | = | max(x1 + 131383, x2 + 102442, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 115764, 0) |
[U15(x1, x2)] | = | max(x1 + 86829, 0) |
[U61(x1, x2)] | = | max(0) |
[U51#(x1)] | = | 0 |
[U11#(x1, x2, x3)] | = | max(x1 + 86824, x2 + 0, x3 + 86825, 0) |
[U31(x1, x2, x3)] | = | max(x1 + 27570, 0) |
[U92(x1)] | = | 0 |
[U41#(x1, x2)] | = | max(x1 + 12701, x2 + 115763, 0) |
[U102(x1, x2, x3)] | = | max(x1 + 102442, x2 + 102442, x3 + 131383, 0) |
[U21#(x1, x2)] | = | max(x2 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x2 + 115764, x3 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 625, x2 + 115764, x3 + 0, 0) |
[U22#(x1, x2)] | = | max(x2 + 0, 0) |
[tt] | = | 0 |
[U84#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U71#(x1, x2)] | = | max(x2 + 0, 0) |
[U13(x1, x2, x3)] | = | max(x1 + 57888, x2 + 86827, 0) |
[U22(x1, x2)] | = | max(x2 + 46740, 0) |
[U51(x1)] | = | x1 + 0 |
[isNatKind#(x1)] | = | x1 + 0 |
[U41(x1, x2)] | = | max(0) |
[U31#(x1, x2, x3)] | = | max(x1 + 102442, x2 + 102441, x3 + 102441, 0) |
[U91#(x1, x2)] | = | max(x2 + 66289, 0) |
[U61#(x1, x2)] | = | max(x1 + 73501, x2 + 31250, 0) |
activate(n__plus(X1,X2)) | → | plus(X1,X2) | (50) |
U104(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
U101(tt,M,N) | → | U102(isNatKind(activate(M)),activate(M),activate(N)) | (1) |
U103(tt,M,N) | → | U104(isNatKind(activate(N)),activate(M),activate(N)) | (3) |
U42(tt) | → | tt | (21) |
U72(tt,N) | → | activate(N) | (26) |
U92(tt) | → | 0 | (32) |
U81(tt,M,N) | → | U82(isNatKind(activate(M)),activate(M),activate(N)) | (27) |
U51(tt) | → | tt | (22) |
U82(tt,M,N) | → | U83(isNat(activate(N)),activate(M),activate(N)) | (28) |
x(N,s(M)) | → | U101(isNat(M),M,N) | (44) |
isNatKind(n__s(V1)) | → | U51(isNatKind(activate(V1))) | (39) |
U41(tt,V2) | → | U42(isNatKind(activate(V2))) | (20) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
activate(n__0) | → | 0 | (49) |
activate(n__x(X1,X2)) | → | x(X1,X2) | (52) |
U84(tt,M,N) | → | s(plus(activate(N),activate(M))) | (30) |
U91(tt,N) | → | U92(isNatKind(activate(N))) | (31) |
0 | → | n__0 | (45) |
U61(tt,V2) | → | U62(isNatKind(activate(V2))) | (23) |
U62(tt) | → | tt | (24) |
activate(n__s(X)) | → | s(X) | (51) |
isNatKind(n__x(V1,V2)) | → | U61(isNatKind(activate(V1)),activate(V2)) | (40) |
isNatKind(n__plus(V1,V2)) | → | U41(isNatKind(activate(V1)),activate(V2)) | (38) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(X) | → | X | (53) |
s(X) | → | n__s(X) | (47) |
isNatKind(n__0) | → | tt | (37) |
plus(N,0) | → | U71(isNat(N),N) | (41) |
plus(N,s(M)) | → | U81(isNat(M),M,N) | (42) |
plus(X1,X2) | → | n__plus(X1,X2) | (46) |
U83(tt,M,N) | → | U84(isNatKind(activate(N)),activate(M),activate(N)) | (29) |
x(N,0) | → | U91(isNat(N),N) | (43) |
U102(tt,M,N) | → | U103(isNat(activate(N)),activate(M),activate(N)) | (2) |
U32#(tt,V1,V2) | → | U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (129) |
isNat#(n__x(V1,V2)) | → | activate#(V1) | (92) |
U91#(tt,N) | → | activate#(N) | (176) |
U32#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (128) |
U31#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (125) |
U91#(tt,N) | → | isNatKind#(activate(N)) | (126) |
U102#(tt,M,N) | → | activate#(M) | (174) |
isNatKind#(n__x(V1,V2)) | → | U61#(isNatKind(activate(V1)),activate(V2)) | (124) |
isNat#(n__x(V1,V2)) | → | isNatKind#(activate(V1)) | (122) |
U34#(tt,V1,V2) | → | activate#(V2) | (172) |
U33#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (120) |
U32#(tt,V1,V2) | → | activate#(V2) | (118) |
isNatKind#(n__x(V1,V2)) | → | isNatKind#(activate(V1)) | (114) |
U101#(tt,M,N) | → | isNatKind#(activate(M)) | (171) |
U35#(tt,V2) | → | isNat#(activate(V2)) | (170) |
U34#(tt,V1,V2) | → | activate#(V1) | (112) |
U31#(tt,V1,V2) | → | activate#(V1) | (73) |
U101#(tt,M,N) | → | activate#(N) | (168) |
U103#(tt,M,N) | → | activate#(M) | (108) |
U14#(tt,V1,V2) | → | activate#(V2) | (106) |
U11#(tt,V1,V2) | → | activate#(V2) | (107) |
U13#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (104) |
U102#(tt,M,N) | → | activate#(N) | (140) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V2) | (102) |
isNat#(n__x(V1,V2)) | → | activate#(V2) | (100) |
isNatKind#(n__plus(V1,V2)) | → | U41#(isNatKind(activate(V1)),activate(V2)) | (163) |
U15#(tt,V2) | → | isNat#(activate(V2)) | (162) |
U32#(tt,V1,V2) | → | activate#(V2) | (118) |
U41#(tt,V2) | → | activate#(V2) | (161) |
U101#(tt,M,N) | → | activate#(M) | (76) |
U34#(tt,V1,V2) | → | isNat#(activate(V1)) | (159) |
isNat#(n__x(V1,V2)) | → | U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (157) |
U12#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (158) |
isNat#(n__x(V1,V2)) | → | activate#(V1) | (92) |
U31#(tt,V1,V2) | → | U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (93) |
U14#(tt,V1,V2) | → | U15#(isNat(activate(V1)),activate(V2)) | (154) |
isNatKind#(n__x(V1,V2)) | → | activate#(V1) | (152) |
U41#(tt,V2) | → | isNatKind#(activate(V2)) | (90) |
U32#(tt,V1,V2) | → | activate#(V1) | (88) |
U31#(tt,V1,V2) | → | activate#(V2) | (89) |
U103#(tt,M,N) | → | activate#(N) | (134) |
U33#(tt,V1,V2) | → | U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (87) |
x#(N,0) | → | U91#(isNat(N),N) | (85) |
U35#(tt,V2) | → | activate#(V2) | (149) |
U103#(tt,M,N) | → | isNatKind#(activate(N)) | (84) |
U104#(tt,M,N) | → | activate#(M) | (148) |
U12#(tt,V1,V2) | → | activate#(V2) | (57) |
U104#(tt,M,N) | → | activate#(N) | (80) |
U33#(tt,V1,V2) | → | activate#(V1) | (81) |
U33#(tt,V1,V2) | → | activate#(V2) | (67) |
U101#(tt,M,N) | → | activate#(M) | (76) |
U13#(tt,V1,V2) | → | activate#(V2) | (71) |
U31#(tt,V1,V2) | → | activate#(V1) | (73) |
U13#(tt,V1,V2) | → | activate#(V2) | (71) |
U61#(tt,V2) | → | activate#(V2) | (141) |
U102#(tt,M,N) | → | activate#(N) | (140) |
U33#(tt,V1,V2) | → | activate#(V2) | (67) |
U34#(tt,V1,V2) | → | U35#(isNat(activate(V1)),activate(V2)) | (68) |
U15#(tt,V2) | → | activate#(V2) | (66) |
isNatKind#(n__x(V1,V2)) | → | activate#(V2) | (137) |
U103#(tt,M,N) | → | activate#(N) | (134) |
isNat#(n__plus(V1,V2)) | → | activate#(V2) | (135) |
U104#(tt,M,N) | → | activate#(N) | (80) |
x#(N,s(M)) | → | isNat#(M) | (59) |
x#(N,0) | → | isNat#(N) | (132) |
U12#(tt,V1,V2) | → | activate#(V2) | (57) |
U61#(tt,V2) | → | isNatKind#(activate(V2)) | (56) |
U102#(tt,M,N) | → | isNat#(activate(N)) | (54) |
The dependency pairs are split into 1 component.
activate#(n__plus(X1,X2)) | → | plus#(X1,X2) | (74) |
U104#(tt,M,N) | → | x#(activate(N),activate(M)) | (156) |
U104#(tt,M,N) | → | plus#(x(activate(N),activate(M)),activate(N)) | (103) |
U14#(tt,V1,V2) | → | activate#(V1) | (144) |
U14#(tt,V1,V2) | → | isNat#(activate(V1)) | (131) |
U101#(tt,M,N) | → | U102#(isNatKind(activate(M)),activate(M),activate(N)) | (139) |
U103#(tt,M,N) | → | U104#(isNatKind(activate(N)),activate(M),activate(N)) | (63) |
U72#(tt,N) | → | activate#(N) | (175) |
U81#(tt,M,N) | → | activate#(N) | (97) |
U81#(tt,M,N) | → | activate#(M) | (69) |
U81#(tt,M,N) | → | activate#(M) | (69) |
U81#(tt,M,N) | → | isNatKind#(activate(M)) | (64) |
U81#(tt,M,N) | → | U82#(isNatKind(activate(M)),activate(M),activate(N)) | (101) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (70) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (70) |
isNat#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (91) |
isNat#(n__plus(V1,V2)) | → | U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (117) |
U82#(tt,M,N) | → | activate#(N) | (55) |
U82#(tt,M,N) | → | activate#(M) | (147) |
U82#(tt,M,N) | → | activate#(N) | (55) |
U82#(tt,M,N) | → | isNat#(activate(N)) | (160) |
U82#(tt,M,N) | → | U83#(isNat(activate(N)),activate(M),activate(N)) | (146) |
x#(N,s(M)) | → | U101#(isNat(M),M,N) | (119) |
U11#(tt,V1,V2) | → | activate#(V1) | (115) |
U11#(tt,V1,V2) | → | activate#(V1) | (115) |
U11#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (109) |
U11#(tt,V1,V2) | → | U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (165) |
isNatKind#(n__s(V1)) | → | activate#(V1) | (99) |
isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | (77) |
U13#(tt,V1,V2) | → | activate#(V1) | (138) |
U13#(tt,V1,V2) | → | U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (111) |
U71#(tt,N) | → | activate#(N) | (136) |
U71#(tt,N) | → | activate#(N) | (136) |
U71#(tt,N) | → | isNatKind#(activate(N)) | (155) |
U71#(tt,N) | → | U72#(isNatKind(activate(N)),activate(N)) | (123) |
activate#(n__x(X1,X2)) | → | x#(X1,X2) | (150) |
U84#(tt,M,N) | → | activate#(M) | (86) |
U84#(tt,M,N) | → | activate#(N) | (79) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (98) |
U22#(tt,V1) | → | activate#(V1) | (72) |
U22#(tt,V1) | → | isNat#(activate(V1)) | (61) |
U21#(tt,V1) | → | activate#(V1) | (65) |
U21#(tt,V1) | → | activate#(V1) | (65) |
U21#(tt,V1) | → | isNatKind#(activate(V1)) | (133) |
U21#(tt,V1) | → | U22#(isNatKind(activate(V1)),activate(V1)) | (83) |
U12#(tt,V1,V2) | → | activate#(V1) | (142) |
U12#(tt,V1,V2) | → | U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (127) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V1) | (105) |
isNatKind#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (143) |
plus#(N,0) | → | isNat#(N) | (130) |
plus#(N,0) | → | U71#(isNat(N),N) | (153) |
plus#(N,s(M)) | → | isNat#(M) | (177) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (151) |
isNat#(n__s(V1)) | → | activate#(V1) | (164) |
isNat#(n__s(V1)) | → | activate#(V1) | (164) |
isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | (121) |
isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)),activate(V1)) | (94) |
U83#(tt,M,N) | → | activate#(N) | (113) |
U83#(tt,M,N) | → | activate#(M) | (96) |
U83#(tt,M,N) | → | activate#(N) | (113) |
U83#(tt,M,N) | → | isNatKind#(activate(N)) | (95) |
U83#(tt,M,N) | → | U84#(isNatKind(activate(N)),activate(M),activate(N)) | (169) |
U102#(tt,M,N) | → | U103#(isNat(activate(N)),activate(M),activate(N)) | (166) |
[0#] | = | 0 |
[U72#(x1, x2)] | = | max(x2 + 0, 0) |
[U32#(x1, x2, x3)] | = | max(0) |
[isNatKind(x1)] | = | 5 |
[U16(x1)] | = | 84699 |
[U21(x1, x2)] | = | max(x2 + 1374, 0) |
[U83#(x1, x2, x3)] | = | max(x2 + 6, x3 + 0, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 15999, x2 + 16001, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | x1 + 0 |
[U42(x1)] | = | 3 |
[U91(x1, x2)] | = | max(x2 + 3, 0) |
[U35#(x1, x2)] | = | max(0) |
[U101#(x1, x2, x3)] | = | max(x2 + 1, x3 + 10, 0) |
[activate(x1)] | = | x1 + 0 |
[U82#(x1, x2, x3)] | = | max(x1 + 0, x2 + 6, x3 + 0, 0) |
[U104#(x1, x2, x3)] | = | max(x1 + 4, x2 + 1, x3 + 10, 0) |
[U71(x1, x2)] | = | max(x2 + 0, 0) |
[U81#(x1, x2, x3)] | = | max(x2 + 6, x3 + 0, 0) |
[U92#(x1)] | = | 0 |
[plus#(x1, x2)] | = | max(x1 + 0, x2 + 6, 0) |
[U101(x1, x2, x3)] | = | max(x2 + 1, x3 + 10, 0) |
[activate#(x1)] | = | x1 + 0 |
[U103(x1, x2, x3)] | = | max(x2 + 1, x3 + 10, 0) |
[U23#(x1)] | = | 0 |
[U84(x1, x2, x3)] | = | max(x2 + 10, x3 + 0, 0) |
[U23(x1)] | = | 2 |
[U35(x1, x2)] | = | max(x1 + 9, 0) |
[U72(x1, x2)] | = | max(x2 + 0, 0) |
[U13#(x1, x2, x3)] | = | max(x1 + 2, x2 + 0, 0) |
[U34(x1, x2, x3)] | = | max(x1 + 6, x2 + 10, x3 + 9, 0) |
[U103#(x1, x2, x3)] | = | max(x2 + 1, x3 + 10, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 15997, x3 + 16003, 0) |
[U33#(x1, x2, x3)] | = | max(0) |
[x(x1, x2)] | = | max(x1 + 10, x2 + 1, 0) |
[U16#(x1)] | = | 0 |
[n__s(x1)] | = | x1 + 0 |
[U104(x1, x2, x3)] | = | max(x1 + 3, x2 + 1, x3 + 10, 0) |
[U42#(x1)] | = | 0 |
[U12#(x1, x2, x3)] | = | max(x1 + 4, x2 + 0, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x2 + 10, x3 + 0, 0) |
[0] | = | 1 |
[U14#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, 0) |
[U36#(x1)] | = | 0 |
[U36(x1)] | = | x1 + 0 |
[U102#(x1, x2, x3)] | = | max(x2 + 1, x3 + 10, 0) |
[x#(x1, x2)] | = | max(x1 + 10, x2 + 1, 0) |
[s#(x1)] | = | 0 |
[U62(x1)] | = | 3 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 10, 0) |
[U15#(x1, x2)] | = | max(0) |
[U32(x1, x2, x3)] | = | max(x1 + 6, 0) |
[U33(x1, x2, x3)] | = | max(x1 + 5, x2 + 10, x3 + 11, 0) |
[n__0] | = | 1 |
[U34#(x1, x2, x3)] | = | max(0) |
[U14(x1, x2, x3)] | = | max(x1 + 84694, 0) |
[isNat(x1)] | = | x1 + 1 |
[n__x(x1, x2)] | = | max(x1 + 10, x2 + 1, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 10, 0) |
[U15(x1, x2)] | = | max(x1 + 86828, x2 + 84698, 0) |
[U61(x1, x2)] | = | max(x1 + 0, 0) |
[U51#(x1)] | = | 0 |
[U11#(x1, x2, x3)] | = | max(x1 + 5, x2 + 0, x3 + 9, 0) |
[U31(x1, x2, x3)] | = | max(x1 + 7, 0) |
[U92(x1)] | = | 1 |
[U41#(x1, x2)] | = | max(0) |
[U102(x1, x2, x3)] | = | max(x2 + 1, x3 + 10, 0) |
[U21#(x1, x2)] | = | max(x2 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x2 + 10, x3 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 2, x2 + 10, x3 + 0, 0) |
[U22#(x1, x2)] | = | max(x2 + 0, 0) |
[tt] | = | 3 |
[U84#(x1, x2, x3)] | = | max(x2 + 6, x3 + 0, 0) |
[U71#(x1, x2)] | = | max(x2 + 0, 0) |
[U13(x1, x2, x3)] | = | max(x1 + 15999, x2 + 84698, 0) |
[U22(x1, x2)] | = | max(x2 + 1, 0) |
[U51(x1)] | = | 3 |
[isNatKind#(x1)] | = | x1 + 0 |
[U41(x1, x2)] | = | max(x1 + 0, 0) |
[U31#(x1, x2, x3)] | = | max(0) |
[U91#(x1, x2)] | = | max(0) |
[U61#(x1, x2)] | = | max(0) |
activate(n__plus(X1,X2)) | → | plus(X1,X2) | (50) |
U104(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
U101(tt,M,N) | → | U102(isNatKind(activate(M)),activate(M),activate(N)) | (1) |
U103(tt,M,N) | → | U104(isNatKind(activate(N)),activate(M),activate(N)) | (3) |
U42(tt) | → | tt | (21) |
U72(tt,N) | → | activate(N) | (26) |
U92(tt) | → | 0 | (32) |
U81(tt,M,N) | → | U82(isNatKind(activate(M)),activate(M),activate(N)) | (27) |
U51(tt) | → | tt | (22) |
U82(tt,M,N) | → | U83(isNat(activate(N)),activate(M),activate(N)) | (28) |
x(N,s(M)) | → | U101(isNat(M),M,N) | (44) |
isNatKind(n__s(V1)) | → | U51(isNatKind(activate(V1))) | (39) |
U41(tt,V2) | → | U42(isNatKind(activate(V2))) | (20) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
activate(n__0) | → | 0 | (49) |
activate(n__x(X1,X2)) | → | x(X1,X2) | (52) |
U84(tt,M,N) | → | s(plus(activate(N),activate(M))) | (30) |
U91(tt,N) | → | U92(isNatKind(activate(N))) | (31) |
0 | → | n__0 | (45) |
U61(tt,V2) | → | U62(isNatKind(activate(V2))) | (23) |
U62(tt) | → | tt | (24) |
activate(n__s(X)) | → | s(X) | (51) |
isNatKind(n__x(V1,V2)) | → | U61(isNatKind(activate(V1)),activate(V2)) | (40) |
isNatKind(n__plus(V1,V2)) | → | U41(isNatKind(activate(V1)),activate(V2)) | (38) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(X) | → | X | (53) |
s(X) | → | n__s(X) | (47) |
isNatKind(n__0) | → | tt | (37) |
plus(N,0) | → | U71(isNat(N),N) | (41) |
plus(N,s(M)) | → | U81(isNat(M),M,N) | (42) |
plus(X1,X2) | → | n__plus(X1,X2) | (46) |
U83(tt,M,N) | → | U84(isNatKind(activate(N)),activate(M),activate(N)) | (29) |
x(N,0) | → | U91(isNat(N),N) | (43) |
U102(tt,M,N) | → | U103(isNat(activate(N)),activate(M),activate(N)) | (2) |
U81#(tt,M,N) | → | activate#(M) | (69) |
U81#(tt,M,N) | → | activate#(M) | (69) |
U81#(tt,M,N) | → | isNatKind#(activate(M)) | (64) |
U82#(tt,M,N) | → | activate#(M) | (147) |
U84#(tt,M,N) | → | activate#(M) | (86) |
plus#(N,s(M)) | → | isNat#(M) | (177) |
U83#(tt,M,N) | → | activate#(M) | (96) |
The dependency pairs are split into 1 component.
activate#(n__plus(X1,X2)) | → | plus#(X1,X2) | (74) |
U104#(tt,M,N) | → | x#(activate(N),activate(M)) | (156) |
U104#(tt,M,N) | → | plus#(x(activate(N),activate(M)),activate(N)) | (103) |
U14#(tt,V1,V2) | → | activate#(V1) | (144) |
U14#(tt,V1,V2) | → | isNat#(activate(V1)) | (131) |
U101#(tt,M,N) | → | U102#(isNatKind(activate(M)),activate(M),activate(N)) | (139) |
U103#(tt,M,N) | → | U104#(isNatKind(activate(N)),activate(M),activate(N)) | (63) |
U72#(tt,N) | → | activate#(N) | (175) |
U81#(tt,M,N) | → | activate#(N) | (97) |
U81#(tt,M,N) | → | U82#(isNatKind(activate(M)),activate(M),activate(N)) | (101) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (70) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (70) |
isNat#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (91) |
isNat#(n__plus(V1,V2)) | → | U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (117) |
U82#(tt,M,N) | → | activate#(N) | (55) |
U82#(tt,M,N) | → | activate#(N) | (55) |
U82#(tt,M,N) | → | isNat#(activate(N)) | (160) |
U82#(tt,M,N) | → | U83#(isNat(activate(N)),activate(M),activate(N)) | (146) |
x#(N,s(M)) | → | U101#(isNat(M),M,N) | (119) |
U11#(tt,V1,V2) | → | activate#(V1) | (115) |
U11#(tt,V1,V2) | → | activate#(V1) | (115) |
U11#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (109) |
U11#(tt,V1,V2) | → | U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (165) |
isNatKind#(n__s(V1)) | → | activate#(V1) | (99) |
isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | (77) |
U13#(tt,V1,V2) | → | activate#(V1) | (138) |
U13#(tt,V1,V2) | → | U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (111) |
U71#(tt,N) | → | activate#(N) | (136) |
U71#(tt,N) | → | activate#(N) | (136) |
U71#(tt,N) | → | isNatKind#(activate(N)) | (155) |
U71#(tt,N) | → | U72#(isNatKind(activate(N)),activate(N)) | (123) |
activate#(n__x(X1,X2)) | → | x#(X1,X2) | (150) |
U84#(tt,M,N) | → | activate#(N) | (79) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (98) |
U22#(tt,V1) | → | activate#(V1) | (72) |
U22#(tt,V1) | → | isNat#(activate(V1)) | (61) |
U21#(tt,V1) | → | activate#(V1) | (65) |
U21#(tt,V1) | → | activate#(V1) | (65) |
U21#(tt,V1) | → | isNatKind#(activate(V1)) | (133) |
U21#(tt,V1) | → | U22#(isNatKind(activate(V1)),activate(V1)) | (83) |
U12#(tt,V1,V2) | → | activate#(V1) | (142) |
U12#(tt,V1,V2) | → | U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (127) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V1) | (105) |
isNatKind#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (143) |
plus#(N,0) | → | isNat#(N) | (130) |
plus#(N,0) | → | U71#(isNat(N),N) | (153) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (151) |
isNat#(n__s(V1)) | → | activate#(V1) | (164) |
isNat#(n__s(V1)) | → | activate#(V1) | (164) |
isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | (121) |
isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)),activate(V1)) | (94) |
U83#(tt,M,N) | → | activate#(N) | (113) |
U83#(tt,M,N) | → | activate#(N) | (113) |
U83#(tt,M,N) | → | isNatKind#(activate(N)) | (95) |
U83#(tt,M,N) | → | U84#(isNatKind(activate(N)),activate(M),activate(N)) | (169) |
U102#(tt,M,N) | → | U103#(isNat(activate(N)),activate(M),activate(N)) | (166) |
π(U16) | = | 1 |
π(U11) | = | 1 |
π(activate) | = | 1 |
π(U71) | = | 2 |
π(U92#) | = | 1 |
π(activate#) | = | 1 |
π(U23) | = | 1 |
π(U35) | = | 1 |
π(U72) | = | 2 |
π(U34) | = | 1 |
π(U12) | = | 1 |
π(U36) | = | 1 |
π(U62) | = | 1 |
π(U34#) | = | 2 |
π(U15) | = | 1 |
π(U61) | = | 1 |
π(U51#) | = | 1 |
π(U31) | = | 1 |
π(U13) | = | 1 |
π(U51) | = | 1 |
π(isNatKind#) | = | 1 |
π(U41) | = | 1 |
π(U61#) | = | 2 |
prec(0#) | = | 0 | status(0#) | = | [] | list-extension(0#) | = | Lex | ||
prec(U72#) | = | 0 | status(U72#) | = | [2] | list-extension(U72#) | = | Lex | ||
prec(U32#) | = | 0 | status(U32#) | = | [3, 2, 1] | list-extension(U32#) | = | Lex | ||
prec(isNatKind) | = | 6 | status(isNatKind) | = | [] | list-extension(isNatKind) | = | Lex | ||
prec(U21) | = | 6 | status(U21) | = | [] | list-extension(U21) | = | Lex | ||
prec(U83#) | = | 5 | status(U83#) | = | [3] | list-extension(U83#) | = | Lex | ||
prec(s) | = | 8 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(isNat#) | = | 2 | status(isNat#) | = | [1] | list-extension(isNat#) | = | Lex | ||
prec(U42) | = | 6 | status(U42) | = | [] | list-extension(U42) | = | Lex | ||
prec(U91) | = | 6 | status(U91) | = | [] | list-extension(U91) | = | Lex | ||
prec(U35#) | = | 0 | status(U35#) | = | [] | list-extension(U35#) | = | Lex | ||
prec(U101#) | = | 10 | status(U101#) | = | [2, 3, 1] | list-extension(U101#) | = | Lex | ||
prec(U82#) | = | 5 | status(U82#) | = | [3] | list-extension(U82#) | = | Lex | ||
prec(U104#) | = | 10 | status(U104#) | = | [2, 3, 1] | list-extension(U104#) | = | Lex | ||
prec(U81#) | = | 5 | status(U81#) | = | [3] | list-extension(U81#) | = | Lex | ||
prec(plus#) | = | 5 | status(plus#) | = | [1] | list-extension(plus#) | = | Lex | ||
prec(U101) | = | 10 | status(U101) | = | [2, 3, 1] | list-extension(U101) | = | Lex | ||
prec(U103) | = | 10 | status(U103) | = | [2, 3, 1] | list-extension(U103) | = | Lex | ||
prec(U23#) | = | 0 | status(U23#) | = | [] | list-extension(U23#) | = | Lex | ||
prec(U84) | = | 9 | status(U84) | = | [2, 3, 1] | list-extension(U84) | = | Lex | ||
prec(U13#) | = | 4 | status(U13#) | = | [2, 3] | list-extension(U13#) | = | Lex | ||
prec(U103#) | = | 10 | status(U103#) | = | [2, 3, 1] | list-extension(U103#) | = | Lex | ||
prec(U33#) | = | 0 | status(U33#) | = | [2, 1] | list-extension(U33#) | = | Lex | ||
prec(x) | = | 10 | status(x) | = | [2, 1] | list-extension(x) | = | Lex | ||
prec(U16#) | = | 0 | status(U16#) | = | [] | list-extension(U16#) | = | Lex | ||
prec(n__s) | = | 8 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(U104) | = | 10 | status(U104) | = | [2, 3, 1] | list-extension(U104) | = | Lex | ||
prec(U42#) | = | 0 | status(U42#) | = | [] | list-extension(U42#) | = | Lex | ||
prec(U12#) | = | 5 | status(U12#) | = | [2, 3] | list-extension(U12#) | = | Lex | ||
prec(U62#) | = | 0 | status(U62#) | = | [] | list-extension(U62#) | = | Lex | ||
prec(U83) | = | 9 | status(U83) | = | [2, 3, 1] | list-extension(U83) | = | Lex | ||
prec(0) | = | 6 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(U14#) | = | 3 | status(U14#) | = | [2] | list-extension(U14#) | = | Lex | ||
prec(U36#) | = | 0 | status(U36#) | = | [] | list-extension(U36#) | = | Lex | ||
prec(U102#) | = | 10 | status(U102#) | = | [2, 3, 1] | list-extension(U102#) | = | Lex | ||
prec(x#) | = | 10 | status(x#) | = | [2, 1] | list-extension(x#) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(n__plus) | = | 9 | status(n__plus) | = | [2, 1] | list-extension(n__plus) | = | Lex | ||
prec(U15#) | = | 0 | status(U15#) | = | [] | list-extension(U15#) | = | Lex | ||
prec(U32) | = | 6 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(U33) | = | 6 | status(U33) | = | [] | list-extension(U33) | = | Lex | ||
prec(n__0) | = | 6 | status(n__0) | = | [] | list-extension(n__0) | = | Lex | ||
prec(U14) | = | 6 | status(U14) | = | [] | list-extension(U14) | = | Lex | ||
prec(isNat) | = | 6 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(n__x) | = | 10 | status(n__x) | = | [2, 1] | list-extension(n__x) | = | Lex | ||
prec(plus) | = | 9 | status(plus) | = | [2, 1] | list-extension(plus) | = | Lex | ||
prec(U11#) | = | 6 | status(U11#) | = | [3, 2] | list-extension(U11#) | = | Lex | ||
prec(U92) | = | 6 | status(U92) | = | [] | list-extension(U92) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [1, 2] | list-extension(U41#) | = | Lex | ||
prec(U102) | = | 10 | status(U102) | = | [2, 3, 1] | list-extension(U102) | = | Lex | ||
prec(U21#) | = | 7 | status(U21#) | = | [1, 2] | list-extension(U21#) | = | Lex | ||
prec(U81) | = | 9 | status(U81) | = | [2, 3, 1] | list-extension(U81) | = | Lex | ||
prec(U82) | = | 9 | status(U82) | = | [2, 3, 1] | list-extension(U82) | = | Lex | ||
prec(U22#) | = | 3 | status(U22#) | = | [2] | list-extension(U22#) | = | Lex | ||
prec(tt) | = | 6 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U84#) | = | 5 | status(U84#) | = | [3] | list-extension(U84#) | = | Lex | ||
prec(U71#) | = | 3 | status(U71#) | = | [2] | list-extension(U71#) | = | Lex | ||
prec(U22) | = | 6 | status(U22) | = | [] | list-extension(U22) | = | Lex | ||
prec(U31#) | = | 0 | status(U31#) | = | [2, 1, 3] | list-extension(U31#) | = | Lex | ||
prec(U91#) | = | 0 | status(U91#) | = | [] | list-extension(U91#) | = | Lex |
[0#] | = | 0 |
[U72#(x1, x2)] | = | max(x2 + 0, 0) |
[U32#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | max(0) |
[U83#(x1, x2, x3)] | = | max(x3 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | x1 + 0 |
[U42(x1)] | = | 0 |
[U91(x1, x2)] | = | max(0) |
[U35#(x1, x2)] | = | max(0) |
[U101#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U82#(x1, x2, x3)] | = | max(x3 + 0, 0) |
[U104#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U81#(x1, x2, x3)] | = | max(x3 + 0, 0) |
[plus#(x1, x2)] | = | max(x1 + 0, 0) |
[U101(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U103(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U23#(x1)] | = | 0 |
[U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U13#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U103#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U33#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U16#(x1)] | = | 0 |
[n__s(x1)] | = | x1 + 0 |
[U104(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U42#(x1)] | = | 0 |
[U12#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[0] | = | 0 |
[U14#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U36#(x1)] | = | 0 |
[U102#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[x#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[s#(x1)] | = | 0 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15#(x1, x2)] | = | max(0) |
[U32(x1, x2, x3)] | = | max(0) |
[U33(x1, x2, x3)] | = | max(0) |
[n__0] | = | 0 |
[U14(x1, x2, x3)] | = | max(0) |
[isNat(x1)] | = | 0 |
[n__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U11#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U92(x1)] | = | 0 |
[U41#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U102(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U21#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U22#(x1, x2)] | = | max(x2 + 0, 0) |
[tt] | = | 0 |
[U84#(x1, x2, x3)] | = | max(x3 + 0, 0) |
[U71#(x1, x2)] | = | max(x2 + 0, 0) |
[U22(x1, x2)] | = | max(0) |
[U31#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U91#(x1, x2)] | = | max(0) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
activate(n__plus(X1,X2)) | → | plus(X1,X2) | (50) |
U104(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
U32(tt,V1,V2) | → | U33(isNatKind(activate(V2)),activate(V1),activate(V2)) | (15) |
U14(tt,V1,V2) | → | U15(isNat(activate(V1)),activate(V2)) | (8) |
U101(tt,M,N) | → | U102(isNatKind(activate(M)),activate(M),activate(N)) | (1) |
U103(tt,M,N) | → | U104(isNatKind(activate(N)),activate(M),activate(N)) | (3) |
U33(tt,V1,V2) | → | U34(isNatKind(activate(V2)),activate(V1),activate(V2)) | (16) |
U42(tt) | → | tt | (21) |
isNat(n__x(V1,V2)) | → | U31(isNatKind(activate(V1)),activate(V1),activate(V2)) | (36) |
U72(tt,N) | → | activate(N) | (26) |
U36(tt) | → | tt | (19) |
U92(tt) | → | 0 | (32) |
U34(tt,V1,V2) | → | U35(isNat(activate(V1)),activate(V2)) | (17) |
U81(tt,M,N) | → | U82(isNatKind(activate(M)),activate(M),activate(N)) | (27) |
isNat(n__plus(V1,V2)) | → | U11(isNatKind(activate(V1)),activate(V1),activate(V2)) | (34) |
U51(tt) | → | tt | (22) |
U82(tt,M,N) | → | U83(isNat(activate(N)),activate(M),activate(N)) | (28) |
x(N,s(M)) | → | U101(isNat(M),M,N) | (44) |
U11(tt,V1,V2) | → | U12(isNatKind(activate(V1)),activate(V1),activate(V2)) | (5) |
isNat(n__0) | → | tt | (33) |
U16(tt) | → | tt | (10) |
isNatKind(n__s(V1)) | → | U51(isNatKind(activate(V1))) | (39) |
U13(tt,V1,V2) | → | U14(isNatKind(activate(V2)),activate(V1),activate(V2)) | (7) |
U41(tt,V2) | → | U42(isNatKind(activate(V2))) | (20) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
activate(n__0) | → | 0 | (49) |
activate(n__x(X1,X2)) | → | x(X1,X2) | (52) |
U84(tt,M,N) | → | s(plus(activate(N),activate(M))) | (30) |
U31(tt,V1,V2) | → | U32(isNatKind(activate(V1)),activate(V1),activate(V2)) | (14) |
U91(tt,N) | → | U92(isNatKind(activate(N))) | (31) |
U22(tt,V1) | → | U23(isNat(activate(V1))) | (12) |
0 | → | n__0 | (45) |
U61(tt,V2) | → | U62(isNatKind(activate(V2))) | (23) |
U62(tt) | → | tt | (24) |
U21(tt,V1) | → | U22(isNatKind(activate(V1)),activate(V1)) | (11) |
U15(tt,V2) | → | U16(isNat(activate(V2))) | (9) |
U23(tt) | → | tt | (13) |
activate(n__s(X)) | → | s(X) | (51) |
isNatKind(n__x(V1,V2)) | → | U61(isNatKind(activate(V1)),activate(V2)) | (40) |
U12(tt,V1,V2) | → | U13(isNatKind(activate(V2)),activate(V1),activate(V2)) | (6) |
isNatKind(n__plus(V1,V2)) | → | U41(isNatKind(activate(V1)),activate(V2)) | (38) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(X) | → | X | (53) |
s(X) | → | n__s(X) | (47) |
isNatKind(n__0) | → | tt | (37) |
plus(N,0) | → | U71(isNat(N),N) | (41) |
plus(N,s(M)) | → | U81(isNat(M),M,N) | (42) |
plus(X1,X2) | → | n__plus(X1,X2) | (46) |
isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)),activate(V1)) | (35) |
U83(tt,M,N) | → | U84(isNatKind(activate(N)),activate(M),activate(N)) | (29) |
x(N,0) | → | U91(isNat(N),N) | (43) |
U102(tt,M,N) | → | U103(isNat(activate(N)),activate(M),activate(N)) | (2) |
activate#(n__plus(X1,X2)) | → | plus#(X1,X2) | (74) |
U104#(tt,M,N) | → | x#(activate(N),activate(M)) | (156) |
U104#(tt,M,N) | → | plus#(x(activate(N),activate(M)),activate(N)) | (103) |
U14#(tt,V1,V2) | → | activate#(V1) | (144) |
U14#(tt,V1,V2) | → | isNat#(activate(V1)) | (131) |
U72#(tt,N) | → | activate#(N) | (175) |
U81#(tt,M,N) | → | activate#(N) | (97) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (70) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (70) |
isNat#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (91) |
isNat#(n__plus(V1,V2)) | → | U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (117) |
U82#(tt,M,N) | → | activate#(N) | (55) |
U82#(tt,M,N) | → | activate#(N) | (55) |
U82#(tt,M,N) | → | isNat#(activate(N)) | (160) |
x#(N,s(M)) | → | U101#(isNat(M),M,N) | (119) |
U11#(tt,V1,V2) | → | activate#(V1) | (115) |
U11#(tt,V1,V2) | → | activate#(V1) | (115) |
U11#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (109) |
U11#(tt,V1,V2) | → | U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (165) |
isNatKind#(n__s(V1)) | → | activate#(V1) | (99) |
isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | (77) |
U13#(tt,V1,V2) | → | activate#(V1) | (138) |
U13#(tt,V1,V2) | → | U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (111) |
U71#(tt,N) | → | activate#(N) | (136) |
U71#(tt,N) | → | activate#(N) | (136) |
U71#(tt,N) | → | isNatKind#(activate(N)) | (155) |
U71#(tt,N) | → | U72#(isNatKind(activate(N)),activate(N)) | (123) |
U84#(tt,M,N) | → | activate#(N) | (79) |
U22#(tt,V1) | → | activate#(V1) | (72) |
U22#(tt,V1) | → | isNat#(activate(V1)) | (61) |
U21#(tt,V1) | → | activate#(V1) | (65) |
U21#(tt,V1) | → | activate#(V1) | (65) |
U21#(tt,V1) | → | isNatKind#(activate(V1)) | (133) |
U21#(tt,V1) | → | U22#(isNatKind(activate(V1)),activate(V1)) | (83) |
U12#(tt,V1,V2) | → | activate#(V1) | (142) |
U12#(tt,V1,V2) | → | U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (127) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V1) | (105) |
isNatKind#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (143) |
plus#(N,0) | → | isNat#(N) | (130) |
plus#(N,0) | → | U71#(isNat(N),N) | (153) |
isNat#(n__s(V1)) | → | activate#(V1) | (164) |
isNat#(n__s(V1)) | → | activate#(V1) | (164) |
isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | (121) |
isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)),activate(V1)) | (94) |
U83#(tt,M,N) | → | activate#(N) | (113) |
U83#(tt,M,N) | → | activate#(N) | (113) |
U83#(tt,M,N) | → | isNatKind#(activate(N)) | (95) |
The dependency pairs are split into 1 component.
U81#(tt,M,N) | → | U82#(isNatKind(activate(M)),activate(M),activate(N)) | (101) |
U82#(tt,M,N) | → | U83#(isNat(activate(N)),activate(M),activate(N)) | (146) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (98) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (151) |
U83#(tt,M,N) | → | U84#(isNatKind(activate(N)),activate(M),activate(N)) | (169) |
π(U16) | = | 1 |
π(U11) | = | 1 |
π(activate) | = | 1 |
π(U71) | = | 2 |
π(U92#) | = | 1 |
π(activate#) | = | 1 |
π(U23) | = | 1 |
π(U35) | = | 1 |
π(U72) | = | 2 |
π(U34) | = | 1 |
π(U12) | = | 1 |
π(U36) | = | 1 |
π(U62) | = | 1 |
π(U34#) | = | 2 |
π(U15) | = | 1 |
π(U61) | = | 1 |
π(U51#) | = | 1 |
π(U31) | = | 1 |
π(U13) | = | 1 |
π(U51) | = | 1 |
π(isNatKind#) | = | 1 |
π(U41) | = | 1 |
π(U61#) | = | 2 |
prec(0#) | = | 0 | status(0#) | = | [] | list-extension(0#) | = | Lex | ||
prec(U72#) | = | 0 | status(U72#) | = | [2] | list-extension(U72#) | = | Lex | ||
prec(U32#) | = | 0 | status(U32#) | = | [3, 2, 1] | list-extension(U32#) | = | Lex | ||
prec(isNatKind) | = | 6 | status(isNatKind) | = | [] | list-extension(isNatKind) | = | Lex | ||
prec(U21) | = | 6 | status(U21) | = | [] | list-extension(U21) | = | Lex | ||
prec(U83#) | = | 7 | status(U83#) | = | [2] | list-extension(U83#) | = | Lex | ||
prec(s) | = | 10 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(isNat#) | = | 2 | status(isNat#) | = | [1] | list-extension(isNat#) | = | Lex | ||
prec(U42) | = | 6 | status(U42) | = | [] | list-extension(U42) | = | Lex | ||
prec(U91) | = | 6 | status(U91) | = | [] | list-extension(U91) | = | Lex | ||
prec(U35#) | = | 0 | status(U35#) | = | [] | list-extension(U35#) | = | Lex | ||
prec(U101#) | = | 10 | status(U101#) | = | [2, 3, 1] | list-extension(U101#) | = | Lex | ||
prec(U82#) | = | 8 | status(U82#) | = | [2] | list-extension(U82#) | = | Lex | ||
prec(U104#) | = | 10 | status(U104#) | = | [2, 3, 1] | list-extension(U104#) | = | Lex | ||
prec(U81#) | = | 9 | status(U81#) | = | [2] | list-extension(U81#) | = | Lex | ||
prec(plus#) | = | 4 | status(plus#) | = | [2] | list-extension(plus#) | = | Lex | ||
prec(U101) | = | 12 | status(U101) | = | [2, 3, 1] | list-extension(U101) | = | Lex | ||
prec(U103) | = | 12 | status(U103) | = | [2, 3, 1] | list-extension(U103) | = | Lex | ||
prec(U23#) | = | 0 | status(U23#) | = | [] | list-extension(U23#) | = | Lex | ||
prec(U84) | = | 11 | status(U84) | = | [2, 3, 1] | list-extension(U84) | = | Lex | ||
prec(U13#) | = | 4 | status(U13#) | = | [2, 3] | list-extension(U13#) | = | Lex | ||
prec(U103#) | = | 10 | status(U103#) | = | [2, 3, 1] | list-extension(U103#) | = | Lex | ||
prec(U33#) | = | 0 | status(U33#) | = | [2, 1] | list-extension(U33#) | = | Lex | ||
prec(x) | = | 12 | status(x) | = | [2, 1] | list-extension(x) | = | Lex | ||
prec(U16#) | = | 0 | status(U16#) | = | [] | list-extension(U16#) | = | Lex | ||
prec(n__s) | = | 10 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(U104) | = | 12 | status(U104) | = | [2, 3, 1] | list-extension(U104) | = | Lex | ||
prec(U42#) | = | 0 | status(U42#) | = | [] | list-extension(U42#) | = | Lex | ||
prec(U12#) | = | 5 | status(U12#) | = | [2, 3] | list-extension(U12#) | = | Lex | ||
prec(U62#) | = | 0 | status(U62#) | = | [] | list-extension(U62#) | = | Lex | ||
prec(U83) | = | 11 | status(U83) | = | [2, 3, 1] | list-extension(U83) | = | Lex | ||
prec(0) | = | 6 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(U14#) | = | 3 | status(U14#) | = | [2] | list-extension(U14#) | = | Lex | ||
prec(U36#) | = | 0 | status(U36#) | = | [] | list-extension(U36#) | = | Lex | ||
prec(U102#) | = | 10 | status(U102#) | = | [2, 3, 1] | list-extension(U102#) | = | Lex | ||
prec(x#) | = | 10 | status(x#) | = | [2, 1] | list-extension(x#) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(n__plus) | = | 11 | status(n__plus) | = | [2, 1] | list-extension(n__plus) | = | Lex | ||
prec(U15#) | = | 0 | status(U15#) | = | [] | list-extension(U15#) | = | Lex | ||
prec(U32) | = | 6 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(U33) | = | 6 | status(U33) | = | [] | list-extension(U33) | = | Lex | ||
prec(n__0) | = | 6 | status(n__0) | = | [] | list-extension(n__0) | = | Lex | ||
prec(U14) | = | 6 | status(U14) | = | [] | list-extension(U14) | = | Lex | ||
prec(isNat) | = | 6 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(n__x) | = | 12 | status(n__x) | = | [2, 1] | list-extension(n__x) | = | Lex | ||
prec(plus) | = | 11 | status(plus) | = | [2, 1] | list-extension(plus) | = | Lex | ||
prec(U11#) | = | 6 | status(U11#) | = | [3, 2] | list-extension(U11#) | = | Lex | ||
prec(U92) | = | 6 | status(U92) | = | [] | list-extension(U92) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [1, 2] | list-extension(U41#) | = | Lex | ||
prec(U102) | = | 12 | status(U102) | = | [2, 3, 1] | list-extension(U102) | = | Lex | ||
prec(U21#) | = | 7 | status(U21#) | = | [1, 2] | list-extension(U21#) | = | Lex | ||
prec(U81) | = | 11 | status(U81) | = | [2, 3, 1] | list-extension(U81) | = | Lex | ||
prec(U82) | = | 11 | status(U82) | = | [2, 3, 1] | list-extension(U82) | = | Lex | ||
prec(U22#) | = | 3 | status(U22#) | = | [2] | list-extension(U22#) | = | Lex | ||
prec(tt) | = | 6 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U84#) | = | 5 | status(U84#) | = | [2] | list-extension(U84#) | = | Lex | ||
prec(U71#) | = | 3 | status(U71#) | = | [2] | list-extension(U71#) | = | Lex | ||
prec(U22) | = | 6 | status(U22) | = | [] | list-extension(U22) | = | Lex | ||
prec(U31#) | = | 0 | status(U31#) | = | [2, 1, 3] | list-extension(U31#) | = | Lex | ||
prec(U91#) | = | 0 | status(U91#) | = | [] | list-extension(U91#) | = | Lex |
[0#] | = | 0 |
[U72#(x1, x2)] | = | max(x2 + 0, 0) |
[U32#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[isNatKind(x1)] | = | 0 |
[U21(x1, x2)] | = | max(0) |
[U83#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | x1 + 0 |
[U42(x1)] | = | 0 |
[U91(x1, x2)] | = | max(0) |
[U35#(x1, x2)] | = | max(0) |
[U101#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U82#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U104#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U81#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[plus#(x1, x2)] | = | max(x2 + 0, 0) |
[U101(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U103(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U23#(x1)] | = | 0 |
[U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U13#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U103#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U33#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U16#(x1)] | = | 0 |
[n__s(x1)] | = | x1 + 0 |
[U104(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U42#(x1)] | = | 0 |
[U12#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[0] | = | 0 |
[U14#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U36#(x1)] | = | 0 |
[U102#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[x#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[s#(x1)] | = | 0 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15#(x1, x2)] | = | max(0) |
[U32(x1, x2, x3)] | = | max(0) |
[U33(x1, x2, x3)] | = | max(0) |
[n__0] | = | 0 |
[U14(x1, x2, x3)] | = | max(0) |
[isNat(x1)] | = | 0 |
[n__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U11#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U92(x1)] | = | 0 |
[U41#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U102(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U21#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U22#(x1, x2)] | = | max(x2 + 0, 0) |
[tt] | = | 0 |
[U84#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U71#(x1, x2)] | = | max(x2 + 0, 0) |
[U22(x1, x2)] | = | max(0) |
[U31#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U91#(x1, x2)] | = | max(0) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
activate(n__plus(X1,X2)) | → | plus(X1,X2) | (50) |
U104(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
U32(tt,V1,V2) | → | U33(isNatKind(activate(V2)),activate(V1),activate(V2)) | (15) |
U14(tt,V1,V2) | → | U15(isNat(activate(V1)),activate(V2)) | (8) |
U101(tt,M,N) | → | U102(isNatKind(activate(M)),activate(M),activate(N)) | (1) |
U103(tt,M,N) | → | U104(isNatKind(activate(N)),activate(M),activate(N)) | (3) |
U33(tt,V1,V2) | → | U34(isNatKind(activate(V2)),activate(V1),activate(V2)) | (16) |
U42(tt) | → | tt | (21) |
isNat(n__x(V1,V2)) | → | U31(isNatKind(activate(V1)),activate(V1),activate(V2)) | (36) |
U72(tt,N) | → | activate(N) | (26) |
U36(tt) | → | tt | (19) |
U92(tt) | → | 0 | (32) |
U34(tt,V1,V2) | → | U35(isNat(activate(V1)),activate(V2)) | (17) |
U81(tt,M,N) | → | U82(isNatKind(activate(M)),activate(M),activate(N)) | (27) |
isNat(n__plus(V1,V2)) | → | U11(isNatKind(activate(V1)),activate(V1),activate(V2)) | (34) |
U51(tt) | → | tt | (22) |
U82(tt,M,N) | → | U83(isNat(activate(N)),activate(M),activate(N)) | (28) |
x(N,s(M)) | → | U101(isNat(M),M,N) | (44) |
U11(tt,V1,V2) | → | U12(isNatKind(activate(V1)),activate(V1),activate(V2)) | (5) |
isNat(n__0) | → | tt | (33) |
U16(tt) | → | tt | (10) |
isNatKind(n__s(V1)) | → | U51(isNatKind(activate(V1))) | (39) |
U13(tt,V1,V2) | → | U14(isNatKind(activate(V2)),activate(V1),activate(V2)) | (7) |
U41(tt,V2) | → | U42(isNatKind(activate(V2))) | (20) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
activate(n__0) | → | 0 | (49) |
activate(n__x(X1,X2)) | → | x(X1,X2) | (52) |
U84(tt,M,N) | → | s(plus(activate(N),activate(M))) | (30) |
U31(tt,V1,V2) | → | U32(isNatKind(activate(V1)),activate(V1),activate(V2)) | (14) |
U91(tt,N) | → | U92(isNatKind(activate(N))) | (31) |
U22(tt,V1) | → | U23(isNat(activate(V1))) | (12) |
0 | → | n__0 | (45) |
U61(tt,V2) | → | U62(isNatKind(activate(V2))) | (23) |
U62(tt) | → | tt | (24) |
U21(tt,V1) | → | U22(isNatKind(activate(V1)),activate(V1)) | (11) |
U15(tt,V2) | → | U16(isNat(activate(V2))) | (9) |
U23(tt) | → | tt | (13) |
activate(n__s(X)) | → | s(X) | (51) |
isNatKind(n__x(V1,V2)) | → | U61(isNatKind(activate(V1)),activate(V2)) | (40) |
U12(tt,V1,V2) | → | U13(isNatKind(activate(V2)),activate(V1),activate(V2)) | (6) |
isNatKind(n__plus(V1,V2)) | → | U41(isNatKind(activate(V1)),activate(V2)) | (38) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(X) | → | X | (53) |
s(X) | → | n__s(X) | (47) |
isNatKind(n__0) | → | tt | (37) |
plus(N,0) | → | U71(isNat(N),N) | (41) |
plus(N,s(M)) | → | U81(isNat(M),M,N) | (42) |
plus(X1,X2) | → | n__plus(X1,X2) | (46) |
isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)),activate(V1)) | (35) |
U83(tt,M,N) | → | U84(isNatKind(activate(N)),activate(M),activate(N)) | (29) |
x(N,0) | → | U91(isNat(N),N) | (43) |
U102(tt,M,N) | → | U103(isNat(activate(N)),activate(M),activate(N)) | (2) |
U81#(tt,M,N) | → | U82#(isNatKind(activate(M)),activate(M),activate(N)) | (101) |
U82#(tt,M,N) | → | U83#(isNat(activate(N)),activate(M),activate(N)) | (146) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (98) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (151) |
U83#(tt,M,N) | → | U84#(isNatKind(activate(N)),activate(M),activate(N)) | (169) |
The dependency pairs are split into 0 components.