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(activate(X1),activate(X2)) | (50) |
activate(n__s(X)) | → | s(activate(X)) | (51) |
activate(n__x(X1,X2)) | → | x(activate(X1),activate(X2)) | (52) |
activate(X) | → | X | (53) |
There are 147 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
There are 136 ruless (increase limit for explicit display).
[0#] | = | 0 |
[U72#(x1, x2)] | = | max(x2 + 7069, 0) |
[U32#(x1, x2, x3)] | = | max(x2 + 19905, x3 + 7073, 0) |
[isNatKind(x1)] | = | 1 |
[U16(x1)] | = | 3 |
[U21(x1, x2)] | = | max(x2 + 3, 0) |
[U83#(x1, x2, x3)] | = | max(x1 + 7066, x2 + 18408, x3 + 7069, 0) |
[U11(x1, x2, x3)] | = | max(x2 + 3, x3 + 11338, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | x1 + 7069 |
[U42(x1)] | = | x1 + 0 |
[U91(x1, x2)] | = | max(x1 + 12835, x2 + 12837, 0) |
[U35#(x1, x2)] | = | max(x1 + 7067, x2 + 7070, 0) |
[U101#(x1, x2, x3)] | = | max(x1 + 19905, x2 + 19909, x3 + 19907, 0) |
[activate(x1)] | = | x1 + 0 |
[U82#(x1, x2, x3)] | = | max(x2 + 18408, x3 + 7069, 0) |
[U104#(x1, x2, x3)] | = | max(x2 + 19909, x3 + 19907, 0) |
[U71(x1, x2)] | = | max(x2 + 0, 0) |
[U81#(x1, x2, x3)] | = | max(x1 + 18405, x2 + 18408, x3 + 7069, 0) |
[U92#(x1)] | = | 0 |
[plus#(x1, x2)] | = | max(x1 + 7069, x2 + 18408, 0) |
[U101(x1, x2, x3)] | = | max(x1 + 12836, x2 + 12840, x3 + 12838, 0) |
[activate#(x1)] | = | x1 + 7069 |
[U103(x1, x2, x3)] | = | max(x1 + 12835, x2 + 12840, x3 + 12838, 0) |
[U23#(x1)] | = | 0 |
[U84(x1, x2, x3)] | = | max(x2 + 11339, x3 + 0, 0) |
[U23(x1)] | = | 3 |
[U35(x1, x2)] | = | max(x2 + 3, 0) |
[U72(x1, x2)] | = | max(x2 + 0, 0) |
[U13#(x1, x2, x3)] | = | max(x2 + 7069, x3 + 7072, 0) |
[U34(x1, x2, x3)] | = | max(x3 + 12239, 0) |
[U103#(x1, x2, x3)] | = | max(x2 + 19909, x3 + 19907, 0) |
[U12(x1, x2, x3)] | = | max(x2 + 3, x3 + 11338, 0) |
[U33#(x1, x2, x3)] | = | max(x2 + 7072, x3 + 7072, 0) |
[x(x1, x2)] | = | max(x1 + 12838, x2 + 12840, 0) |
[U16#(x1)] | = | 0 |
[n__s(x1)] | = | x1 + 0 |
[U104(x1, x2, x3)] | = | max(x2 + 12840, x3 + 12838, 0) |
[U42#(x1)] | = | 0 |
[U12#(x1, x2, x3)] | = | max(x2 + 7069, x3 + 7073, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x2 + 11339, x3 + 0, 0) |
[0] | = | 0 |
[U14#(x1, x2, x3)] | = | max(x2 + 7069, x3 + 7071, 0) |
[U36#(x1)] | = | 0 |
[U36(x1)] | = | x1 + 0 |
[U102#(x1, x2, x3)] | = | max(x2 + 19909, x3 + 19907, 0) |
[x#(x1, x2)] | = | max(x1 + 19907, x2 + 19909, 0) |
[s#(x1)] | = | 0 |
[U62(x1)] | = | 2 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 11339, 0) |
[U15#(x1, x2)] | = | max(x1 + 7065, x2 + 7070, 0) |
[U32(x1, x2, x3)] | = | max(x3 + 12239, 0) |
[U33(x1, x2, x3)] | = | max(x3 + 12239, 0) |
[n__0] | = | 0 |
[U34#(x1, x2, x3)] | = | max(x2 + 7071, x3 + 7071, 0) |
[U14(x1, x2, x3)] | = | max(x2 + 3, x3 + 1, 0) |
[isNat(x1)] | = | x1 + 3 |
[n__x(x1, x2)] | = | max(x1 + 12838, x2 + 12840, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 11339, 0) |
[U15(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[U61(x1, x2)] | = | max(x1 + 1, 0) |
[U51#(x1)] | = | 0 |
[U11#(x1, x2, x3)] | = | max(x2 + 7069, x3 + 7073, 0) |
[U31(x1, x2, x3)] | = | max(x3 + 12239, 0) |
[U92(x1)] | = | 12838 |
[U41#(x1, x2)] | = | max(x2 + 7070, 0) |
[U102(x1, x2, x3)] | = | max(x2 + 12840, x3 + 12838, 0) |
[U21#(x1, x2)] | = | max(x2 + 7069, 0) |
[U81(x1, x2, x3)] | = | max(x2 + 11339, x3 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x2 + 11339, x3 + 0, 0) |
[U22#(x1, x2)] | = | max(x2 + 7069, 0) |
[tt] | = | 3 |
[U84#(x1, x2, x3)] | = | max(x2 + 18408, x3 + 7069, 0) |
[U71#(x1, x2)] | = | max(x1 + 7065, x2 + 7069, 0) |
[U13(x1, x2, x3)] | = | max(x2 + 3, x3 + 11338, 0) |
[U22(x1, x2)] | = | max(x2 + 3, 0) |
[U51(x1)] | = | 2 |
[isNatKind#(x1)] | = | x1 + 7069 |
[U41(x1, x2)] | = | max(x1 + 15620, x2 + 31251, 0) |
[U31#(x1, x2, x3)] | = | max(x2 + 19906, x3 + 7074, 0) |
[U91#(x1, x2)] | = | max(x2 + 7070, 0) |
[U61#(x1, x2)] | = | max(x2 + 7070, 0) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
activate(n__plus(X1,X2)) | → | plus(activate(X1),activate(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) |
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) |
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) |
U13(tt,V1,V2) | → | U14(isNatKind(activate(V2)),activate(V1),activate(V2)) | (7) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
activate(n__0) | → | 0 | (49) |
activate(n__x(X1,X2)) | → | x(activate(X1),activate(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) |
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(activate(X)) | (51) |
U12(tt,V1,V2) | → | U13(isNatKind(activate(V2)),activate(V1),activate(V2)) | (6) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(X) | → | X | (53) |
s(X) | → | n__s(X) | (47) |
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) |
plus#(N,s(M)) | → | isNat#(M) | (182) |
isNat#(n__x(V1,V2)) | → | U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (129) |
U91#(tt,N) | → | isNatKind#(activate(N)) | (181) |
U34#(tt,V1,V2) | → | activate#(V1) | (179) |
U31#(tt,V1,V2) | → | U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (125) |
U102#(tt,M,N) | → | activate#(M) | (178) |
activate#(n__x(X1,X2)) | → | activate#(X1) | (123) |
isNatKind#(n__x(V1,V2)) | → | U61#(isNatKind(activate(V1)),activate(V2)) | (124) |
U34#(tt,V1,V2) | → | isNat#(activate(V1)) | (177) |
U34#(tt,V1,V2) | → | U35#(isNat(activate(V1)),activate(V2)) | (176) |
isNat#(n__x(V1,V2)) | → | activate#(V1) | (89) |
U32#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (120) |
U31#(tt,V1,V2) | → | activate#(V2) | (119) |
isNatKind#(n__x(V1,V2)) | → | isNatKind#(activate(V1)) | (117) |
U103#(tt,M,N) | → | activate#(M) | (174) |
U104#(tt,M,N) | → | activate#(N) | (75) |
isNat#(n__plus(V1,V2)) | → | activate#(V2) | (113) |
U61#(tt,V2) | → | activate#(V2) | (112) |
U31#(tt,V1,V2) | → | activate#(V1) | (91) |
U101#(tt,M,N) | → | isNatKind#(activate(M)) | (172) |
U104#(tt,M,N) | → | activate#(M) | (171) |
U14#(tt,V1,V2) | → | U15#(isNat(activate(V1)),activate(V2)) | (108) |
U41#(tt,V2) | → | isNatKind#(activate(V2)) | (106) |
U32#(tt,V1,V2) | → | activate#(V2) | (105) |
U102#(tt,M,N) | → | activate#(N) | (143) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V2) | (104) |
isNat#(n__x(V1,V2)) | → | isNatKind#(activate(V1)) | (103) |
isNatKind#(n__plus(V1,V2)) | → | U41#(isNatKind(activate(V1)),activate(V2)) | (167) |
U13#(tt,V1,V2) | → | activate#(V2) | (80) |
U14#(tt,V1,V2) | → | activate#(V2) | (165) |
U103#(tt,M,N) | → | activate#(N) | (142) |
U81#(tt,M,N) | → | activate#(M) | (67) |
U81#(tt,M,N) | → | isNatKind#(activate(M)) | (101) |
U34#(tt,V1,V2) | → | activate#(V2) | (162) |
U12#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (163) |
U83#(tt,M,N) | → | activate#(M) | (100) |
U32#(tt,V1,V2) | → | activate#(V1) | (161) |
activate#(n__x(X1,X2)) | → | activate#(X2) | (160) |
U91#(tt,N) | → | activate#(N) | (97) |
U35#(tt,V2) | → | isNat#(activate(V2)) | (95) |
U101#(tt,M,N) | → | activate#(M) | (132) |
isNatKind#(n__x(V1,V2)) | → | activate#(V1) | (157) |
U82#(tt,M,N) | → | activate#(M) | (94) |
U32#(tt,V1,V2) | → | U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (90) |
U31#(tt,V1,V2) | → | activate#(V1) | (91) |
U33#(tt,V1,V2) | → | activate#(V2) | (63) |
isNat#(n__x(V1,V2)) | → | activate#(V1) | (89) |
U84#(tt,M,N) | → | activate#(M) | (155) |
x#(N,0) | → | U91#(isNat(N),N) | (87) |
activate#(n__plus(X1,X2)) | → | activate#(X2) | (153) |
U33#(tt,V1,V2) | → | activate#(V1) | (86) |
U12#(tt,V1,V2) | → | activate#(V2) | (57) |
U15#(tt,V2) | → | activate#(V2) | (85) |
U33#(tt,V1,V2) | → | U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (83) |
U11#(tt,V1,V2) | → | activate#(V2) | (150) |
isNat#(n__x(V1,V2)) | → | activate#(V2) | (79) |
U13#(tt,V1,V2) | → | activate#(V2) | (80) |
U35#(tt,V2) | → | activate#(V2) | (74) |
U104#(tt,M,N) | → | activate#(N) | (75) |
U101#(tt,M,N) | → | activate#(N) | (148) |
U41#(tt,V2) | → | activate#(V2) | (73) |
U31#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (72) |
U13#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (70) |
U61#(tt,V2) | → | isNatKind#(activate(V2)) | (144) |
U103#(tt,M,N) | → | activate#(N) | (142) |
U102#(tt,M,N) | → | activate#(N) | (143) |
U33#(tt,V1,V2) | → | isNatKind#(activate(V2)) | (66) |
U81#(tt,M,N) | → | activate#(M) | (67) |
U15#(tt,V2) | → | isNat#(activate(V2)) | (65) |
isNatKind#(n__x(V1,V2)) | → | activate#(V2) | (140) |
U103#(tt,M,N) | → | isNatKind#(activate(N)) | (137) |
U33#(tt,V1,V2) | → | activate#(V2) | (63) |
U32#(tt,V1,V2) | → | activate#(V2) | (105) |
x#(N,0) | → | isNat#(N) | (134) |
U12#(tt,V1,V2) | → | activate#(V2) | (57) |
U101#(tt,M,N) | → | activate#(M) | (132) |
x#(N,s(M)) | → | isNat#(M) | (55) |
U102#(tt,M,N) | → | isNat#(activate(N)) | (54) |
The dependency pairs are split into 1 component.
activate#(n__plus(X1,X2)) | → | activate#(X1) | (159) |
activate#(n__plus(X1,X2)) | → | plus#(activate(X1),activate(X2)) | (154) |
U104#(tt,M,N) | → | x#(activate(N),activate(M)) | (82) |
U104#(tt,M,N) | → | plus#(x(activate(N),activate(M)),activate(N)) | (152) |
U14#(tt,V1,V2) | → | activate#(V1) | (128) |
U14#(tt,V1,V2) | → | isNat#(activate(V1)) | (130) |
U101#(tt,M,N) | → | U102#(isNatKind(activate(M)),activate(M),activate(N)) | (77) |
U103#(tt,M,N) | → | U104#(isNatKind(activate(N)),activate(M),activate(N)) | (110) |
U72#(tt,N) | → | activate#(N) | (96) |
U81#(tt,M,N) | → | activate#(N) | (115) |
U81#(tt,M,N) | → | U82#(isNatKind(activate(M)),activate(M),activate(N)) | (68) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (64) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (64) |
isNat#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (138) |
isNat#(n__plus(V1,V2)) | → | U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (136) |
U82#(tt,M,N) | → | activate#(N) | (69) |
U82#(tt,M,N) | → | activate#(N) | (69) |
U82#(tt,M,N) | → | isNat#(activate(N)) | (133) |
U82#(tt,M,N) | → | U83#(isNat(activate(N)),activate(M),activate(N)) | (151) |
x#(N,s(M)) | → | U101#(isNat(M),M,N) | (164) |
U11#(tt,V1,V2) | → | activate#(V1) | (59) |
U11#(tt,V1,V2) | → | activate#(V1) | (59) |
U11#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (109) |
U11#(tt,V1,V2) | → | U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (180) |
isNatKind#(n__s(V1)) | → | activate#(V1) | (118) |
isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | (111) |
U13#(tt,V1,V2) | → | activate#(V1) | (78) |
U13#(tt,V1,V2) | → | U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (141) |
U71#(tt,N) | → | activate#(N) | (92) |
U71#(tt,N) | → | activate#(N) | (92) |
U71#(tt,N) | → | isNatKind#(activate(N)) | (60) |
U71#(tt,N) | → | U72#(isNatKind(activate(N)),activate(N)) | (145) |
activate#(n__x(X1,X2)) | → | x#(activate(X1),activate(X2)) | (84) |
U84#(tt,M,N) | → | activate#(N) | (88) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (81) |
U22#(tt,V1) | → | activate#(V1) | (76) |
U22#(tt,V1) | → | isNat#(activate(V1)) | (71) |
U21#(tt,V1) | → | activate#(V1) | (62) |
U21#(tt,V1) | → | activate#(V1) | (62) |
U21#(tt,V1) | → | isNatKind#(activate(V1)) | (93) |
U21#(tt,V1) | → | U22#(isNatKind(activate(V1)),activate(V1)) | (135) |
activate#(n__s(X)) | → | activate#(X) | (58) |
U12#(tt,V1,V2) | → | activate#(V1) | (146) |
U12#(tt,V1,V2) | → | U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (127) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V1) | (107) |
isNatKind#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (147) |
plus#(N,0) | → | isNat#(N) | (131) |
plus#(N,0) | → | U71#(isNat(N),N) | (158) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (156) |
isNat#(n__s(V1)) | → | activate#(V1) | (168) |
isNat#(n__s(V1)) | → | activate#(V1) | (168) |
isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | (121) |
isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)),activate(V1)) | (98) |
U83#(tt,M,N) | → | activate#(N) | (116) |
U83#(tt,M,N) | → | activate#(N) | (116) |
U83#(tt,M,N) | → | isNatKind#(activate(N)) | (99) |
U83#(tt,M,N) | → | U84#(isNatKind(activate(N)),activate(M),activate(N)) | (173) |
U102#(tt,M,N) | → | U103#(isNat(activate(N)),activate(M),activate(N)) | (170) |
π(U72#) | = | 2 |
π(U83#) | = | 3 |
π(U11) | = | 1 |
π(isNat#) | = | 1 |
π(U42) | = | 1 |
π(U91) | = | 1 |
π(U35#) | = | 2 |
π(activate) | = | 1 |
π(U82#) | = | 3 |
π(U71) | = | 2 |
π(U81#) | = | 3 |
π(plus#) | = | 1 |
π(activate#) | = | 1 |
π(U23#) | = | 1 |
π(U23) | = | 1 |
π(U72) | = | 2 |
π(U34) | = | 1 |
π(U14#) | = | 2 |
π(U36) | = | 1 |
π(U14) | = | 1 |
π(U31) | = | 1 |
π(U92) | = | 1 |
π(U84#) | = | 3 |
π(U71#) | = | 2 |
π(isNatKind#) | = | 1 |
π(U31#) | = | 2 |
π(U61#) | = | 2 |
prec(0#) | = | 0 | status(0#) | = | [] | list-extension(0#) | = | Lex | ||
prec(U32#) | = | 0 | status(U32#) | = | [1, 3] | list-extension(U32#) | = | Lex | ||
prec(isNatKind) | = | 3 | status(isNatKind) | = | [] | list-extension(isNatKind) | = | Lex | ||
prec(U16) | = | 3 | status(U16) | = | [] | list-extension(U16) | = | Lex | ||
prec(U21) | = | 3 | status(U21) | = | [] | list-extension(U21) | = | Lex | ||
prec(s) | = | 3 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(U101#) | = | 9 | status(U101#) | = | [2, 3, 1] | list-extension(U101#) | = | Lex | ||
prec(U104#) | = | 9 | status(U104#) | = | [2, 3] | list-extension(U104#) | = | Lex | ||
prec(U92#) | = | 0 | status(U92#) | = | [] | list-extension(U92#) | = | Lex | ||
prec(U101) | = | 9 | status(U101) | = | [2, 3, 1] | list-extension(U101) | = | Lex | ||
prec(U103) | = | 9 | status(U103) | = | [2, 3, 1] | list-extension(U103) | = | Lex | ||
prec(U84) | = | 8 | status(U84) | = | [2, 3, 1] | list-extension(U84) | = | Lex | ||
prec(U35) | = | 3 | status(U35) | = | [] | list-extension(U35) | = | Lex | ||
prec(U13#) | = | 2 | status(U13#) | = | [2] | list-extension(U13#) | = | Lex | ||
prec(U103#) | = | 9 | status(U103#) | = | [2, 3] | list-extension(U103#) | = | Lex | ||
prec(U12) | = | 3 | status(U12) | = | [] | list-extension(U12) | = | Lex | ||
prec(U33#) | = | 0 | status(U33#) | = | [3, 2, 1] | list-extension(U33#) | = | Lex | ||
prec(x) | = | 9 | status(x) | = | [2, 1] | list-extension(x) | = | Lex | ||
prec(U16#) | = | 0 | status(U16#) | = | [] | list-extension(U16#) | = | Lex | ||
prec(n__s) | = | 3 | status(n__s) | = | [1] | list-extension(n__s) | = | Lex | ||
prec(U104) | = | 9 | status(U104) | = | [2, 3, 1] | list-extension(U104) | = | Lex | ||
prec(U42#) | = | 0 | status(U42#) | = | [] | list-extension(U42#) | = | Lex | ||
prec(U12#) | = | 3 | status(U12#) | = | [2] | list-extension(U12#) | = | Lex | ||
prec(U62#) | = | 0 | status(U62#) | = | [] | list-extension(U62#) | = | Lex | ||
prec(U83) | = | 8 | status(U83) | = | [2, 3, 1] | list-extension(U83) | = | Lex | ||
prec(0) | = | 3 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(U36#) | = | 0 | status(U36#) | = | [] | list-extension(U36#) | = | Lex | ||
prec(U102#) | = | 9 | status(U102#) | = | [2, 3] | list-extension(U102#) | = | Lex | ||
prec(x#) | = | 9 | status(x#) | = | [2, 1] | list-extension(x#) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(U62) | = | 3 | status(U62) | = | [] | list-extension(U62) | = | Lex | ||
prec(n__plus) | = | 8 | status(n__plus) | = | [2, 1] | list-extension(n__plus) | = | Lex | ||
prec(U15#) | = | 0 | status(U15#) | = | [1, 2] | list-extension(U15#) | = | Lex | ||
prec(U32) | = | 3 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(U33) | = | 3 | status(U33) | = | [] | list-extension(U33) | = | Lex | ||
prec(n__0) | = | 3 | status(n__0) | = | [] | list-extension(n__0) | = | Lex | ||
prec(U34#) | = | 0 | status(U34#) | = | [3, 2, 1] | list-extension(U34#) | = | Lex | ||
prec(isNat) | = | 3 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(n__x) | = | 9 | status(n__x) | = | [2, 1] | list-extension(n__x) | = | Lex | ||
prec(plus) | = | 8 | status(plus) | = | [2, 1] | list-extension(plus) | = | Lex | ||
prec(U15) | = | 3 | status(U15) | = | [] | list-extension(U15) | = | Lex | ||
prec(U61) | = | 3 | status(U61) | = | [] | list-extension(U61) | = | Lex | ||
prec(U51#) | = | 0 | status(U51#) | = | [] | list-extension(U51#) | = | Lex | ||
prec(U11#) | = | 7 | status(U11#) | = | [1, 2] | list-extension(U11#) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [2, 1] | list-extension(U41#) | = | Lex | ||
prec(U102) | = | 9 | status(U102) | = | [2, 3, 1] | list-extension(U102) | = | Lex | ||
prec(U21#) | = | 2 | status(U21#) | = | [2] | list-extension(U21#) | = | Lex | ||
prec(U81) | = | 8 | status(U81) | = | [2, 3, 1] | list-extension(U81) | = | Lex | ||
prec(U82) | = | 8 | status(U82) | = | [2, 3, 1] | list-extension(U82) | = | Lex | ||
prec(U22#) | = | 1 | status(U22#) | = | [2] | list-extension(U22#) | = | Lex | ||
prec(tt) | = | 3 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U13) | = | 3 | status(U13) | = | [] | list-extension(U13) | = | Lex | ||
prec(U22) | = | 3 | status(U22) | = | [] | list-extension(U22) | = | Lex | ||
prec(U51) | = | 3 | status(U51) | = | [] | list-extension(U51) | = | Lex | ||
prec(U41) | = | 3 | status(U41) | = | [] | list-extension(U41) | = | Lex | ||
prec(U91#) | = | 0 | status(U91#) | = | [2, 1] | list-extension(U91#) | = | Lex |
[0#] | = | 0 |
[U32#(x1, x2, x3)] | = | max(x1 + 0, x3 + 0, 0) |
[isNatKind(x1)] | = | 0 |
[U16(x1)] | = | 0 |
[U21(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[U101#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U104#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U92#(x1)] | = | 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) |
[U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U35(x1, x2)] | = | max(0) |
[U13#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U103#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U12(x1, x2, x3)] | = | max(0) |
[U33#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 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, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[0] | = | 0 |
[U36#(x1)] | = | 0 |
[U102#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[x#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[s#(x1)] | = | 0 |
[U62(x1)] | = | 0 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U32(x1, x2, x3)] | = | max(0) |
[U33(x1, x2, x3)] | = | max(0) |
[n__0] | = | 0 |
[U34#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[isNat(x1)] | = | 0 |
[n__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15(x1, x2)] | = | max(0) |
[U61(x1, x2)] | = | max(0) |
[U51#(x1)] | = | 0 |
[U11#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, 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(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 |
[U13(x1, x2, x3)] | = | max(0) |
[U22(x1, x2)] | = | max(0) |
[U51(x1)] | = | 0 |
[U41(x1, x2)] | = | max(0) |
[U91#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
activate(n__plus(X1,X2)) | → | plus(activate(X1),activate(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(activate(X1),activate(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(activate(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)) | → | activate#(X1) | (159) |
activate#(n__plus(X1,X2)) | → | plus#(activate(X1),activate(X2)) | (154) |
U101#(tt,M,N) | → | U102#(isNatKind(activate(M)),activate(M),activate(N)) | (77) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (64) |
isNat#(n__plus(V1,V2)) | → | activate#(V1) | (64) |
isNat#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (138) |
isNat#(n__plus(V1,V2)) | → | U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (136) |
x#(N,s(M)) | → | U101#(isNat(M),M,N) | (164) |
U11#(tt,V1,V2) | → | activate#(V1) | (59) |
U11#(tt,V1,V2) | → | activate#(V1) | (59) |
U11#(tt,V1,V2) | → | isNatKind#(activate(V1)) | (109) |
U11#(tt,V1,V2) | → | U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) | (180) |
isNatKind#(n__s(V1)) | → | activate#(V1) | (118) |
isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | (111) |
U13#(tt,V1,V2) | → | activate#(V1) | (78) |
U13#(tt,V1,V2) | → | U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (141) |
U22#(tt,V1) | → | activate#(V1) | (76) |
U22#(tt,V1) | → | isNat#(activate(V1)) | (71) |
U21#(tt,V1) | → | activate#(V1) | (62) |
U21#(tt,V1) | → | activate#(V1) | (62) |
U21#(tt,V1) | → | isNatKind#(activate(V1)) | (93) |
U21#(tt,V1) | → | U22#(isNatKind(activate(V1)),activate(V1)) | (135) |
activate#(n__s(X)) | → | activate#(X) | (58) |
U12#(tt,V1,V2) | → | activate#(V1) | (146) |
U12#(tt,V1,V2) | → | U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) | (127) |
isNatKind#(n__plus(V1,V2)) | → | activate#(V1) | (107) |
isNatKind#(n__plus(V1,V2)) | → | isNatKind#(activate(V1)) | (147) |
isNat#(n__s(V1)) | → | activate#(V1) | (168) |
isNat#(n__s(V1)) | → | activate#(V1) | (168) |
isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | (121) |
isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)),activate(V1)) | (98) |
The dependency pairs are split into 1 component.
U81#(tt,M,N) | → | U82#(isNatKind(activate(M)),activate(M),activate(N)) | (68) |
U82#(tt,M,N) | → | U83#(isNat(activate(N)),activate(M),activate(N)) | (151) |
U84#(tt,M,N) | → | plus#(activate(N),activate(M)) | (81) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (156) |
U83#(tt,M,N) | → | U84#(isNatKind(activate(N)),activate(M),activate(N)) | (173) |
π(U72#) | = | 2 |
π(U11) | = | 1 |
π(isNat#) | = | 1 |
π(U42) | = | 1 |
π(U91) | = | 1 |
π(U35#) | = | 2 |
π(activate) | = | 1 |
π(U71) | = | 2 |
π(activate#) | = | 1 |
π(U23#) | = | 1 |
π(U23) | = | 1 |
π(U72) | = | 2 |
π(U34) | = | 1 |
π(U14#) | = | 2 |
π(U36) | = | 1 |
π(U14) | = | 1 |
π(U31) | = | 1 |
π(U92) | = | 1 |
π(U71#) | = | 2 |
π(isNatKind#) | = | 1 |
π(U31#) | = | 2 |
π(U61#) | = | 2 |
prec(0#) | = | 0 | status(0#) | = | [] | list-extension(0#) | = | Lex | ||
prec(U32#) | = | 0 | status(U32#) | = | [1, 3] | list-extension(U32#) | = | Lex | ||
prec(isNatKind) | = | 3 | status(isNatKind) | = | [] | list-extension(isNatKind) | = | Lex | ||
prec(U16) | = | 3 | status(U16) | = | [] | list-extension(U16) | = | Lex | ||
prec(U21) | = | 3 | status(U21) | = | [] | list-extension(U21) | = | Lex | ||
prec(U83#) | = | 3 | status(U83#) | = | [2, 3] | list-extension(U83#) | = | Lex | ||
prec(s) | = | 3 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(U101#) | = | 9 | status(U101#) | = | [2, 3, 1] | list-extension(U101#) | = | Lex | ||
prec(U82#) | = | 3 | status(U82#) | = | [2, 3] | list-extension(U82#) | = | Lex | ||
prec(U104#) | = | 9 | status(U104#) | = | [2, 3] | list-extension(U104#) | = | Lex | ||
prec(U81#) | = | 3 | status(U81#) | = | [2, 3] | list-extension(U81#) | = | Lex | ||
prec(U92#) | = | 0 | status(U92#) | = | [] | list-extension(U92#) | = | Lex | ||
prec(plus#) | = | 3 | status(plus#) | = | [2, 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(U84) | = | 9 | status(U84) | = | [2, 3, 1] | list-extension(U84) | = | Lex | ||
prec(U35) | = | 3 | status(U35) | = | [] | list-extension(U35) | = | Lex | ||
prec(U13#) | = | 2 | status(U13#) | = | [2] | list-extension(U13#) | = | Lex | ||
prec(U103#) | = | 9 | status(U103#) | = | [2, 3] | list-extension(U103#) | = | Lex | ||
prec(U12) | = | 3 | status(U12) | = | [] | list-extension(U12) | = | Lex | ||
prec(U33#) | = | 0 | status(U33#) | = | [3, 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) | = | 3 | 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#) | = | 3 | status(U12#) | = | [2] | 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) | = | 3 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(U36#) | = | 0 | status(U36#) | = | [] | list-extension(U36#) | = | Lex | ||
prec(U102#) | = | 9 | status(U102#) | = | [2, 3] | list-extension(U102#) | = | Lex | ||
prec(x#) | = | 9 | status(x#) | = | [2, 1] | list-extension(x#) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(U62) | = | 3 | status(U62) | = | [] | list-extension(U62) | = | Lex | ||
prec(n__plus) | = | 9 | status(n__plus) | = | [2, 1] | list-extension(n__plus) | = | Lex | ||
prec(U15#) | = | 0 | status(U15#) | = | [1, 2] | list-extension(U15#) | = | Lex | ||
prec(U32) | = | 3 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(U33) | = | 3 | status(U33) | = | [] | list-extension(U33) | = | Lex | ||
prec(n__0) | = | 3 | status(n__0) | = | [] | list-extension(n__0) | = | Lex | ||
prec(U34#) | = | 0 | status(U34#) | = | [3, 2, 1] | list-extension(U34#) | = | Lex | ||
prec(isNat) | = | 3 | 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(U15) | = | 3 | status(U15) | = | [] | list-extension(U15) | = | Lex | ||
prec(U61) | = | 3 | status(U61) | = | [] | list-extension(U61) | = | Lex | ||
prec(U51#) | = | 0 | status(U51#) | = | [] | list-extension(U51#) | = | Lex | ||
prec(U11#) | = | 7 | status(U11#) | = | [1, 2] | list-extension(U11#) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [2, 1] | list-extension(U41#) | = | Lex | ||
prec(U102) | = | 10 | status(U102) | = | [2, 3, 1] | list-extension(U102) | = | Lex | ||
prec(U21#) | = | 2 | status(U21#) | = | [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#) | = | 1 | status(U22#) | = | [2] | list-extension(U22#) | = | Lex | ||
prec(tt) | = | 3 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U84#) | = | 3 | status(U84#) | = | [2, 3] | list-extension(U84#) | = | Lex | ||
prec(U13) | = | 3 | status(U13) | = | [] | list-extension(U13) | = | Lex | ||
prec(U22) | = | 3 | status(U22) | = | [] | list-extension(U22) | = | Lex | ||
prec(U51) | = | 3 | status(U51) | = | [] | list-extension(U51) | = | Lex | ||
prec(U41) | = | 3 | status(U41) | = | [] | list-extension(U41) | = | Lex | ||
prec(U91#) | = | 0 | status(U91#) | = | [2, 1] | list-extension(U91#) | = | Lex |
[0#] | = | 0 |
[U32#(x1, x2, x3)] | = | max(x1 + 0, x3 + 0, 0) |
[isNatKind(x1)] | = | 0 |
[U16(x1)] | = | 0 |
[U21(x1, x2)] | = | max(0) |
[U83#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[U101#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U82#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U104#(x1, x2, x3)] | = | max(x2 + 0, x3 + 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(x1 + 0, x2 + 0, x3 + 0, 0) |
[U103(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U35(x1, x2)] | = | max(0) |
[U13#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U103#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U12(x1, x2, x3)] | = | max(0) |
[U33#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 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, 0) |
[U62#(x1)] | = | 0 |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[0] | = | 0 |
[U36#(x1)] | = | 0 |
[U102#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[x#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[s#(x1)] | = | 0 |
[U62(x1)] | = | 0 |
[n__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U32(x1, x2, x3)] | = | max(0) |
[U33(x1, x2, x3)] | = | max(0) |
[n__0] | = | 0 |
[U34#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[isNat(x1)] | = | 0 |
[n__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15(x1, x2)] | = | max(0) |
[U61(x1, x2)] | = | max(0) |
[U51#(x1)] | = | 0 |
[U11#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, 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(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, x3 + 0, 0) |
[U13(x1, x2, x3)] | = | max(0) |
[U22(x1, x2)] | = | max(0) |
[U51(x1)] | = | 0 |
[U41(x1, x2)] | = | max(0) |
[U91#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
activate(n__plus(X1,X2)) | → | plus(activate(X1),activate(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(activate(X1),activate(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(activate(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) |
plus#(N,s(M)) | → | U81#(isNat(M),M,N) | (156) |
The dependency pairs are split into 0 components.