The rewrite relation of the following TRS is considered.
There are 119 ruless (increase limit for explicit display).
The evaluation strategy is innermost.There are 145 ruless (increase limit for explicit display).
The dependency pairs are split into 3 components.
a__U102#(tt,M,N) | → | a__U103#(a__isNat(N),M,N) | (122) |
a__U103#(tt,M,N) | → | a__U104#(a__isNatKind(N),M,N) | (124) |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (126) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (184) |
a__U71#(tt,N) | → | a__U72#(a__isNatKind(N),N) | (158) |
a__U72#(tt,N) | → | mark#(N) | (160) |
mark#(U101(X1,X2,X3)) | → | a__U101#(mark(X1),X2,X3) | (192) |
a__U101#(tt,M,N) | → | a__U102#(a__isNatKind(M),M,N) | (120) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (193) |
mark#(U102(X1,X2,X3)) | → | a__U102#(mark(X1),X2,X3) | (194) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (195) |
mark#(U103(X1,X2,X3)) | → | a__U103#(mark(X1),X2,X3) | (197) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (198) |
mark#(U104(X1,X2,X3)) | → | a__U104#(mark(X1),X2,X3) | (200) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (127) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (190) |
a__U104#(tt,M,N) | → | mark#(N) | (128) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (201) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (202) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (186) |
a__U81#(tt,M,N) | → | a__U82#(a__isNatKind(M),M,N) | (161) |
a__U82#(tt,M,N) | → | a__U83#(a__isNat(N),M,N) | (163) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (165) |
a__U84#(tt,M,N) | → | a__plus#(mark(N),mark(M)) | (167) |
a__U84#(tt,M,N) | → | mark#(N) | (168) |
mark#(plus(X1,X2)) | → | mark#(X1) | (203) |
mark#(plus(X1,X2)) | → | mark#(X2) | (204) |
mark#(x(X1,X2)) | → | a__x#(mark(X1),mark(X2)) | (205) |
mark#(x(X1,X2)) | → | mark#(X1) | (206) |
mark#(x(X1,X2)) | → | mark#(X2) | (207) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (209) |
mark#(U12(X1,X2,X3)) | → | mark#(X1) | (211) |
mark#(U13(X1,X2,X3)) | → | mark#(X1) | (213) |
mark#(U14(X1,X2,X3)) | → | mark#(X1) | (215) |
mark#(U15(X1,X2)) | → | mark#(X1) | (217) |
mark#(U16(X)) | → | mark#(X) | (219) |
mark#(U21(X1,X2)) | → | mark#(X1) | (221) |
mark#(U22(X1,X2)) | → | mark#(X1) | (223) |
mark#(U23(X)) | → | mark#(X) | (225) |
mark#(U31(X1,X2,X3)) | → | mark#(X1) | (227) |
mark#(U32(X1,X2,X3)) | → | mark#(X1) | (229) |
mark#(U33(X1,X2,X3)) | → | mark#(X1) | (231) |
mark#(U34(X1,X2,X3)) | → | mark#(X1) | (233) |
mark#(U35(X1,X2)) | → | mark#(X1) | (235) |
mark#(U36(X)) | → | mark#(X) | (237) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U42(X)) | → | mark#(X) | (241) |
mark#(U51(X)) | → | mark#(X) | (243) |
mark#(U61(X1,X2)) | → | mark#(X1) | (245) |
mark#(U62(X)) | → | mark#(X) | (247) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (248) |
mark#(U71(X1,X2)) | → | mark#(X1) | (249) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (250) |
mark#(U72(X1,X2)) | → | mark#(X1) | (251) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (252) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (253) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (254) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (255) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (256) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (257) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (258) |
a__U84#(tt,M,N) | → | mark#(M) | (169) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (259) |
mark#(U91(X1,X2)) | → | mark#(X1) | (261) |
mark#(U92(X)) | → | mark#(X) | (263) |
mark#(s(X)) | → | mark#(X) | (264) |
a__U104#(tt,M,N) | → | mark#(M) | (129) |
prec(a__U102#) | = | 6 | stat(a__U102#) | = | mul | |
prec(tt) | = | 2 | stat(tt) | = | mul | |
prec(a__U103#) | = | 6 | stat(a__U103#) | = | mul | |
prec(a__isNat) | = | 2 | stat(a__isNat) | = | mul | |
prec(a__U104#) | = | 6 | stat(a__U104#) | = | mul | |
prec(a__isNatKind) | = | 2 | stat(a__isNatKind) | = | mul | |
prec(a__plus#) | = | 3 | stat(a__plus#) | = | mul | |
prec(a__x) | = | 6 | stat(a__x) | = | mul | |
prec(0) | = | 1 | stat(0) | = | mul | |
prec(U101) | = | 6 | stat(U101) | = | mul | |
prec(a__U101#) | = | 6 | stat(a__U101#) | = | mul | |
prec(U102) | = | 6 | stat(U102) | = | mul | |
prec(U103) | = | 6 | stat(U103) | = | mul | |
prec(U104) | = | 6 | stat(U104) | = | mul | |
prec(a__x#) | = | 6 | stat(a__x#) | = | mul | |
prec(s) | = | 4 | stat(s) | = | mul | |
prec(plus) | = | 5 | stat(plus) | = | mul | |
prec(a__U81#) | = | 3 | stat(a__U81#) | = | mul | |
prec(a__U82#) | = | 3 | stat(a__U82#) | = | mul | |
prec(a__U83#) | = | 3 | stat(a__U83#) | = | mul | |
prec(a__U84#) | = | 3 | stat(a__U84#) | = | mul | |
prec(x) | = | 6 | stat(x) | = | mul | |
prec(U71) | = | 0 | stat(U71) | = | mul | |
prec(U72) | = | 0 | stat(U72) | = | mul | |
prec(U81) | = | 5 | stat(U81) | = | mul | |
prec(U82) | = | 5 | stat(U82) | = | mul | |
prec(U83) | = | 5 | stat(U83) | = | mul | |
prec(U84) | = | 5 | stat(U84) | = | mul | |
prec(U91) | = | 2 | stat(U91) | = | mul | |
prec(isNat) | = | 2 | stat(isNat) | = | mul | |
prec(isNatKind) | = | 2 | stat(isNatKind) | = | mul | |
prec(a__U102) | = | 6 | stat(a__U102) | = | mul | |
prec(a__U103) | = | 6 | stat(a__U103) | = | mul | |
prec(a__U104) | = | 6 | stat(a__U104) | = | mul | |
prec(a__plus) | = | 5 | stat(a__plus) | = | mul | |
prec(a__U71) | = | 0 | stat(a__U71) | = | mul | |
prec(a__U72) | = | 0 | stat(a__U72) | = | mul | |
prec(a__U101) | = | 6 | stat(a__U101) | = | mul | |
prec(a__U81) | = | 5 | stat(a__U81) | = | mul | |
prec(a__U82) | = | 5 | stat(a__U82) | = | mul | |
prec(a__U83) | = | 5 | stat(a__U83) | = | mul | |
prec(a__U84) | = | 5 | stat(a__U84) | = | mul | |
prec(a__U91) | = | 2 | stat(a__U91) | = | mul |
π(a__U102#) | = | [1,2,3] |
π(tt) | = | [] |
π(a__U103#) | = | [1,2,3] |
π(a__isNat) | = | [] |
π(a__U104#) | = | [1,2,3] |
π(a__isNatKind) | = | [] |
π(a__plus#) | = | [1,2] |
π(a__x) | = | [1,2] |
π(mark) | = | 1 |
π(0) | = | [] |
π(a__U71#) | = | 2 |
π(a__U72#) | = | 2 |
π(mark#) | = | 1 |
π(U101) | = | [1,2,3] |
π(a__U101#) | = | [1,2,3] |
π(U102) | = | [1,2,3] |
π(U103) | = | [1,2,3] |
π(U104) | = | [1,2,3] |
π(a__x#) | = | [1,2] |
π(s) | = | [1] |
π(plus) | = | [1,2] |
π(a__U81#) | = | [1,2,3] |
π(a__U82#) | = | [1,2,3] |
π(a__U83#) | = | [1,2,3] |
π(a__U84#) | = | [2,3] |
π(x) | = | [1,2] |
π(U11) | = | 1 |
π(U12) | = | 1 |
π(U13) | = | 1 |
π(U14) | = | 1 |
π(U15) | = | 1 |
π(U16) | = | 1 |
π(U21) | = | 1 |
π(U22) | = | 1 |
π(U23) | = | 1 |
π(U31) | = | 1 |
π(U32) | = | 1 |
π(U33) | = | 1 |
π(U34) | = | 1 |
π(U35) | = | 1 |
π(U36) | = | 1 |
π(U41) | = | 1 |
π(U42) | = | 1 |
π(U51) | = | 1 |
π(U61) | = | 1 |
π(U62) | = | 1 |
π(U71) | = | [1,2] |
π(U72) | = | [1,2] |
π(U81) | = | [1,2,3] |
π(U82) | = | [1,2,3] |
π(U83) | = | [1,2,3] |
π(U84) | = | [1,2,3] |
π(U91) | = | [1,2] |
π(U92) | = | 1 |
π(a__U11) | = | 1 |
π(a__U21) | = | 1 |
π(a__U31) | = | 1 |
π(isNat) | = | [] |
π(a__U41) | = | 1 |
π(a__U51) | = | 1 |
π(a__U61) | = | 1 |
π(isNatKind) | = | [] |
π(a__U102) | = | [1,2,3] |
π(a__U103) | = | [1,2,3] |
π(a__U104) | = | [1,2,3] |
π(a__plus) | = | [1,2] |
π(a__U71) | = | [1,2] |
π(a__U72) | = | [1,2] |
π(a__U101) | = | [1,2,3] |
π(a__U12) | = | 1 |
π(a__U13) | = | 1 |
π(a__U14) | = | 1 |
π(a__U15) | = | 1 |
π(a__U16) | = | 1 |
π(a__U22) | = | 1 |
π(a__U23) | = | 1 |
π(a__U32) | = | 1 |
π(a__U33) | = | 1 |
π(a__U34) | = | 1 |
π(a__U35) | = | 1 |
π(a__U36) | = | 1 |
π(a__U42) | = | 1 |
π(a__U62) | = | 1 |
π(a__U81) | = | [1,2,3] |
π(a__U82) | = | [1,2,3] |
π(a__U83) | = | [1,2,3] |
π(a__U84) | = | [1,2,3] |
π(a__U91) | = | [1,2] |
π(a__U92) | = | 1 |
a__U104#(tt,M,N) | → | a__plus#(a__x(mark(N),mark(M)),mark(N)) | (126) |
a__plus#(N,0) | → | a__U71#(a__isNat(N),N) | (184) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (193) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (195) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (198) |
a__U104#(tt,M,N) | → | a__x#(mark(N),mark(M)) | (127) |
a__x#(N,s(M)) | → | a__U101#(a__isNat(M),M,N) | (190) |
a__U104#(tt,M,N) | → | mark#(N) | (128) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (201) |
mark#(plus(X1,X2)) | → | a__plus#(mark(X1),mark(X2)) | (202) |
a__plus#(N,s(M)) | → | a__U81#(a__isNat(M),M,N) | (186) |
a__U83#(tt,M,N) | → | a__U84#(a__isNatKind(N),M,N) | (165) |
a__U84#(tt,M,N) | → | mark#(N) | (168) |
mark#(plus(X1,X2)) | → | mark#(X1) | (203) |
mark#(plus(X1,X2)) | → | mark#(X2) | (204) |
mark#(x(X1,X2)) | → | mark#(X1) | (206) |
mark#(x(X1,X2)) | → | mark#(X2) | (207) |
mark#(U71(X1,X2)) | → | a__U71#(mark(X1),X2) | (248) |
mark#(U71(X1,X2)) | → | mark#(X1) | (249) |
mark#(U72(X1,X2)) | → | a__U72#(mark(X1),X2) | (250) |
mark#(U72(X1,X2)) | → | mark#(X1) | (251) |
mark#(U81(X1,X2,X3)) | → | a__U81#(mark(X1),X2,X3) | (252) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (253) |
mark#(U82(X1,X2,X3)) | → | a__U82#(mark(X1),X2,X3) | (254) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (255) |
mark#(U83(X1,X2,X3)) | → | a__U83#(mark(X1),X2,X3) | (256) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (257) |
mark#(U84(X1,X2,X3)) | → | a__U84#(mark(X1),X2,X3) | (258) |
a__U84#(tt,M,N) | → | mark#(M) | (169) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (259) |
mark#(U91(X1,X2)) | → | mark#(X1) | (261) |
mark#(s(X)) | → | mark#(X) | (264) |
a__U104#(tt,M,N) | → | mark#(M) | (129) |
The dependency pairs are split into 1 component.
mark#(U12(X1,X2,X3)) | → | mark#(X1) | (211) |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (209) |
mark#(U13(X1,X2,X3)) | → | mark#(X1) | (213) |
mark#(U14(X1,X2,X3)) | → | mark#(X1) | (215) |
mark#(U15(X1,X2)) | → | mark#(X1) | (217) |
mark#(U16(X)) | → | mark#(X) | (219) |
mark#(U21(X1,X2)) | → | mark#(X1) | (221) |
mark#(U22(X1,X2)) | → | mark#(X1) | (223) |
mark#(U23(X)) | → | mark#(X) | (225) |
mark#(U31(X1,X2,X3)) | → | mark#(X1) | (227) |
mark#(U32(X1,X2,X3)) | → | mark#(X1) | (229) |
mark#(U33(X1,X2,X3)) | → | mark#(X1) | (231) |
mark#(U34(X1,X2,X3)) | → | mark#(X1) | (233) |
mark#(U35(X1,X2)) | → | mark#(X1) | (235) |
mark#(U36(X)) | → | mark#(X) | (237) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U42(X)) | → | mark#(X) | (241) |
mark#(U51(X)) | → | mark#(X) | (243) |
mark#(U61(X1,X2)) | → | mark#(X1) | (245) |
mark#(U62(X)) | → | mark#(X) | (247) |
mark#(U92(X)) | → | mark#(X) | (263) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
mark#(U12(X1,X2,X3)) | → | mark#(X1) | (211) |
1 | > | 1 | |
mark#(U11(X1,X2,X3)) | → | mark#(X1) | (209) |
1 | > | 1 | |
mark#(U13(X1,X2,X3)) | → | mark#(X1) | (213) |
1 | > | 1 | |
mark#(U14(X1,X2,X3)) | → | mark#(X1) | (215) |
1 | > | 1 | |
mark#(U15(X1,X2)) | → | mark#(X1) | (217) |
1 | > | 1 | |
mark#(U16(X)) | → | mark#(X) | (219) |
1 | > | 1 | |
mark#(U21(X1,X2)) | → | mark#(X1) | (221) |
1 | > | 1 | |
mark#(U22(X1,X2)) | → | mark#(X1) | (223) |
1 | > | 1 | |
mark#(U23(X)) | → | mark#(X) | (225) |
1 | > | 1 | |
mark#(U31(X1,X2,X3)) | → | mark#(X1) | (227) |
1 | > | 1 | |
mark#(U32(X1,X2,X3)) | → | mark#(X1) | (229) |
1 | > | 1 | |
mark#(U33(X1,X2,X3)) | → | mark#(X1) | (231) |
1 | > | 1 | |
mark#(U34(X1,X2,X3)) | → | mark#(X1) | (233) |
1 | > | 1 | |
mark#(U35(X1,X2)) | → | mark#(X1) | (235) |
1 | > | 1 | |
mark#(U36(X)) | → | mark#(X) | (237) |
1 | > | 1 | |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
1 | > | 1 | |
mark#(U42(X)) | → | mark#(X) | (241) |
1 | > | 1 | |
mark#(U51(X)) | → | mark#(X) | (243) |
1 | > | 1 | |
mark#(U61(X1,X2)) | → | mark#(X1) | (245) |
1 | > | 1 | |
mark#(U62(X)) | → | mark#(X) | (247) |
1 | > | 1 | |
mark#(U92(X)) | → | mark#(X) | (263) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U12#(tt,V1,V2) | → | a__U13#(a__isNatKind(V2),V1,V2) | (132) |
a__U13#(tt,V1,V2) | → | a__U14#(a__isNatKind(V2),V1,V2) | (134) |
a__U14#(tt,V1,V2) | → | a__U15#(a__isNat(V1),V2) | (136) |
a__U15#(tt,V2) | → | a__isNat#(V2) | (139) |
a__isNat#(plus(V1,V2)) | → | a__U11#(a__isNatKind(V1),V1,V2) | (172) |
a__U11#(tt,V1,V2) | → | a__U12#(a__isNatKind(V1),V1,V2) | (130) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (174) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (140) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (143) |
a__isNat#(x(V1,V2)) | → | a__U31#(a__isNatKind(V1),V1,V2) | (176) |
a__U31#(tt,V1,V2) | → | a__U32#(a__isNatKind(V1),V1,V2) | (144) |
a__U32#(tt,V1,V2) | → | a__U33#(a__isNatKind(V2),V1,V2) | (146) |
a__U33#(tt,V1,V2) | → | a__U34#(a__isNatKind(V2),V1,V2) | (148) |
a__U34#(tt,V1,V2) | → | a__U35#(a__isNat(V1),V2) | (150) |
a__U35#(tt,V2) | → | a__isNat#(V2) | (153) |
a__U34#(tt,V1,V2) | → | a__isNat#(V1) | (151) |
a__U14#(tt,V1,V2) | → | a__isNat#(V1) | (137) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNat(0) | → | tt | (33) |
a__isNat(plus(V1,V2)) | → | a__U11(a__isNatKind(V1),V1,V2) | (34) |
a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1),V1) | (35) |
a__isNat(x(V1,V2)) | → | a__U31(a__isNatKind(V1),V1,V2) | (36) |
a__isNat(X) | → | isNat(X) | (88) |
a__isNatKind(0) | → | tt | (37) |
a__isNatKind(plus(V1,V2)) | → | a__U41(a__isNatKind(V1),V2) | (38) |
a__isNatKind(s(V1)) | → | a__U51(a__isNatKind(V1)) | (39) |
a__isNatKind(x(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (40) |
a__isNatKind(X) | → | isNatKind(X) | (86) |
a__U31(tt,V1,V2) | → | a__U32(a__isNatKind(V1),V1,V2) | (14) |
a__U31(X1,X2,X3) | → | U31(X1,X2,X3) | (101) |
a__U32(tt,V1,V2) | → | a__U33(a__isNatKind(V2),V1,V2) | (15) |
a__U32(X1,X2,X3) | → | U32(X1,X2,X3) | (102) |
a__U33(tt,V1,V2) | → | a__U34(a__isNatKind(V2),V1,V2) | (16) |
a__U33(X1,X2,X3) | → | U33(X1,X2,X3) | (103) |
a__U34(tt,V1,V2) | → | a__U35(a__isNat(V1),V2) | (17) |
a__U34(X1,X2,X3) | → | U34(X1,X2,X3) | (104) |
a__U35(tt,V2) | → | a__U36(a__isNat(V2)) | (18) |
a__U35(X1,X2) | → | U35(X1,X2) | (105) |
a__U36(tt) | → | tt | (19) |
a__U36(X) | → | U36(X) | (106) |
a__U61(tt,V2) | → | a__U62(a__isNatKind(V2)) | (23) |
a__U61(X1,X2) | → | U61(X1,X2) | (110) |
a__U62(tt) | → | tt | (24) |
a__U62(X) | → | U62(X) | (111) |
a__U51(tt) | → | tt | (22) |
a__U51(X) | → | U51(X) | (109) |
a__U41(tt,V2) | → | a__U42(a__isNatKind(V2)) | (20) |
a__U41(X1,X2) | → | U41(X1,X2) | (107) |
a__U42(tt) | → | tt | (21) |
a__U42(X) | → | U42(X) | (108) |
a__U21(tt,V1) | → | a__U22(a__isNatKind(V1),V1) | (11) |
a__U21(X1,X2) | → | U21(X1,X2) | (98) |
a__U22(tt,V1) | → | a__U23(a__isNat(V1)) | (12) |
a__U22(X1,X2) | → | U22(X1,X2) | (99) |
a__U23(tt) | → | tt | (13) |
a__U23(X) | → | U23(X) | (100) |
a__U11(tt,V1,V2) | → | a__U12(a__isNatKind(V1),V1,V2) | (5) |
a__U11(X1,X2,X3) | → | U11(X1,X2,X3) | (92) |
a__U12(tt,V1,V2) | → | a__U13(a__isNatKind(V2),V1,V2) | (6) |
a__U12(X1,X2,X3) | → | U12(X1,X2,X3) | (93) |
a__U13(tt,V1,V2) | → | a__U14(a__isNatKind(V2),V1,V2) | (7) |
a__U13(X1,X2,X3) | → | U13(X1,X2,X3) | (94) |
a__U14(tt,V1,V2) | → | a__U15(a__isNat(V1),V2) | (8) |
a__U14(X1,X2,X3) | → | U14(X1,X2,X3) | (95) |
a__U15(tt,V2) | → | a__U16(a__isNat(V2)) | (9) |
a__U15(X1,X2) | → | U15(X1,X2) | (96) |
a__U16(tt) | → | tt | (10) |
a__U16(X) | → | U16(X) | (97) |
We restrict the innermost strategy to the following left hand sides.
a__isNatKind(x0) |
a__isNat(x0) |
a__U11(x0,x1,x2) |
a__U12(x0,x1,x2) |
a__U13(x0,x1,x2) |
a__U14(x0,x1,x2) |
a__U15(x0,x1) |
a__U16(x0) |
a__U21(x0,x1) |
a__U22(x0,x1) |
a__U23(x0) |
a__U31(x0,x1,x2) |
a__U32(x0,x1,x2) |
a__U33(x0,x1,x2) |
a__U34(x0,x1,x2) |
a__U35(x0,x1) |
a__U36(x0) |
a__U41(x0,x1) |
a__U42(x0) |
a__U51(x0) |
a__U61(x0,x1) |
a__U62(x0) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
a__U13#(tt,V1,V2) | → | a__U14#(a__isNatKind(V2),V1,V2) | (134) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U11#(tt,V1,V2) | → | a__U12#(a__isNatKind(V1),V1,V2) | (130) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U12#(tt,V1,V2) | → | a__U13#(a__isNatKind(V2),V1,V2) | (132) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U15#(tt,V2) | → | a__isNat#(V2) | (139) |
2 | ≥ | 1 | |
a__U14#(tt,V1,V2) | → | a__U15#(a__isNat(V1),V2) | (136) |
3 | ≥ | 2 | |
a__U14#(tt,V1,V2) | → | a__isNat#(V1) | (137) |
2 | ≥ | 1 | |
a__isNat#(plus(V1,V2)) | → | a__U11#(a__isNatKind(V1),V1,V2) | (172) |
1 | > | 2 | |
1 | > | 3 | |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (140) |
2 | ≥ | 2 | |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (174) |
1 | > | 2 | |
a__isNat#(x(V1,V2)) | → | a__U31#(a__isNatKind(V1),V1,V2) | (176) |
1 | > | 2 | |
1 | > | 3 | |
a__U22#(tt,V1) | → | a__isNat#(V1) | (143) |
2 | ≥ | 1 | |
a__U31#(tt,V1,V2) | → | a__U32#(a__isNatKind(V1),V1,V2) | (144) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U32#(tt,V1,V2) | → | a__U33#(a__isNatKind(V2),V1,V2) | (146) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U33#(tt,V1,V2) | → | a__U34#(a__isNatKind(V2),V1,V2) | (148) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U34#(tt,V1,V2) | → | a__U35#(a__isNat(V1),V2) | (150) |
3 | ≥ | 2 | |
a__U34#(tt,V1,V2) | → | a__isNat#(V1) | (151) |
2 | ≥ | 1 | |
a__U35#(tt,V2) | → | a__isNat#(V2) | (153) |
2 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U41#(tt,V2) | → | a__isNatKind#(V2) | (155) |
a__isNatKind#(plus(V1,V2)) | → | a__U41#(a__isNatKind(V1),V2) | (178) |
a__isNatKind#(plus(V1,V2)) | → | a__isNatKind#(V1) | (179) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (181) |
a__isNatKind#(x(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (182) |
a__U61#(tt,V2) | → | a__isNatKind#(V2) | (157) |
a__isNatKind#(x(V1,V2)) | → | a__isNatKind#(V1) | (183) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNatKind(0) | → | tt | (37) |
a__isNatKind(plus(V1,V2)) | → | a__U41(a__isNatKind(V1),V2) | (38) |
a__isNatKind(s(V1)) | → | a__U51(a__isNatKind(V1)) | (39) |
a__isNatKind(x(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (40) |
a__isNatKind(X) | → | isNatKind(X) | (86) |
a__U61(tt,V2) | → | a__U62(a__isNatKind(V2)) | (23) |
a__U61(X1,X2) | → | U61(X1,X2) | (110) |
a__U62(tt) | → | tt | (24) |
a__U62(X) | → | U62(X) | (111) |
a__U51(tt) | → | tt | (22) |
a__U51(X) | → | U51(X) | (109) |
a__U41(tt,V2) | → | a__U42(a__isNatKind(V2)) | (20) |
a__U41(X1,X2) | → | U41(X1,X2) | (107) |
a__U42(tt) | → | tt | (21) |
a__U42(X) | → | U42(X) | (108) |
We restrict the innermost strategy to the following left hand sides.
a__isNatKind(x0) |
a__U41(x0,x1) |
a__U42(x0) |
a__U51(x0) |
a__U61(x0,x1) |
a__U62(x0) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
a__isNatKind#(plus(V1,V2)) | → | a__U41#(a__isNatKind(V1),V2) | (178) |
1 | > | 2 | |
a__isNatKind#(x(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (182) |
1 | > | 2 | |
a__U41#(tt,V2) | → | a__isNatKind#(V2) | (155) |
2 | ≥ | 1 | |
a__U61#(tt,V2) | → | a__isNatKind#(V2) | (157) |
2 | ≥ | 1 | |
a__isNatKind#(plus(V1,V2)) | → | a__isNatKind#(V1) | (179) |
1 | > | 1 | |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (181) |
1 | > | 1 | |
a__isNatKind#(x(V1,V2)) | → | a__isNatKind#(V1) | (183) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.