The rewrite relation of the following TRS is considered.
There are 119 ruless (increase limit for explicit display).
There are 146 ruless (increase limit for explicit display).
The dependency pairs are split into 3 components.
mark#(U71(X1,X2)) | → | mark#(X1) | (264) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
mark#(U34(X1,X2,X3)) | → | mark#(X1) | (261) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (198) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (194) |
a__U84#(tt,M,N) | → | mark#(M) | (190) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (256) |
mark#(U31(X1,X2,X3)) | → | mark#(X1) | (186) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (187) |
mark#(U16(X)) | → | mark#(X) | (185) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (184) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
mark#(U33(X1,X2,X3)) | → | mark#(X1) | (181) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
a__U104#(tt,M,N) | → | mark#(N) | (148) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (176) |
a__U84#(tt,M,N) | → | mark#(N) | (177) |
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (250) |
mark#(U61(X1,X2)) | → | mark#(X1) | (175) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (172) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (246) |
mark#(U12(X1,X2,X3)) | → | mark#(X1) | (244) |
mark#(x(X1,X2)) | → | mark#(X2) | (241) |
mark#(U62(X)) | → | mark#(X) | (167) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (166) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (236) |
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
a__U72#(tt,N) | → | mark#(N) | (230) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (227) |
mark#(U92(X)) | → | mark#(X) | (228) |
mark#(U32(X1,X2,X3)) | → | mark#(X1) | (152) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (226) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (225) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (224) |
a__U104#(tt,M,N) | → | mark#(N) | (148) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(x(X1,X2)) | → | mark#(X1) | (223) |
mark#(U22(X1,X2)) | → | mark#(X1) | (145) |
mark#(U14(X1,X2,X3)) | → | mark#(X1) | (146) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(plus(X1,X2)) | → | mark#(X2) | (142) |
a__U104#(tt,M,N) | → | mark#(M) | (141) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (221) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
mark#(U91(X1,X2)) | → | mark#(X1) | (214) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (212) |
mark#(U23(X)) | → | mark#(X) | (213) |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
mark#(U13(X1,X2,X3)) | → | mark#(X1) | (131) |
mark#(U35(X1,X2)) | → | mark#(X1) | (208) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (207) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (125) |
mark#(U42(X)) | → | mark#(X) | (126) |
mark#(U21(X1,X2)) | → | mark#(X1) | (206) |
mark#(U72(X1,X2)) | → | mark#(X1) | (123) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
mark#(U36(X)) | → | mark#(X) | (122) |
[a__U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 35295, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | x1 + 0 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 35295, 0) |
[U16(x1)] | = | x1 + 1 |
[U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U102(x1, x2, x3)] | = | max(x1 + 24552, x2 + 35292, x3 + 116339, 0) |
[a__U82#(x1, x2, x3)] | = | max(x1 + 17015, x2 + 91785, x3 + 56492, 0) |
[a__U15#(x1, x2)] | = | max(0) |
[a__U72#(x1, x2)] | = | max(x1 + 56491, x2 + 56492, 0) |
[a__U71#(x1, x2)] | = | max(x1 + 26666, x2 + 56492, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 25955, 0) |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | max(x1 + 116339, x2 + 35292, x3 + 116339, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(0) |
[a__U33#(x1, x2, x3)] | = | max(0) |
[a__U33(x1, x2, x3)] | = | max(x1 + 35291, x2 + 35290, x3 + 35290, 0) |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | x1 + 1 |
[U91(x1, x2)] | = | max(x1 + 1, x2 + 91788, 0) |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | max(x1 + 35294, x2 + 35295, x3 + 0, 0) |
[a__U14#(x1, x2, x3)] | = | max(0) |
[U71(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 35295, x3 + 0, 0) |
[a__U62(x1)] | = | x1 + 1 |
[U101(x1, x2, x3)] | = | max(x1 + 35292, x2 + 35292, x3 + 116339, 0) |
[a__U13#(x1, x2, x3)] | = | max(0) |
[U103(x1, x2, x3)] | = | max(x1 + 116339, x2 + 35292, x3 + 116339, 0) |
[a__U103#(x1, x2, x3)] | = | max(x2 + 91784, x3 + 172831, 0) |
[U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 35295, x3 + 0, 0) |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 0 |
[U35(x1, x2)] | = | max(x1 + 35289, x2 + 35288, 0) |
[a__x#(x1, x2)] | = | max(x1 + 172831, x2 + 91784, 0) |
[a__U22(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U72(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[U34(x1, x2, x3)] | = | max(x1 + 35289, x2 + 35289, x3 + 35290, 0) |
[a__U31(x1, x2, x3)] | = | max(x1 + 35292, x2 + 35292, x3 + 35292, 0) |
[a__U51(x1)] | = | x1 + 0 |
[a__U81(x1, x2, x3)] | = | max(x1 + 35294, x2 + 35295, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 116339, x2 + 35292, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 25955, 0) |
[a__U84#(x1, x2, x3)] | = | max(x1 + 0, x2 + 91785, x3 + 56492, 0) |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | x1 + 1 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[x(x1, x2)] | = | max(x1 + 116339, x2 + 35292, 0) |
[a__U12#(x1, x2, x3)] | = | max(0) |
[U104(x1, x2, x3)] | = | max(x1 + 116339, x2 + 35292, x3 + 116339, 0) |
[a__U14(x1, x2, x3)] | = | max(x1 + 25954, x2 + 0, x3 + 90, 0) |
[a__U21#(x1, x2)] | = | max(0) |
[a__U81#(x1, x2, x3)] | = | max(x2 + 91785, x3 + 56492, 0) |
[a__U61#(x1, x2)] | = | max(0) |
[a__U34(x1, x2, x3)] | = | max(x1 + 35289, x2 + 35289, x3 + 35290, 0) |
[a__plus#(x1, x2)] | = | max(x1 + 56492, x2 + 91785, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 35295, x3 + 0, 0) |
[mark#(x1)] | = | x1 + 56492 |
[0] | = | 91786 |
[a__U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U36(x1)] | = | x1 + 1 |
[a__U32(x1, x2, x3)] | = | max(x1 + 35292, x2 + 35291, x3 + 35291, 0) |
[a__U91(x1, x2)] | = | max(x1 + 1, x2 + 91788, 0) |
[a__U36(x1)] | = | x1 + 1 |
[U62(x1)] | = | x1 + 1 |
[a__U102#(x1, x2, x3)] | = | max(x2 + 91784, x3 + 172831, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U72(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x1 + 91783, x2 + 91784, x3 + 172831, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 25955, 0) |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | max(x1 + 35292, x2 + 35291, x3 + 35291, 0) |
[a__U42(x1)] | = | x1 + 1 |
[U33(x1, x2, x3)] | = | max(x1 + 35291, x2 + 35290, x3 + 35290, 0) |
[U14(x1, x2, x3)] | = | max(x1 + 25954, x2 + 0, x3 + 90, 0) |
[a__U12(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 25955, 0) |
[a__U104#(x1, x2, x3)] | = | max(x1 + 172831, x2 + 91784, x3 + 172831, 0) |
[isNat(x1)] | = | x1 + 0 |
[a__U35(x1, x2)] | = | max(x1 + 35289, x2 + 35288, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 35295, 0) |
[U15(x1, x2)] | = | max(x1 + 0, x2 + 13, 0) |
[U61(x1, x2)] | = | max(x1 + 22281, x2 + 22280, 0) |
[a__U35#(x1, x2)] | = | max(0) |
[a__U22#(x1, x2)] | = | max(0) |
[a__U13(x1, x2, x3)] | = | max(x1 + 25955, x2 + 0, x3 + 25954, 0) |
[U31(x1, x2, x3)] | = | max(x1 + 35292, x2 + 35292, x3 + 35292, 0) |
[a__U83#(x1, x2, x3)] | = | max(x2 + 91785, x3 + 56492, 0) |
[a__U71(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U92(x1)] | = | x1 + 91788 |
[a__U92(x1)] | = | x1 + 91788 |
[a__U61(x1, x2)] | = | max(x1 + 22281, x2 + 22280, 0) |
[U102(x1, x2, x3)] | = | max(x1 + 24552, x2 + 35292, x3 + 116339, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 35294, x2 + 35295, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(0) |
[a__U15(x1, x2)] | = | max(x1 + 0, x2 + 13, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 35294, x2 + 35295, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 91786 |
[a__isNat(x1)] | = | x1 + 0 |
[U13(x1, x2, x3)] | = | max(x1 + 25955, x2 + 0, x3 + 25954, 0) |
[a__U23(x1)] | = | x1 + 0 |
[a__isNatKind(x1)] | = | x1 + 0 |
[U22(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U51(x1)] | = | x1 + 0 |
[a__U34#(x1, x2, x3)] | = | max(0) |
[a__U103(x1, x2, x3)] | = | max(x1 + 116339, x2 + 35292, x3 + 116339, 0) |
[U41(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[a__U32#(x1, x2, x3)] | = | max(0) |
[a__U101(x1, x2, x3)] | = | max(x1 + 35292, x2 + 35292, x3 + 116339, 0) |
[a__U91#(x1, x2)] | = | max(0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(U34(X1,X2,X3)) | → | mark#(X1) | (261) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (198) |
a__U84#(tt,M,N) | → | mark#(M) | (190) |
mark#(U31(X1,X2,X3)) | → | mark#(X1) | (186) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (187) |
mark#(U16(X)) | → | mark#(X) | (185) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (184) |
mark#(U33(X1,X2,X3)) | → | mark#(X1) | (181) |
a__U104#(tt,M,N) | → | mark#(N) | (148) |
mark#(U61(X1,X2)) | → | mark#(X1) | (175) |
mark#(x(X1,X2)) | → | mark#(X2) | (241) |
mark#(U62(X)) | → | mark#(X) | (167) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (227) |
mark#(U92(X)) | → | mark#(X) | (228) |
mark#(U32(X1,X2,X3)) | → | mark#(X1) | (152) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (225) |
a__U104#(tt,M,N) | → | mark#(N) | (148) |
mark#(x(X1,X2)) | → | mark#(X1) | (223) |
mark#(U14(X1,X2,X3)) | → | mark#(X1) | (146) |
mark#(plus(X1,X2)) | → | mark#(X2) | (142) |
a__U104#(tt,M,N) | → | mark#(M) | (141) |
mark#(U91(X1,X2)) | → | mark#(X1) | (214) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (212) |
mark#(U13(X1,X2,X3)) | → | mark#(X1) | (131) |
mark#(U35(X1,X2)) | → | mark#(X1) | (208) |
mark#(U42(X)) | → | mark#(X) | (126) |
mark#(U36(X)) | → | mark#(X) | (122) |
The dependency pairs are split into 1 component.
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (226) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (207) |
mark#(U12(X1,X2,X3)) | → | mark#(X1) | (244) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (176) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (221) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
a__U72#(tt,N) | → | mark#(N) | (230) |
mark#(U22(X1,X2)) | → | mark#(X1) | (145) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (224) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (125) |
a__U84#(tt,M,N) | → | mark#(N) | (177) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (236) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (194) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(U21(X1,X2)) | → | mark#(X1) | (206) |
mark#(U23(X)) | → | mark#(X) | (213) |
mark#(U72(X1,X2)) | → | mark#(X1) | (123) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (172) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (246) |
mark#(U71(X1,X2)) | → | mark#(X1) | (264) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (256) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (166) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (250) |
[a__U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 50386, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 0 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 50386, 0) |
[U16(x1)] | = | x1 + 0 |
[U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U102(x1, x2, x3)] | = | max(x1 + 13855, x2 + 50385, x3 + 62770, 0) |
[a__U82#(x1, x2, x3)] | = | max(x1 + 33988, x2 + 63179, x3 + 90404, 0) |
[a__U15#(x1, x2)] | = | max(0) |
[a__U72#(x1, x2)] | = | max(x1 + 32299, x2 + 90404, 0) |
[a__U71#(x1, x2)] | = | max(x1 + 72680, x2 + 90404, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 50386, 0) |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | max(x1 + 62770, x2 + 50385, x3 + 62770, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(0) |
[a__U33#(x1, x2, x3)] | = | max(0) |
[a__U33(x1, x2, x3)] | = | max(x1 + 3, x2 + 2, x3 + 2, 0) |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[U91(x1, x2)] | = | max(x1 + 3103, x2 + 59885, 0) |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | max(x1 + 50386, x2 + 50386, x3 + 0, 0) |
[a__U14#(x1, x2, x3)] | = | max(0) |
[U71(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x1 + 50386, x2 + 50386, x3 + 0, 0) |
[a__U62(x1)] | = | 0 |
[U101(x1, x2, x3)] | = | max(x1 + 50385, x2 + 50385, x3 + 62770, 0) |
[a__U13#(x1, x2, x3)] | = | max(0) |
[U103(x1, x2, x3)] | = | max(x1 + 62770, x2 + 50385, x3 + 62770, 0) |
[a__U103#(x1, x2, x3)] | = | max(x2 + 140789, x3 + 153174, 0) |
[U84(x1, x2, x3)] | = | max(x1 + 50386, x2 + 50386, x3 + 0, 0) |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 0 |
[U35(x1, x2)] | = | max(x1 + 1, 0) |
[a__x#(x1, x2)] | = | max(x1 + 153174, x2 + 140789, 0) |
[a__U22(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U72(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[U34(x1, x2, x3)] | = | max(x1 + 1, x2 + 1, x3 + 2, 0) |
[a__U31(x1, x2, x3)] | = | max(x1 + 50385, x2 + 50385, x3 + 50385, 0) |
[a__U51(x1)] | = | x1 + 0 |
[a__U81(x1, x2, x3)] | = | max(x1 + 50386, x2 + 50386, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 62770, x2 + 50385, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 18128, x2 + 0, x3 + 50386, 0) |
[a__U84#(x1, x2, x3)] | = | max(x1 + 63180, x2 + 63179, x3 + 90404, 0) |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | x1 + 0 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(x1 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 62770, x2 + 50385, 0) |
[a__U12#(x1, x2, x3)] | = | max(0) |
[U104(x1, x2, x3)] | = | max(x1 + 62770, x2 + 50385, x3 + 62770, 0) |
[a__U14(x1, x2, x3)] | = | max(x1 + 15118, x2 + 0, x3 + 1, 0) |
[a__U21#(x1, x2)] | = | max(0) |
[a__U81#(x1, x2, x3)] | = | max(x2 + 63179, x3 + 90404, 0) |
[a__U61#(x1, x2)] | = | max(0) |
[a__U34(x1, x2, x3)] | = | max(x1 + 1, x2 + 1, x3 + 2, 0) |
[a__plus#(x1, x2)] | = | max(x1 + 90404, x2 + 63179, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 50386, x3 + 0, 0) |
[mark#(x1)] | = | x1 + 90404 |
[0] | = | 9500 |
[a__U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U36(x1)] | = | 0 |
[a__U32(x1, x2, x3)] | = | max(x1 + 28582, x2 + 2, x3 + 28581, 0) |
[a__U91(x1, x2)] | = | max(x1 + 3103, x2 + 59885, 0) |
[a__U36(x1)] | = | 0 |
[U62(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | max(x2 + 140789, x3 + 153174, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U72(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x1 + 25783, x2 + 140789, x3 + 153174, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 50386, 0) |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | max(x1 + 28582, x2 + 2, x3 + 28581, 0) |
[a__U42(x1)] | = | x1 + 0 |
[U33(x1, x2, x3)] | = | max(x1 + 3, x2 + 2, x3 + 2, 0) |
[U14(x1, x2, x3)] | = | max(x1 + 15118, x2 + 0, x3 + 1, 0) |
[a__U12(x1, x2, x3)] | = | max(x1 + 18128, x2 + 0, x3 + 50386, 0) |
[a__U104#(x1, x2, x3)] | = | max(x1 + 153173, x2 + 140789, x3 + 153174, 0) |
[isNat(x1)] | = | x1 + 0 |
[a__U35(x1, x2)] | = | max(x1 + 1, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 50386, 0) |
[U15(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[U61(x1, x2)] | = | max(0) |
[a__U35#(x1, x2)] | = | max(0) |
[a__U22#(x1, x2)] | = | max(0) |
[a__U13(x1, x2, x3)] | = | max(x1 + 15119, x2 + 0, x3 + 15118, 0) |
[U31(x1, x2, x3)] | = | max(x1 + 50385, x2 + 50385, x3 + 50385, 0) |
[a__U83#(x1, x2, x3)] | = | max(x2 + 63179, x3 + 90404, 0) |
[a__U71(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U92(x1)] | = | x1 + 59885 |
[a__U92(x1)] | = | x1 + 59885 |
[a__U61(x1, x2)] | = | max(0) |
[U102(x1, x2, x3)] | = | max(x1 + 13855, x2 + 50385, x3 + 62770, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 50386, x2 + 50386, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(0) |
[a__U15(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 50386, x2 + 50386, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 0 |
[a__isNat(x1)] | = | x1 + 0 |
[U13(x1, x2, x3)] | = | max(x1 + 15119, x2 + 0, x3 + 15118, 0) |
[a__U23(x1)] | = | x1 + 0 |
[a__isNatKind(x1)] | = | 0 |
[U22(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U51(x1)] | = | x1 + 0 |
[a__U34#(x1, x2, x3)] | = | max(0) |
[a__U103(x1, x2, x3)] | = | max(x1 + 62770, x2 + 50385, x3 + 62770, 0) |
[U41(x1, x2)] | = | max(x1 + 0, 0) |
[a__U32#(x1, x2, x3)] | = | max(0) |
[a__U101(x1, x2, x3)] | = | max(x1 + 50385, x2 + 50385, x3 + 62770, 0) |
[a__U91#(x1, x2)] | = | max(0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(U12(X1,X2,X3)) | → | mark#(X1) | (244) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (194) |
The dependency pairs are split into 1 component.
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (226) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (207) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (176) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (221) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
a__U72#(tt,N) | → | mark#(N) | (230) |
mark#(U22(X1,X2)) | → | mark#(X1) | (145) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (224) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (125) |
a__U84#(tt,M,N) | → | mark#(N) | (177) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (236) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(U21(X1,X2)) | → | mark#(X1) | (206) |
mark#(U23(X)) | → | mark#(X) | (213) |
mark#(U72(X1,X2)) | → | mark#(X1) | (123) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (172) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (246) |
mark#(U71(X1,X2)) | → | mark#(X1) | (264) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (256) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (166) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (250) |
[a__U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 0 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U16(x1)] | = | 0 |
[U21(x1, x2)] | = | max(x1 + 0, 0) |
[a__U102(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U82#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U15#(x1, x2)] | = | max(0) |
[a__U72#(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__U71#(x1, x2)] | = | max(x1 + 15215, x2 + 0, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 0, 0) |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(0) |
[a__U33#(x1, x2, x3)] | = | max(0) |
[a__U33(x1, x2, x3)] | = | max(0) |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | 0 |
[U91(x1, x2)] | = | max(x1 + 15215, 0) |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U14#(x1, x2, x3)] | = | max(0) |
[U71(x1, x2)] | = | max(x1 + 15215, x2 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U62(x1)] | = | 0 |
[U101(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U13#(x1, x2, x3)] | = | max(0) |
[U103(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U103#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U84(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 0 |
[U35(x1, x2)] | = | max(0) |
[a__x#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U22(x1, x2)] | = | max(x1 + 0, 0) |
[U72(x1, x2)] | = | max(x1 + 7250, x2 + 0, 0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[U34(x1, x2, x3)] | = | max(0) |
[a__U31(x1, x2, x3)] | = | max(0) |
[a__U51(x1)] | = | x1 + 0 |
[a__U81(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U12(x1, x2, x3)] | = | max(0) |
[a__U84#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 0 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(x1 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U12#(x1, x2, x3)] | = | max(0) |
[U104(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U14(x1, x2, x3)] | = | max(0) |
[a__U21#(x1, x2)] | = | max(0) |
[a__U81#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U61#(x1, x2)] | = | max(0) |
[a__U34(x1, x2, x3)] | = | max(0) |
[a__plus#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 15215 |
[a__U21(x1, x2)] | = | max(x1 + 0, 0) |
[U36(x1)] | = | 0 |
[a__U32(x1, x2, x3)] | = | max(0) |
[a__U91(x1, x2)] | = | max(x1 + 15215, 0) |
[a__U36(x1)] | = | 0 |
[U62(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U72(x1, x2)] | = | max(x1 + 7250, x2 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 0, 0) |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | max(0) |
[a__U42(x1)] | = | 0 |
[U33(x1, x2, x3)] | = | max(0) |
[U14(x1, x2, x3)] | = | max(0) |
[a__U12(x1, x2, x3)] | = | max(0) |
[a__U104#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[isNat(x1)] | = | 0 |
[a__U35(x1, x2)] | = | max(0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15(x1, x2)] | = | max(x1 + 0, 0) |
[U61(x1, x2)] | = | max(x1 + 0, 0) |
[a__U35#(x1, x2)] | = | max(0) |
[a__U22#(x1, x2)] | = | max(0) |
[a__U13(x1, x2, x3)] | = | max(0) |
[U31(x1, x2, x3)] | = | max(0) |
[a__U83#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U71(x1, x2)] | = | max(x1 + 15215, x2 + 0, 0) |
[U92(x1)] | = | 15215 |
[a__U92(x1)] | = | 15215 |
[a__U61(x1, x2)] | = | max(x1 + 0, 0) |
[U102(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(0) |
[a__U15(x1, x2)] | = | max(x1 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 0 |
[a__isNat(x1)] | = | 0 |
[U13(x1, x2, x3)] | = | max(0) |
[a__U23(x1)] | = | x1 + 0 |
[a__isNatKind(x1)] | = | 0 |
[U22(x1, x2)] | = | max(x1 + 0, 0) |
[U51(x1)] | = | x1 + 0 |
[a__U34#(x1, x2, x3)] | = | max(0) |
[a__U103(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[U41(x1, x2)] | = | max(x1 + 0, 0) |
[a__U32#(x1, x2, x3)] | = | max(0) |
[a__U101(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[a__U91#(x1, x2)] | = | max(0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(U72(X1,X2)) | → | mark#(X1) | (123) |
mark#(U71(X1,X2)) | → | mark#(X1) | (264) |
The dependency pairs are split into 1 component.
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (226) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (207) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (176) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (221) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
a__U72#(tt,N) | → | mark#(N) | (230) |
mark#(U22(X1,X2)) | → | mark#(X1) | (145) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (224) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (125) |
a__U84#(tt,M,N) | → | mark#(N) | (177) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (236) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(U21(X1,X2)) | → | mark#(X1) | (206) |
mark#(U23(X)) | → | mark#(X) | (213) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (172) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (246) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (256) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (166) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (250) |
[a__U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 1, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 0 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[U16(x1)] | = | 0 |
[U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U102(x1, x2, x3)] | = | max(x2 + 6264, x3 + 6264, 0) |
[a__U82#(x1, x2, x3)] | = | max(x1 + 2, x2 + 1, x3 + 2, 0) |
[a__U15#(x1, x2)] | = | max(0) |
[a__U72#(x1, x2)] | = | max(x1 + 1, x2 + 2, 0) |
[a__U71#(x1, x2)] | = | max(x2 + 2, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 1, x2 + 0, x3 + 1, 0) |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | max(x1 + 6264, x2 + 6264, x3 + 6264, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(0) |
[a__U33#(x1, x2, x3)] | = | max(0) |
[a__U33(x1, x2, x3)] | = | max(0) |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | 0 |
[U91(x1, x2)] | = | max(x1 + 2, 0) |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 1, x3 + 0, 0) |
[a__U14#(x1, x2, x3)] | = | max(0) |
[U71(x1, x2)] | = | max(x2 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x2 + 1, x3 + 0, 0) |
[a__U62(x1)] | = | 0 |
[U101(x1, x2, x3)] | = | max(x2 + 6264, x3 + 6264, 0) |
[a__U13#(x1, x2, x3)] | = | max(0) |
[U103(x1, x2, x3)] | = | max(x2 + 6264, x3 + 6264, 0) |
[a__U103#(x1, x2, x3)] | = | max(x2 + 6266, x3 + 6266, 0) |
[U84(x1, x2, x3)] | = | max(x2 + 1, x3 + 0, 0) |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 0 |
[U35(x1, x2)] | = | max(0) |
[a__x#(x1, x2)] | = | max(x1 + 6266, x2 + 6266, 0) |
[a__U22(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U72(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[U34(x1, x2, x3)] | = | max(0) |
[a__U31(x1, x2, x3)] | = | max(0) |
[a__U51(x1)] | = | x1 + 0 |
[a__U81(x1, x2, x3)] | = | max(x1 + 1, x2 + 1, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 6264, x2 + 6264, 0) |
[U12(x1, x2, x3)] | = | max(x2 + 0, x3 + 1, 0) |
[a__U84#(x1, x2, x3)] | = | max(x2 + 1, x3 + 2, 0) |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 0 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(x1 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 6264, x2 + 6264, 0) |
[a__U12#(x1, x2, x3)] | = | max(0) |
[U104(x1, x2, x3)] | = | max(x1 + 6264, x2 + 6264, x3 + 6264, 0) |
[a__U14(x1, x2, x3)] | = | max(x2 + 0, x3 + 1, 0) |
[a__U21#(x1, x2)] | = | max(0) |
[a__U81#(x1, x2, x3)] | = | max(x2 + 1, x3 + 2, 0) |
[a__U61#(x1, x2)] | = | max(0) |
[a__U34(x1, x2, x3)] | = | max(0) |
[a__plus#(x1, x2)] | = | max(x1 + 2, x2 + 1, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 1, x3 + 0, 0) |
[mark#(x1)] | = | x1 + 2 |
[0] | = | 2 |
[a__U21(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U36(x1)] | = | 0 |
[a__U32(x1, x2, x3)] | = | max(0) |
[a__U91(x1, x2)] | = | max(x1 + 2, 0) |
[a__U36(x1)] | = | 0 |
[U62(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | max(x2 + 6266, x3 + 6266, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U72(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x2 + 6266, x3 + 6266, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 1, x2 + 0, x3 + 1, 0) |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | max(0) |
[a__U42(x1)] | = | 0 |
[U33(x1, x2, x3)] | = | max(0) |
[U14(x1, x2, x3)] | = | max(x2 + 0, x3 + 1, 0) |
[a__U12(x1, x2, x3)] | = | max(x2 + 0, x3 + 1, 0) |
[a__U104#(x1, x2, x3)] | = | max(x2 + 6266, x3 + 6266, 0) |
[isNat(x1)] | = | x1 + 0 |
[a__U35(x1, x2)] | = | max(0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 1, 0) |
[U15(x1, x2)] | = | max(x1 + 0, 0) |
[U61(x1, x2)] | = | max(x1 + 0, 0) |
[a__U35#(x1, x2)] | = | max(0) |
[a__U22#(x1, x2)] | = | max(0) |
[a__U13(x1, x2, x3)] | = | max(x2 + 0, x3 + 1, 0) |
[U31(x1, x2, x3)] | = | max(0) |
[a__U83#(x1, x2, x3)] | = | max(x2 + 1, x3 + 2, 0) |
[a__U71(x1, x2)] | = | max(x2 + 0, 0) |
[U92(x1)] | = | 2 |
[a__U92(x1)] | = | 2 |
[a__U61(x1, x2)] | = | max(x1 + 0, 0) |
[U102(x1, x2, x3)] | = | max(x2 + 6264, x3 + 6264, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 1, x2 + 1, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(0) |
[a__U15(x1, x2)] | = | max(x1 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 1, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 0 |
[a__isNat(x1)] | = | x1 + 0 |
[U13(x1, x2, x3)] | = | max(x2 + 0, x3 + 1, 0) |
[a__U23(x1)] | = | x1 + 0 |
[a__isNatKind(x1)] | = | 0 |
[U22(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U51(x1)] | = | x1 + 0 |
[a__U34#(x1, x2, x3)] | = | max(0) |
[a__U103(x1, x2, x3)] | = | max(x2 + 6264, x3 + 6264, 0) |
[U41(x1, x2)] | = | max(x1 + 0, 0) |
[a__U32#(x1, x2, x3)] | = | max(0) |
[a__U101(x1, x2, x3)] | = | max(x2 + 6264, x3 + 6264, 0) |
[a__U91#(x1, x2)] | = | max(0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairmark#(U11(X1,X2,X3)) | → | mark#(X1) | (246) |
The dependency pairs are split into 1 component.
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (226) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (207) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (176) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (221) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
a__U72#(tt,N) | → | mark#(N) | (230) |
mark#(U22(X1,X2)) | → | mark#(X1) | (145) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (224) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (125) |
a__U84#(tt,M,N) | → | mark#(N) | (177) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (236) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(U21(X1,X2)) | → | mark#(X1) | (206) |
mark#(U23(X)) | → | mark#(X) | (213) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (172) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (256) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (166) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (250) |
[a__U83(x1, x2, x3)] | = | max(x1 + 1, x2 + 34850, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 1 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 34850, 0) |
[U16(x1)] | = | 1 |
[U21(x1, x2)] | = | max(x1 + 34848, 0) |
[a__U102(x1, x2, x3)] | = | max(x1 + 46323, x2 + 81173, x3 + 46322, 0) |
[a__U82#(x1, x2, x3)] | = | max(x3 + 95745, 0) |
[a__U15#(x1, x2)] | = | max(0) |
[a__U72#(x1, x2)] | = | max(x1 + 63660, x2 + 95745, 0) |
[a__U71#(x1, x2)] | = | max(x2 + 95745, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | max(x1 + 13213, x2 + 81173, x3 + 46322, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(0) |
[a__U33#(x1, x2, x3)] | = | max(0) |
[a__U33(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | 1 |
[U91(x1, x2)] | = | max(x1 + 28371, 0) |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | max(x1 + 20841, x2 + 34850, x3 + 0, 0) |
[a__U14#(x1, x2, x3)] | = | max(0) |
[U71(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x1 + 17451, x2 + 34850, x3 + 0, 0) |
[a__U62(x1)] | = | 1 |
[U101(x1, x2, x3)] | = | max(x1 + 46324, x2 + 81173, x3 + 46322, 0) |
[a__U13#(x1, x2, x3)] | = | max(0) |
[U103(x1, x2, x3)] | = | max(x1 + 11476, x2 + 81173, x3 + 46322, 0) |
[a__U103#(x1, x2, x3)] | = | max(x2 + 176918, x3 + 142067, 0) |
[U84(x1, x2, x3)] | = | max(x1 + 17451, x2 + 34850, x3 + 0, 0) |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 0 |
[U35(x1, x2)] | = | max(x1 + 0, 0) |
[a__x#(x1, x2)] | = | max(x1 + 142067, x2 + 176918, 0) |
[a__U22(x1, x2)] | = | max(x1 + 34848, 0) |
[U72(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[U34(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U31(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U51(x1)] | = | x1 + 0 |
[a__U81(x1, x2, x3)] | = | max(x2 + 34850, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 46322, x2 + 81173, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U84#(x1, x2, x3)] | = | max(x1 + 95744, x3 + 95745, 0) |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 1 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(x1 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 46322, x2 + 81173, 0) |
[a__U12#(x1, x2, x3)] | = | max(0) |
[U104(x1, x2, x3)] | = | max(x1 + 13213, x2 + 81173, x3 + 46322, 0) |
[a__U14(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U21#(x1, x2)] | = | max(0) |
[a__U81#(x1, x2, x3)] | = | max(x3 + 95745, 0) |
[a__U61#(x1, x2)] | = | max(0) |
[a__U34(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__plus#(x1, x2)] | = | max(x1 + 95745, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 1, x2 + 34850, x3 + 0, 0) |
[mark#(x1)] | = | x1 + 95745 |
[0] | = | 9205 |
[a__U21(x1, x2)] | = | max(x1 + 34848, 0) |
[U36(x1)] | = | 1 |
[a__U32(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U91(x1, x2)] | = | max(x1 + 28371, 0) |
[a__U36(x1)] | = | 1 |
[U62(x1)] | = | 1 |
[a__U102#(x1, x2, x3)] | = | max(x2 + 176918, x3 + 142067, 0) |
[mark(x1)] | = | x1 + 0 |
[a__U72(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x1 + 142068, x2 + 176918, x3 + 142067, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U42(x1)] | = | 1 |
[U33(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[U14(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U12(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U104#(x1, x2, x3)] | = | max(x2 + 176918, x3 + 142067, 0) |
[isNat(x1)] | = | 34849 |
[a__U35(x1, x2)] | = | max(x1 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 34850, 0) |
[U15(x1, x2)] | = | max(x1 + 0, 0) |
[U61(x1, x2)] | = | max(x1 + 0, 0) |
[a__U35#(x1, x2)] | = | max(0) |
[a__U22#(x1, x2)] | = | max(0) |
[a__U13(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[U31(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U83#(x1, x2, x3)] | = | max(x3 + 95745, 0) |
[a__U71(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[U92(x1)] | = | 9205 |
[a__U92(x1)] | = | 9205 |
[a__U61(x1, x2)] | = | max(x1 + 0, 0) |
[U102(x1, x2, x3)] | = | max(x1 + 46323, x2 + 81173, x3 + 46322, 0) |
[U81(x1, x2, x3)] | = | max(x2 + 34850, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(0) |
[a__U15(x1, x2)] | = | max(x1 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 20841, x2 + 34850, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 1 |
[a__isNat(x1)] | = | 34849 |
[U13(x1, x2, x3)] | = | max(x1 + 34848, 0) |
[a__U23(x1)] | = | x1 + 0 |
[a__isNatKind(x1)] | = | 1 |
[U22(x1, x2)] | = | max(x1 + 34848, 0) |
[U51(x1)] | = | x1 + 0 |
[a__U34#(x1, x2, x3)] | = | max(0) |
[a__U103(x1, x2, x3)] | = | max(x1 + 11476, x2 + 81173, x3 + 46322, 0) |
[U41(x1, x2)] | = | max(x1 + 0, 0) |
[a__U32#(x1, x2, x3)] | = | max(0) |
[a__U101(x1, x2, x3)] | = | max(x1 + 46324, x2 + 81173, x3 + 46322, 0) |
[a__U91#(x1, x2)] | = | max(0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(U83(X1,X2,X3)) | → | mark#(X1) | (221) |
mark#(U22(X1,X2)) | → | mark#(X1) | (145) |
mark#(U21(X1,X2)) | → | mark#(X1) | (206) |
The dependency pairs are split into 1 component.
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (226) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (207) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (176) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
a__U72#(tt,N) | → | mark#(N) | (230) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (224) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (125) |
a__U84#(tt,M,N) | → | mark#(N) | (177) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (236) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(U23(X)) | → | mark#(X) | (213) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (172) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (256) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (166) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (250) |
π(U16) | = | 1 |
π(a__U82#) | = | 3 |
π(a__U15#) | = | 2 |
π(a__U72#) | = | 2 |
π(a__U71#) | = | 2 |
π(a__U92#) | = | 1 |
π(a__U23#) | = | 1 |
π(a__isNat#) | = | 1 |
π(a__U14#) | = | 2 |
π(a__U62) | = | 1 |
π(U23) | = | 1 |
π(a__U22) | = | 1 |
π(U34) | = | 1 |
π(a__U31) | = | 1 |
π(a__U51) | = | 1 |
π(a__U84#) | = | 3 |
π(a__U16) | = | 1 |
π(a__U41) | = | 1 |
π(a__U12#) | = | 2 |
π(a__U14) | = | 1 |
π(a__U81#) | = | 3 |
π(a__U34) | = | 1 |
π(a__plus#) | = | 1 |
π(mark#) | = | 1 |
π(U62) | = | 1 |
π(mark) | = | 1 |
π(a__U36#) | = | 1 |
π(U14) | = | 1 |
π(U15) | = | 1 |
π(U61) | = | 1 |
π(a__U35#) | = | 1 |
π(a__U22#) | = | 2 |
π(a__U13) | = | 1 |
π(U31) | = | 1 |
π(a__U83#) | = | 3 |
π(a__U61) | = | 1 |
π(a__U15) | = | 1 |
π(U13) | = | 1 |
π(a__U23) | = | 1 |
π(U22) | = | 1 |
π(U51) | = | 1 |
π(a__U34#) | = | 3 |
π(U41) | = | 1 |
π(a__U32#) | = | 1 |
prec(a__U83) | = | 3 | status(a__U83) | = | [2, 3, 1] | list-extension(a__U83) | = | Lex | ||
prec(a__isNatKind#) | = | 0 | status(a__isNatKind#) | = | [] | list-extension(a__isNatKind#) | = | Lex | ||
prec(isNatKind) | = | 2 | status(isNatKind) | = | [] | list-extension(isNatKind) | = | Lex | ||
prec(a__plus) | = | 3 | status(a__plus) | = | [2, 1] | list-extension(a__plus) | = | Lex | ||
prec(U21) | = | 2 | status(U21) | = | [] | list-extension(U21) | = | Lex | ||
prec(a__U102) | = | 6 | status(a__U102) | = | [3, 2, 1] | list-extension(a__U102) | = | Lex | ||
prec(U11) | = | 2 | status(U11) | = | [] | list-extension(U11) | = | Lex | ||
prec(a__U104) | = | 6 | status(a__U104) | = | [3, 2, 1] | list-extension(a__U104) | = | Lex | ||
prec(s) | = | 2 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__U31#) | = | 0 | status(a__U31#) | = | [2, 3, 1] | list-extension(a__U31#) | = | Lex | ||
prec(a__U33#) | = | 0 | status(a__U33#) | = | [3, 1, 2] | list-extension(a__U33#) | = | Lex | ||
prec(a__U33) | = | 2 | status(a__U33) | = | [] | list-extension(a__U33) | = | Lex | ||
prec(U42) | = | 2 | status(U42) | = | [] | list-extension(U42) | = | Lex | ||
prec(U91) | = | 5 | status(U91) | = | [] | list-extension(U91) | = | Lex | ||
prec(a__U82) | = | 3 | status(a__U82) | = | [2, 3, 1] | list-extension(a__U82) | = | Lex | ||
prec(U71) | = | 3 | status(U71) | = | [1, 2] | list-extension(U71) | = | Lex | ||
prec(a__U84) | = | 3 | status(a__U84) | = | [2, 3, 1] | list-extension(a__U84) | = | Lex | ||
prec(U101) | = | 6 | status(U101) | = | [3, 2, 1] | list-extension(U101) | = | Lex | ||
prec(a__U13#) | = | 0 | status(a__U13#) | = | [2, 3, 1] | list-extension(a__U13#) | = | Lex | ||
prec(U103) | = | 6 | status(U103) | = | [3, 2, 1] | list-extension(U103) | = | Lex | ||
prec(a__U103#) | = | 6 | status(a__U103#) | = | [3, 2, 1] | list-extension(a__U103#) | = | Lex | ||
prec(U84) | = | 3 | status(U84) | = | [2, 3, 1] | list-extension(U84) | = | Lex | ||
prec(a__U51#) | = | 0 | status(a__U51#) | = | [] | list-extension(a__U51#) | = | Lex | ||
prec(U35) | = | 2 | status(U35) | = | [] | list-extension(U35) | = | Lex | ||
prec(a__x#) | = | 6 | status(a__x#) | = | [1, 2] | list-extension(a__x#) | = | Lex | ||
prec(U72) | = | 0 | status(U72) | = | [2] | list-extension(U72) | = | Lex | ||
prec(a__U11#) | = | 0 | status(a__U11#) | = | [] | list-extension(a__U11#) | = | Lex | ||
prec(a__U81) | = | 3 | status(a__U81) | = | [2, 3, 1] | list-extension(a__U81) | = | Lex | ||
prec(a__x) | = | 6 | status(a__x) | = | [1, 2] | list-extension(a__x) | = | Lex | ||
prec(U12) | = | 2 | status(U12) | = | [] | list-extension(U12) | = | Lex | ||
prec(a__U62#) | = | 0 | status(a__U62#) | = | [] | list-extension(a__U62#) | = | Lex | ||
prec(a__U42#) | = | 0 | status(a__U42#) | = | [] | list-extension(a__U42#) | = | Lex | ||
prec(x) | = | 6 | status(x) | = | [1, 2] | list-extension(x) | = | Lex | ||
prec(U104) | = | 6 | status(U104) | = | [3, 2, 1] | list-extension(U104) | = | Lex | ||
prec(a__U21#) | = | 0 | status(a__U21#) | = | [1, 2] | list-extension(a__U21#) | = | Lex | ||
prec(a__U61#) | = | 0 | status(a__U61#) | = | [2, 1] | list-extension(a__U61#) | = | Lex | ||
prec(U83) | = | 3 | status(U83) | = | [2, 3, 1] | list-extension(U83) | = | Lex | ||
prec(0) | = | 5 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__U21) | = | 2 | status(a__U21) | = | [] | list-extension(a__U21) | = | Lex | ||
prec(U36) | = | 2 | status(U36) | = | [] | list-extension(U36) | = | Lex | ||
prec(a__U32) | = | 2 | status(a__U32) | = | [] | list-extension(a__U32) | = | Lex | ||
prec(a__U91) | = | 5 | status(a__U91) | = | [] | list-extension(a__U91) | = | Lex | ||
prec(a__U36) | = | 2 | status(a__U36) | = | [] | list-extension(a__U36) | = | Lex | ||
prec(a__U102#) | = | 6 | status(a__U102#) | = | [3, 2, 1] | list-extension(a__U102#) | = | Lex | ||
prec(a__U72) | = | 0 | status(a__U72) | = | [2] | list-extension(a__U72) | = | Lex | ||
prec(a__U101#) | = | 6 | status(a__U101#) | = | [3, 2, 1] | list-extension(a__U101#) | = | Lex | ||
prec(a__U11) | = | 2 | status(a__U11) | = | [] | list-extension(a__U11) | = | Lex | ||
prec(U32) | = | 2 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(a__U42) | = | 2 | status(a__U42) | = | [] | list-extension(a__U42) | = | Lex | ||
prec(U33) | = | 2 | status(U33) | = | [] | list-extension(U33) | = | Lex | ||
prec(a__U12) | = | 2 | status(a__U12) | = | [] | list-extension(a__U12) | = | Lex | ||
prec(a__U104#) | = | 6 | status(a__U104#) | = | [3, 2] | list-extension(a__U104#) | = | Lex | ||
prec(isNat) | = | 2 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(a__U35) | = | 2 | status(a__U35) | = | [] | list-extension(a__U35) | = | Lex | ||
prec(plus) | = | 3 | status(plus) | = | [2, 1] | list-extension(plus) | = | Lex | ||
prec(a__U71) | = | 3 | status(a__U71) | = | [1, 2] | list-extension(a__U71) | = | Lex | ||
prec(U92) | = | 5 | status(U92) | = | [] | list-extension(U92) | = | Lex | ||
prec(a__U92) | = | 5 | status(a__U92) | = | [] | list-extension(a__U92) | = | Lex | ||
prec(U102) | = | 6 | status(U102) | = | [3, 2, 1] | list-extension(U102) | = | Lex | ||
prec(U81) | = | 3 | status(U81) | = | [2, 3, 1] | list-extension(U81) | = | Lex | ||
prec(a__U41#) | = | 0 | status(a__U41#) | = | [2, 1] | list-extension(a__U41#) | = | Lex | ||
prec(U82) | = | 3 | status(U82) | = | [2, 3, 1] | list-extension(U82) | = | Lex | ||
prec(a__U16#) | = | 0 | status(a__U16#) | = | [] | list-extension(a__U16#) | = | Lex | ||
prec(tt) | = | 2 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(a__isNat) | = | 2 | status(a__isNat) | = | [] | list-extension(a__isNat) | = | Lex | ||
prec(a__isNatKind) | = | 2 | status(a__isNatKind) | = | [] | list-extension(a__isNatKind) | = | Lex | ||
prec(a__U103) | = | 6 | status(a__U103) | = | [3, 2, 1] | list-extension(a__U103) | = | Lex | ||
prec(a__U101) | = | 6 | status(a__U101) | = | [3, 2, 1] | list-extension(a__U101) | = | Lex | ||
prec(a__U91#) | = | 0 | status(a__U91#) | = | [1, 2] | list-extension(a__U91#) | = | Lex |
[a__U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 0 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U21(x1, x2)] | = | max(0) |
[a__U102(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U11(x1, x2, x3)] | = | max(0) |
[a__U104(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U33#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U33(x1, x2, x3)] | = | max(0) |
[U42(x1)] | = | 0 |
[U91(x1, x2)] | = | max(0) |
[a__U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U71(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U101(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U13#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U103(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U103#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U51#(x1)] | = | 0 |
[U35(x1, x2)] | = | max(0) |
[a__x#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U72(x1, x2)] | = | max(x2 + 0, 0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[a__U81(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U12(x1, x2, x3)] | = | max(0) |
[a__U62#(x1)] | = | 0 |
[a__U42#(x1)] | = | 0 |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U104(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U21#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U61#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[0] | = | 0 |
[a__U21(x1, x2)] | = | max(0) |
[U36(x1)] | = | 0 |
[a__U32(x1, x2, x3)] | = | max(0) |
[a__U91(x1, x2)] | = | max(0) |
[a__U36(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U72(x1, x2)] | = | max(x2 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U11(x1, x2, x3)] | = | max(0) |
[U32(x1, x2, x3)] | = | max(0) |
[a__U42(x1)] | = | 0 |
[U33(x1, x2, x3)] | = | max(0) |
[a__U12(x1, x2, x3)] | = | max(0) |
[a__U104#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[isNat(x1)] | = | 0 |
[a__U35(x1, x2)] | = | max(0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U71(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U92(x1)] | = | 0 |
[a__U92(x1)] | = | 0 |
[U102(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 0 |
[a__isNat(x1)] | = | 0 |
[a__isNatKind(x1)] | = | 0 |
[a__U103(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U101(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U91#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (234) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (203) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (251) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (183) |
mark#(s(X)) | → | mark#(X) | (144) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (150) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (157) |
mark#(plus(X1,X2)) | → | mark#(X1) | (138) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (127) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (219) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (239) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (231) |
The dependency pairs are split into 2 components.
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
π(U21) | = | 1 |
π(a__U15#) | = | 2 |
π(a__U92#) | = | 1 |
π(a__U23#) | = | 1 |
π(U42) | = | 1 |
π(a__isNat#) | = | 1 |
π(a__U14#) | = | 2 |
π(U71) | = | 2 |
π(a__U62) | = | 1 |
π(a__U103#) | = | 2 |
π(U23) | = | 1 |
π(a__x#) | = | 2 |
π(a__U22) | = | 1 |
π(U72) | = | 2 |
π(U34) | = | 1 |
π(a__U31) | = | 1 |
π(a__U51) | = | 1 |
π(U12) | = | 1 |
π(a__U34) | = | 1 |
π(a__plus#) | = | 2 |
π(a__U21) | = | 1 |
π(U36) | = | 1 |
π(a__U32) | = | 1 |
π(a__U36) | = | 1 |
π(U62) | = | 1 |
π(mark) | = | 1 |
π(a__U72) | = | 2 |
π(a__U36#) | = | 1 |
π(U32) | = | 1 |
π(a__U42) | = | 1 |
π(a__U12) | = | 1 |
π(U61) | = | 1 |
π(U31) | = | 1 |
π(a__U71) | = | 2 |
π(U92) | = | 1 |
π(a__U92) | = | 1 |
π(a__U61) | = | 1 |
π(a__U23) | = | 1 |
π(U22) | = | 1 |
π(U51) | = | 1 |
π(a__U34#) | = | 3 |
π(a__U32#) | = | 1 |
prec(a__U83) | = | 7 | status(a__U83) | = | [3, 2, 1] | list-extension(a__U83) | = | Lex | ||
prec(a__isNatKind#) | = | 0 | status(a__isNatKind#) | = | [] | list-extension(a__isNatKind#) | = | Lex | ||
prec(isNatKind) | = | 2 | status(isNatKind) | = | [] | list-extension(isNatKind) | = | Lex | ||
prec(a__plus) | = | 7 | status(a__plus) | = | [1, 2] | list-extension(a__plus) | = | Lex | ||
prec(U16) | = | 2 | status(U16) | = | [] | list-extension(U16) | = | Lex | ||
prec(a__U102) | = | 8 | status(a__U102) | = | [2, 3, 1] | list-extension(a__U102) | = | Lex | ||
prec(a__U82#) | = | 4 | status(a__U82#) | = | [2, 1] | list-extension(a__U82#) | = | Lex | ||
prec(a__U72#) | = | 11 | status(a__U72#) | = | [] | list-extension(a__U72#) | = | Lex | ||
prec(a__U71#) | = | 6 | status(a__U71#) | = | [] | list-extension(a__U71#) | = | Lex | ||
prec(U11) | = | 2 | status(U11) | = | [] | list-extension(U11) | = | Lex | ||
prec(a__U104) | = | 8 | status(a__U104) | = | [2, 3, 1] | list-extension(a__U104) | = | Lex | ||
prec(s) | = | 6 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__U31#) | = | 0 | status(a__U31#) | = | [2, 3, 1] | list-extension(a__U31#) | = | Lex | ||
prec(a__U33#) | = | 0 | status(a__U33#) | = | [3, 1, 2] | list-extension(a__U33#) | = | Lex | ||
prec(a__U33) | = | 2 | status(a__U33) | = | [] | list-extension(a__U33) | = | Lex | ||
prec(U91) | = | 2 | status(U91) | = | [] | list-extension(U91) | = | Lex | ||
prec(a__U82) | = | 7 | status(a__U82) | = | [3, 2, 1] | list-extension(a__U82) | = | Lex | ||
prec(a__U84) | = | 7 | status(a__U84) | = | [3, 2, 1] | list-extension(a__U84) | = | Lex | ||
prec(U101) | = | 8 | status(U101) | = | [2, 3, 1] | list-extension(U101) | = | Lex | ||
prec(a__U13#) | = | 0 | status(a__U13#) | = | [2, 3, 1] | list-extension(a__U13#) | = | Lex | ||
prec(U103) | = | 8 | status(U103) | = | [2, 3, 1] | list-extension(U103) | = | Lex | ||
prec(U84) | = | 7 | status(U84) | = | [3, 2, 1] | list-extension(U84) | = | Lex | ||
prec(a__U51#) | = | 0 | status(a__U51#) | = | [] | list-extension(a__U51#) | = | Lex | ||
prec(U35) | = | 2 | status(U35) | = | [] | list-extension(U35) | = | Lex | ||
prec(a__U11#) | = | 0 | status(a__U11#) | = | [] | list-extension(a__U11#) | = | Lex | ||
prec(a__U81) | = | 7 | status(a__U81) | = | [3, 2, 1] | list-extension(a__U81) | = | Lex | ||
prec(a__x) | = | 8 | status(a__x) | = | [2, 1] | list-extension(a__x) | = | Lex | ||
prec(a__U84#) | = | 3 | status(a__U84#) | = | [2] | list-extension(a__U84#) | = | Lex | ||
prec(a__U62#) | = | 0 | status(a__U62#) | = | [] | list-extension(a__U62#) | = | Lex | ||
prec(a__U16) | = | 2 | status(a__U16) | = | [] | list-extension(a__U16) | = | Lex | ||
prec(a__U42#) | = | 0 | status(a__U42#) | = | [] | list-extension(a__U42#) | = | Lex | ||
prec(a__U41) | = | 2 | status(a__U41) | = | [] | list-extension(a__U41) | = | Lex | ||
prec(x) | = | 8 | status(x) | = | [2, 1] | list-extension(x) | = | Lex | ||
prec(a__U12#) | = | 0 | status(a__U12#) | = | [1] | list-extension(a__U12#) | = | Lex | ||
prec(U104) | = | 8 | status(U104) | = | [2, 3, 1] | list-extension(U104) | = | Lex | ||
prec(a__U14) | = | 2 | status(a__U14) | = | [] | list-extension(a__U14) | = | Lex | ||
prec(a__U21#) | = | 0 | status(a__U21#) | = | [1, 2] | list-extension(a__U21#) | = | Lex | ||
prec(a__U81#) | = | 5 | status(a__U81#) | = | [2] | list-extension(a__U81#) | = | Lex | ||
prec(a__U61#) | = | 0 | status(a__U61#) | = | [2, 1] | list-extension(a__U61#) | = | Lex | ||
prec(U83) | = | 7 | status(U83) | = | [3, 2, 1] | list-extension(U83) | = | Lex | ||
prec(mark#) | = | 11 | status(mark#) | = | [] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 2 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__U91) | = | 2 | status(a__U91) | = | [] | list-extension(a__U91) | = | Lex | ||
prec(a__U102#) | = | 6 | status(a__U102#) | = | [1] | list-extension(a__U102#) | = | Lex | ||
prec(a__U101#) | = | 6 | status(a__U101#) | = | [3] | list-extension(a__U101#) | = | Lex | ||
prec(a__U11) | = | 2 | status(a__U11) | = | [] | list-extension(a__U11) | = | Lex | ||
prec(U33) | = | 2 | status(U33) | = | [] | list-extension(U33) | = | Lex | ||
prec(U14) | = | 2 | status(U14) | = | [] | list-extension(U14) | = | Lex | ||
prec(a__U104#) | = | 6 | status(a__U104#) | = | [1] | list-extension(a__U104#) | = | Lex | ||
prec(isNat) | = | 2 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(a__U35) | = | 2 | status(a__U35) | = | [] | list-extension(a__U35) | = | Lex | ||
prec(plus) | = | 7 | status(plus) | = | [1, 2] | list-extension(plus) | = | Lex | ||
prec(U15) | = | 2 | status(U15) | = | [] | list-extension(U15) | = | Lex | ||
prec(a__U35#) | = | 0 | status(a__U35#) | = | [2] | list-extension(a__U35#) | = | Lex | ||
prec(a__U22#) | = | 0 | status(a__U22#) | = | [2, 1] | list-extension(a__U22#) | = | Lex | ||
prec(a__U13) | = | 2 | status(a__U13) | = | [] | list-extension(a__U13) | = | Lex | ||
prec(a__U83#) | = | 4 | status(a__U83#) | = | [2] | list-extension(a__U83#) | = | Lex | ||
prec(U102) | = | 8 | status(U102) | = | [2, 3, 1] | list-extension(U102) | = | Lex | ||
prec(U81) | = | 7 | status(U81) | = | [3, 2, 1] | list-extension(U81) | = | Lex | ||
prec(a__U41#) | = | 0 | status(a__U41#) | = | [2, 1] | list-extension(a__U41#) | = | Lex | ||
prec(a__U15) | = | 2 | status(a__U15) | = | [] | list-extension(a__U15) | = | Lex | ||
prec(U82) | = | 7 | status(U82) | = | [3, 2, 1] | list-extension(U82) | = | Lex | ||
prec(a__U16#) | = | 0 | status(a__U16#) | = | [] | list-extension(a__U16#) | = | Lex | ||
prec(tt) | = | 2 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(a__isNat) | = | 2 | status(a__isNat) | = | [] | list-extension(a__isNat) | = | Lex | ||
prec(U13) | = | 2 | status(U13) | = | [] | list-extension(U13) | = | Lex | ||
prec(a__isNatKind) | = | 2 | status(a__isNatKind) | = | [] | list-extension(a__isNatKind) | = | Lex | ||
prec(a__U103) | = | 8 | status(a__U103) | = | [2, 3, 1] | list-extension(a__U103) | = | Lex | ||
prec(U41) | = | 2 | status(U41) | = | [] | list-extension(U41) | = | Lex | ||
prec(a__U101) | = | 8 | status(a__U101) | = | [2, 3, 1] | list-extension(a__U101) | = | Lex | ||
prec(a__U91#) | = | 0 | status(a__U91#) | = | [1, 2] | list-extension(a__U91#) | = | Lex |
[a__U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 0 |
[a__plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U16(x1)] | = | 0 |
[a__U102(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U82#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U72#(x1, x2)] | = | max(0) |
[a__U71#(x1, x2)] | = | max(0) |
[U11(x1, x2, x3)] | = | max(0) |
[a__U104(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U33#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U33(x1, x2, x3)] | = | max(0) |
[U91(x1, x2)] | = | max(0) |
[a__U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U84(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U101(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U13#(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) |
[a__U51#(x1)] | = | 0 |
[U35(x1, x2)] | = | max(0) |
[a__U11#(x1, x2, x3)] | = | max(0) |
[a__U81(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U84#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 0 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(0) |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U12#(x1, x2, x3)] | = | max(x1 + 0, 0) |
[U104(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U14(x1, x2, x3)] | = | max(0) |
[a__U21#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U81#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[a__U61#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U83(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[mark#(x1)] | = | 0 |
[0] | = | 0 |
[a__U91(x1, x2)] | = | max(0) |
[a__U102#(x1, x2, x3)] | = | max(x1 + 0, 0) |
[a__U101#(x1, x2, x3)] | = | max(x3 + 0, 0) |
[a__U11(x1, x2, x3)] | = | max(0) |
[U33(x1, x2, x3)] | = | max(0) |
[U14(x1, x2, x3)] | = | max(0) |
[a__U104#(x1, x2, x3)] | = | max(x1 + 0, 0) |
[isNat(x1)] | = | 0 |
[a__U35(x1, x2)] | = | max(0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U15(x1, x2)] | = | max(0) |
[a__U35#(x1, x2)] | = | max(x2 + 0, 0) |
[a__U22#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U13(x1, x2, x3)] | = | max(0) |
[a__U83#(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U102(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U81(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U41#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U15(x1, x2)] | = | max(0) |
[U82(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U16#(x1)] | = | 0 |
[tt] | = | 0 |
[a__isNat(x1)] | = | 0 |
[U13(x1, x2, x3)] | = | max(0) |
[a__isNatKind(x1)] | = | 0 |
[a__U103(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U41(x1, x2)] | = | max(0) |
[a__U101(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[a__U91#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
There are 119 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsa__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (170) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (238) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (262) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (164) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (216) |
The dependency pairs are split into 0 components.
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(U23(X)) | → | mark#(X) | (213) |
[a__U83(x1, x2, x3)] | = | 5 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | x1 + 4 |
[a__plus(x1, x2)] | = | 2 |
[U16(x1)] | = | 9 |
[U21(x1, x2)] | = | 4 |
[a__U102(x1, x2, x3)] | = | x3 + 4 |
[a__U82#(x1, x2, x3)] | = | 0 |
[a__U15#(x1, x2)] | = | 0 |
[a__U72#(x1, x2)] | = | 0 |
[a__U71#(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | x3 + 4 |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | 6 |
[s(x1)] | = | 7 |
[a__U31#(x1, x2, x3)] | = | 0 |
[a__U33#(x1, x2, x3)] | = | 0 |
[a__U33(x1, x2, x3)] | = | x3 + 11 |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | 9 |
[U91(x1, x2)] | = | 2 |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | 4 |
[a__U14#(x1, x2, x3)] | = | 0 |
[U71(x1, x2)] | = | x1 + x2 + 4 |
[a__U84(x1, x2, x3)] | = | x2 + 6 |
[a__U62(x1)] | = | x1 + 2 |
[U101(x1, x2, x3)] | = | x2 + 4 |
[a__U13#(x1, x2, x3)] | = | 0 |
[U103(x1, x2, x3)] | = | 6 |
[a__U103#(x1, x2, x3)] | = | 0 |
[U84(x1, x2, x3)] | = | 7 |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 14 |
[U35(x1, x2)] | = | 8 |
[a__x#(x1, x2)] | = | 0 |
[a__U22(x1, x2)] | = | x1 + x2 + 3 |
[U72(x1, x2)] | = | x1 + 5 |
[a__U11#(x1, x2, x3)] | = | 0 |
[U34(x1, x2, x3)] | = | x1 + 7 |
[a__U31(x1, x2, x3)] | = | 3 |
[a__U51(x1)] | = | 4 |
[a__U81(x1, x2, x3)] | = | 3 |
[a__x(x1, x2)] | = | 2 |
[U12(x1, x2, x3)] | = | x1 + x3 + 5 |
[a__U84#(x1, x2, x3)] | = | 1 |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 8 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | x1 + 1 |
[x(x1, x2)] | = | x1 + 3 |
[a__U12#(x1, x2, x3)] | = | 0 |
[U104(x1, x2, x3)] | = | x2 + x3 + 7 |
[a__U14(x1, x2, x3)] | = | x3 + 6 |
[a__U21#(x1, x2)] | = | 0 |
[a__U81#(x1, x2, x3)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[a__U34(x1, x2, x3)] | = | x2 + 6 |
[a__plus#(x1, x2)] | = | 1 |
[U83(x1, x2, x3)] | = | x1 + x2 + x3 + 6 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 12 |
[a__U21(x1, x2)] | = | x2 + 3 |
[U36(x1)] | = | 9 |
[a__U32(x1, x2, x3)] | = | x1 + 1 |
[a__U91(x1, x2)] | = | x1 + 1 |
[a__U36(x1)] | = | 8 |
[U62(x1)] | = | 3 |
[a__U102#(x1, x2, x3)] | = | 0 |
[mark(x1)] | = | 1 |
[a__U72(x1, x2)] | = | 4 |
[a__U101#(x1, x2, x3)] | = | 0 |
[a__U11(x1, x2, x3)] | = | 3 |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | x2 + 2 |
[a__U42(x1)] | = | x1 + 8 |
[U33(x1, x2, x3)] | = | x1 + x2 + 12 |
[U14(x1, x2, x3)] | = | x2 + 7 |
[a__U12(x1, x2, x3)] | = | 4 |
[a__U104#(x1, x2, x3)] | = | 0 |
[isNat(x1)] | = | x1 + 3 |
[a__U35(x1, x2)] | = | 7 |
[plus(x1, x2)] | = | 3 |
[U15(x1, x2)] | = | x1 + 8 |
[U61(x1, x2)] | = | x1 + 5 |
[a__U35#(x1, x2)] | = | 0 |
[a__U22#(x1, x2)] | = | 0 |
[a__U13(x1, x2, x3)] | = | x2 + 5 |
[U31(x1, x2, x3)] | = | x2 + 4 |
[a__U83#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | 3 |
[U92(x1)] | = | x1 + 12 |
[a__U92(x1)] | = | 11 |
[a__U61(x1, x2)] | = | 4 |
[U102(x1, x2, x3)] | = | x2 + 5 |
[U81(x1, x2, x3)] | = | 4 |
[a__U41#(x1, x2)] | = | 0 |
[a__U15(x1, x2)] | = | x2 + 7 |
[U82(x1, x2, x3)] | = | x1 + x3 + 5 |
[a__U16#(x1)] | = | 0 |
[tt] | = | 9 |
[a__isNat(x1)] | = | 2 |
[U13(x1, x2, x3)] | = | 6 |
[a__U23(x1)] | = | 13 |
[a__isNatKind(x1)] | = | 3 |
[U22(x1, x2)] | = | 4 |
[U51(x1)] | = | x1 + 5 |
[a__U34#(x1, x2, x3)] | = | 0 |
[a__U103(x1, x2, x3)] | = | x3 + 5 |
[U41(x1, x2)] | = | x1 + x2 + 2 |
[a__U32#(x1, x2, x3)] | = | 0 |
[a__U101(x1, x2, x3)] | = | 3 |
[a__U91#(x1, x2)] | = | 0 |
mark#(U41(X1,X2)) | → | mark#(X1) | (210) |
mark#(U51(X)) | → | mark#(X) | (147) |
mark#(U15(X1,X2)) | → | mark#(X1) | (252) |
mark#(U23(X)) | → | mark#(X) | (213) |
The dependency pairs are split into 0 components.
a__U15#(tt,V2) | → | a__isNat#(V2) | (263) |
a__U14#(tt,V1,V2) | → | a__isNat#(V1) | (189) |
a__U32#(tt,V1,V2) | → | a__U33#(a__isNatKind(V2),V1,V2) | (173) |
a__U31#(tt,V1,V2) | → | a__U32#(a__isNatKind(V1),V1,V2) | (169) |
a__U12#(tt,V1,V2) | → | a__U13#(a__isNatKind(V2),V1,V2) | (245) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (243) |
a__U33#(tt,V1,V2) | → | a__U34#(a__isNatKind(V2),V1,V2) | (242) |
a__isNat#(plus(V1,V2)) | → | a__U11#(a__isNatKind(V1),V1,V2) | (162) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (163) |
a__U35#(tt,V2) | → | a__isNat#(V2) | (161) |
a__U14#(tt,V1,V2) | → | a__U15#(a__isNat(V1),V2) | (156) |
a__U34#(tt,V1,V2) | → | a__U35#(a__isNat(V1),V2) | (149) |
a__U13#(tt,V1,V2) | → | a__U14#(a__isNatKind(V2),V1,V2) | (136) |
a__isNat#(x(V1,V2)) | → | a__U31#(a__isNatKind(V1),V1,V2) | (215) |
a__U34#(tt,V1,V2) | → | a__isNat#(V1) | (133) |
a__U11#(tt,V1,V2) | → | a__U12#(a__isNatKind(V1),V1,V2) | (134) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (205) |
[a__U83(x1, x2, x3)] | = | 6 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | x1 + 3 |
[a__plus(x1, x2)] | = | 3 |
[U16(x1)] | = | 9 |
[U21(x1, x2)] | = | 4 |
[a__U102(x1, x2, x3)] | = | x3 + 4 |
[a__U82#(x1, x2, x3)] | = | 0 |
[a__U15#(x1, x2)] | = | x2 + 1 |
[a__U72#(x1, x2)] | = | 0 |
[a__U71#(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | x3 + 4 |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | 6 |
[s(x1)] | = | x1 + 5 |
[a__U31#(x1, x2, x3)] | = | x2 + x3 + 5 |
[a__U33#(x1, x2, x3)] | = | x2 + x3 + 3 |
[a__U33(x1, x2, x3)] | = | x3 + 12 |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | 10 |
[U91(x1, x2)] | = | 2 |
[a__isNat#(x1)] | = | x1 + 0 |
[a__U82(x1, x2, x3)] | = | 5 |
[a__U14#(x1, x2, x3)] | = | x2 + x3 + 2 |
[U71(x1, x2)] | = | x1 + x2 + 5 |
[a__U84(x1, x2, x3)] | = | x2 + 7 |
[a__U62(x1)] | = | x1 + 2 |
[U101(x1, x2, x3)] | = | x2 + 4 |
[a__U13#(x1, x2, x3)] | = | x2 + x3 + 3 |
[U103(x1, x2, x3)] | = | 6 |
[a__U103#(x1, x2, x3)] | = | 0 |
[U84(x1, x2, x3)] | = | 8 |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 14 |
[U35(x1, x2)] | = | 4 |
[a__x#(x1, x2)] | = | 0 |
[a__U22(x1, x2)] | = | x1 + x2 + 3 |
[U72(x1, x2)] | = | x1 + 6 |
[a__U11#(x1, x2, x3)] | = | x2 + x3 + 14734 |
[U34(x1, x2, x3)] | = | x1 + 3 |
[a__U31(x1, x2, x3)] | = | 3 |
[a__U51(x1)] | = | 4 |
[a__U81(x1, x2, x3)] | = | 4 |
[a__x(x1, x2)] | = | 2 |
[U12(x1, x2, x3)] | = | x1 + x3 + 5 |
[a__U84#(x1, x2, x3)] | = | 1 |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 8 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | x1 + 1 |
[x(x1, x2)] | = | x1 + x2 + 6 |
[a__U12#(x1, x2, x3)] | = | x2 + x3 + 14733 |
[U104(x1, x2, x3)] | = | x2 + x3 + 7 |
[a__U14(x1, x2, x3)] | = | x3 + 6 |
[a__U21#(x1, x2)] | = | x2 + 2 |
[a__U81#(x1, x2, x3)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[a__U34(x1, x2, x3)] | = | x2 + 2 |
[a__plus#(x1, x2)] | = | 1 |
[U83(x1, x2, x3)] | = | x1 + x2 + x3 + 7 |
[mark#(x1)] | = | 0 |
[0] | = | 12 |
[a__U21(x1, x2)] | = | x2 + 3 |
[U36(x1)] | = | 5 |
[a__U32(x1, x2, x3)] | = | x1 + 2 |
[a__U91(x1, x2)] | = | x1 + 1 |
[a__U36(x1)] | = | 4 |
[U62(x1)] | = | 3 |
[a__U102#(x1, x2, x3)] | = | 0 |
[mark(x1)] | = | 1 |
[a__U72(x1, x2)] | = | 5 |
[a__U101#(x1, x2, x3)] | = | 0 |
[a__U11(x1, x2, x3)] | = | 3 |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | x2 + 3 |
[a__U42(x1)] | = | x1 + 9 |
[U33(x1, x2, x3)] | = | x1 + x2 + 13 |
[U14(x1, x2, x3)] | = | x2 + 7 |
[a__U12(x1, x2, x3)] | = | 4 |
[a__U104#(x1, x2, x3)] | = | 0 |
[isNat(x1)] | = | x1 + 3 |
[a__U35(x1, x2)] | = | 3 |
[plus(x1, x2)] | = | x1 + x2 + 14735 |
[U15(x1, x2)] | = | x1 + 8 |
[U61(x1, x2)] | = | x1 + 4 |
[a__U35#(x1, x2)] | = | x2 + 1 |
[a__U22#(x1, x2)] | = | x2 + 1 |
[a__U13(x1, x2, x3)] | = | x2 + 5 |
[U31(x1, x2, x3)] | = | x2 + 4 |
[a__U83#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | 4 |
[U92(x1)] | = | x1 + 12 |
[a__U92(x1)] | = | 11 |
[a__U61(x1, x2)] | = | 3 |
[U102(x1, x2, x3)] | = | x2 + 5 |
[U81(x1, x2, x3)] | = | 5 |
[a__U41#(x1, x2)] | = | 0 |
[a__U15(x1, x2)] | = | x2 + 7 |
[U82(x1, x2, x3)] | = | x1 + x3 + 6 |
[a__U16#(x1)] | = | 0 |
[tt] | = | 9 |
[a__isNat(x1)] | = | 2 |
[U13(x1, x2, x3)] | = | 6 |
[a__U23(x1)] | = | 13 |
[a__isNatKind(x1)] | = | 2 |
[U22(x1, x2)] | = | 4 |
[U51(x1)] | = | x1 + 5 |
[a__U34#(x1, x2, x3)] | = | x2 + x3 + 2 |
[a__U103(x1, x2, x3)] | = | x3 + 5 |
[U41(x1, x2)] | = | x1 + x2 + 2 |
[a__U32#(x1, x2, x3)] | = | x2 + x3 + 4 |
[a__U101(x1, x2, x3)] | = | 3 |
[a__U91#(x1, x2)] | = | 0 |
a__U15#(tt,V2) | → | a__isNat#(V2) | (263) |
a__U14#(tt,V1,V2) | → | a__isNat#(V1) | (189) |
a__U32#(tt,V1,V2) | → | a__U33#(a__isNatKind(V2),V1,V2) | (173) |
a__U31#(tt,V1,V2) | → | a__U32#(a__isNatKind(V1),V1,V2) | (169) |
a__U12#(tt,V1,V2) | → | a__U13#(a__isNatKind(V2),V1,V2) | (245) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (243) |
a__U33#(tt,V1,V2) | → | a__U34#(a__isNatKind(V2),V1,V2) | (242) |
a__isNat#(plus(V1,V2)) | → | a__U11#(a__isNatKind(V1),V1,V2) | (162) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (163) |
a__U35#(tt,V2) | → | a__isNat#(V2) | (161) |
a__U14#(tt,V1,V2) | → | a__U15#(a__isNat(V1),V2) | (156) |
a__U34#(tt,V1,V2) | → | a__U35#(a__isNat(V1),V2) | (149) |
a__U13#(tt,V1,V2) | → | a__U14#(a__isNatKind(V2),V1,V2) | (136) |
a__isNat#(x(V1,V2)) | → | a__U31#(a__isNatKind(V1),V1,V2) | (215) |
a__U34#(tt,V1,V2) | → | a__isNat#(V1) | (133) |
a__U11#(tt,V1,V2) | → | a__U12#(a__isNatKind(V1),V1,V2) | (134) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (205) |
The dependency pairs are split into 0 components.
a__isNatKind#(x(V1,V2)) | → | a__isNatKind#(V1) | (180) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (171) |
a__U41#(tt,V2) | → | a__isNatKind#(V2) | (160) |
a__U61#(tt,V2) | → | a__isNatKind#(V2) | (229) |
a__isNatKind#(plus(V1,V2)) | → | a__U41#(a__isNatKind(V1),V2) | (222) |
a__isNatKind#(x(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (217) |
a__isNatKind#(plus(V1,V2)) | → | a__isNatKind#(V1) | (124) |
[a__U83(x1, x2, x3)] | = | 5 |
[a__isNatKind#(x1)] | = | x1 + 0 |
[isNatKind(x1)] | = | x1 + 3 |
[a__plus(x1, x2)] | = | 2 |
[U16(x1)] | = | 9 |
[U21(x1, x2)] | = | 4 |
[a__U102(x1, x2, x3)] | = | x3 + 4 |
[a__U82#(x1, x2, x3)] | = | 0 |
[a__U15#(x1, x2)] | = | 1 |
[a__U72#(x1, x2)] | = | 0 |
[a__U71#(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | x3 + 4 |
[a__U92#(x1)] | = | 0 |
[a__U104(x1, x2, x3)] | = | 6 |
[s(x1)] | = | x1 + 5 |
[a__U31#(x1, x2, x3)] | = | 5 |
[a__U33#(x1, x2, x3)] | = | 3 |
[a__U33(x1, x2, x3)] | = | x3 + 12 |
[a__U23#(x1)] | = | 0 |
[U42(x1)] | = | 10 |
[U91(x1, x2)] | = | 2 |
[a__isNat#(x1)] | = | 0 |
[a__U82(x1, x2, x3)] | = | 4 |
[a__U14#(x1, x2, x3)] | = | 2 |
[U71(x1, x2)] | = | x1 + x2 + 4 |
[a__U84(x1, x2, x3)] | = | x2 + 6 |
[a__U62(x1)] | = | x1 + 2 |
[U101(x1, x2, x3)] | = | x2 + 4 |
[a__U13#(x1, x2, x3)] | = | 3 |
[U103(x1, x2, x3)] | = | 6 |
[a__U103#(x1, x2, x3)] | = | 0 |
[U84(x1, x2, x3)] | = | 7 |
[a__U51#(x1)] | = | 0 |
[U23(x1)] | = | x1 + 14 |
[U35(x1, x2)] | = | 4 |
[a__x#(x1, x2)] | = | 0 |
[a__U22(x1, x2)] | = | x1 + x2 + 3 |
[U72(x1, x2)] | = | x1 + 5 |
[a__U11#(x1, x2, x3)] | = | 14734 |
[U34(x1, x2, x3)] | = | x1 + 3 |
[a__U31(x1, x2, x3)] | = | 3 |
[a__U51(x1)] | = | 3 |
[a__U81(x1, x2, x3)] | = | 3 |
[a__x(x1, x2)] | = | 2 |
[U12(x1, x2, x3)] | = | x1 + x3 + 5 |
[a__U84#(x1, x2, x3)] | = | 1 |
[a__U62#(x1)] | = | 0 |
[a__U16(x1)] | = | 8 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | x1 + 1 |
[x(x1, x2)] | = | x1 + x2 + 6 |
[a__U12#(x1, x2, x3)] | = | 14733 |
[U104(x1, x2, x3)] | = | x2 + x3 + 7 |
[a__U14(x1, x2, x3)] | = | x3 + 6 |
[a__U21#(x1, x2)] | = | 2 |
[a__U81#(x1, x2, x3)] | = | 0 |
[a__U61#(x1, x2)] | = | x2 + 1 |
[a__U34(x1, x2, x3)] | = | x2 + 2 |
[a__plus#(x1, x2)] | = | 1 |
[U83(x1, x2, x3)] | = | x1 + x2 + x3 + 6 |
[mark#(x1)] | = | 0 |
[0] | = | 12 |
[a__U21(x1, x2)] | = | x2 + 3 |
[U36(x1)] | = | 5 |
[a__U32(x1, x2, x3)] | = | x1 + 2 |
[a__U91(x1, x2)] | = | x1 + 1 |
[a__U36(x1)] | = | 4 |
[U62(x1)] | = | 3 |
[a__U102#(x1, x2, x3)] | = | 0 |
[mark(x1)] | = | 1 |
[a__U72(x1, x2)] | = | 4 |
[a__U101#(x1, x2, x3)] | = | 0 |
[a__U11(x1, x2, x3)] | = | 3 |
[a__U36#(x1)] | = | 0 |
[U32(x1, x2, x3)] | = | x2 + 3 |
[a__U42(x1)] | = | x1 + 9 |
[U33(x1, x2, x3)] | = | x1 + x2 + 13 |
[U14(x1, x2, x3)] | = | x2 + 7 |
[a__U12(x1, x2, x3)] | = | 4 |
[a__U104#(x1, x2, x3)] | = | 0 |
[isNat(x1)] | = | x1 + 3 |
[a__U35(x1, x2)] | = | 3 |
[plus(x1, x2)] | = | x1 + x2 + 14734 |
[U15(x1, x2)] | = | x1 + 8 |
[U61(x1, x2)] | = | x1 + 4 |
[a__U35#(x1, x2)] | = | 1 |
[a__U22#(x1, x2)] | = | 1 |
[a__U13(x1, x2, x3)] | = | x2 + 5 |
[U31(x1, x2, x3)] | = | x2 + 4 |
[a__U83#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | 3 |
[U92(x1)] | = | x1 + 12 |
[a__U92(x1)] | = | 11 |
[a__U61(x1, x2)] | = | 3 |
[U102(x1, x2, x3)] | = | x2 + 5 |
[U81(x1, x2, x3)] | = | 4 |
[a__U41#(x1, x2)] | = | x2 + 1 |
[a__U15(x1, x2)] | = | x2 + 7 |
[U82(x1, x2, x3)] | = | x1 + x3 + 5 |
[a__U16#(x1)] | = | 0 |
[tt] | = | 9 |
[a__isNat(x1)] | = | 2 |
[U13(x1, x2, x3)] | = | 6 |
[a__U23(x1)] | = | 13 |
[a__isNatKind(x1)] | = | 2 |
[U22(x1, x2)] | = | 4 |
[U51(x1)] | = | x1 + 4 |
[a__U34#(x1, x2, x3)] | = | 2 |
[a__U103(x1, x2, x3)] | = | x3 + 5 |
[U41(x1, x2)] | = | x1 + x2 + 2 |
[a__U32#(x1, x2, x3)] | = | 4 |
[a__U101(x1, x2, x3)] | = | 3 |
[a__U91#(x1, x2)] | = | 0 |
a__isNatKind#(x(V1,V2)) | → | a__isNatKind#(V1) | (180) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (171) |
a__U41#(tt,V2) | → | a__isNatKind#(V2) | (160) |
a__U61#(tt,V2) | → | a__isNatKind#(V2) | (229) |
a__isNatKind#(plus(V1,V2)) | → | a__U41#(a__isNatKind(V1),V2) | (222) |
a__isNatKind#(x(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (217) |
a__isNatKind#(plus(V1,V2)) | → | a__isNatKind#(V1) | (124) |
The dependency pairs are split into 0 components.