The rewrite relation of the following TRS is considered.
There are 119 ruless (increase limit for explicit display).
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) |
[U12(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U11(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U13(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U14(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U15(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U16(x1)] | = | 1 · x1 |
[U21(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U22(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U23(x1)] | = | 1 · x1 |
[U31(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U32(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U33(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U34(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U35(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U36(x1)] | = | 1 · x1 |
[U41(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U42(x1)] | = | 1 · x1 |
[U51(x1)] | = | 1 · x1 |
[U61(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U62(x1)] | = | 1 · x1 |
[U92(x1)] | = | 1 · x1 |
[mark#(x1)] | = | 1 · x1 |
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) |
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) |
[a__isNatKind(x1)] | = | 1 · x1 |
[0] | = | 0 |
[tt] | = | 0 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
[a__U41(x1, x2)] | = | 1 · x1 + 1 · x2 |
[s(x1)] | = | 1 · x1 |
[a__U51(x1)] | = | 1 · x1 |
[x(x1, x2)] | = | 1 · x1 + 1 · x2 |
[a__U61(x1, x2)] | = | 1 · x1 + 1 · x2 |
[isNatKind(x1)] | = | 1 · x1 |
[a__U62(x1)] | = | 1 · x1 |
[U61(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U62(x1)] | = | 1 · x1 |
[U51(x1)] | = | 1 · x1 |
[a__U42(x1)] | = | 1 · x1 |
[U41(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U42(x1)] | = | 1 · x1 |
[a__isNatKind#(x1)] | = | 1 · x1 |
[a__U41#(x1, x2)] | = | 1 · x1 + 1 · x2 |
[a__U61#(x1, x2)] | = | 1 · x1 + 1 · x2 |
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) |
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.