The rewrite relation of the following TRS is considered.
U101(tt,M,N) | → | U102(isNatKind(activate(M)),activate(M),activate(N)) | (1) |
U102(tt,M,N) | → | U103(isNat(activate(N)),activate(M),activate(N)) | (2) |
U103(tt,M,N) | → | U104(isNatKind(activate(N)),activate(M),activate(N)) | (3) |
U104(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
U11(tt,V1,V2) | → | U12(isNatKind(activate(V1)),activate(V1),activate(V2)) | (5) |
U12(tt,V1,V2) | → | U13(isNatKind(activate(V2)),activate(V1),activate(V2)) | (6) |
U13(tt,V1,V2) | → | U14(isNatKind(activate(V2)),activate(V1),activate(V2)) | (7) |
U14(tt,V1,V2) | → | U15(isNat(activate(V1)),activate(V2)) | (8) |
U15(tt,V2) | → | U16(isNat(activate(V2))) | (9) |
U16(tt) | → | tt | (10) |
U21(tt,V1) | → | U22(isNatKind(activate(V1)),activate(V1)) | (11) |
U22(tt,V1) | → | U23(isNat(activate(V1))) | (12) |
U23(tt) | → | tt | (13) |
U31(tt,V1,V2) | → | U32(isNatKind(activate(V1)),activate(V1),activate(V2)) | (14) |
U32(tt,V1,V2) | → | U33(isNatKind(activate(V2)),activate(V1),activate(V2)) | (15) |
U33(tt,V1,V2) | → | U34(isNatKind(activate(V2)),activate(V1),activate(V2)) | (16) |
U34(tt,V1,V2) | → | U35(isNat(activate(V1)),activate(V2)) | (17) |
U35(tt,V2) | → | U36(isNat(activate(V2))) | (18) |
U36(tt) | → | tt | (19) |
U41(tt,V2) | → | U42(isNatKind(activate(V2))) | (20) |
U42(tt) | → | tt | (21) |
U51(tt) | → | tt | (22) |
U61(tt,V2) | → | U62(isNatKind(activate(V2))) | (23) |
U62(tt) | → | tt | (24) |
U71(tt,N) | → | U72(isNatKind(activate(N)),activate(N)) | (25) |
U72(tt,N) | → | activate(N) | (26) |
U81(tt,M,N) | → | U82(isNatKind(activate(M)),activate(M),activate(N)) | (27) |
U82(tt,M,N) | → | U83(isNat(activate(N)),activate(M),activate(N)) | (28) |
U83(tt,M,N) | → | U84(isNatKind(activate(N)),activate(M),activate(N)) | (29) |
U84(tt,M,N) | → | s(plus(activate(N),activate(M))) | (30) |
U91(tt,N) | → | U92(isNatKind(activate(N))) | (31) |
U92(tt) | → | 0 | (32) |
isNat(n__0) | → | tt | (33) |
isNat(n__plus(V1,V2)) | → | U11(isNatKind(activate(V1)),activate(V1),activate(V2)) | (34) |
isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)),activate(V1)) | (35) |
isNat(n__x(V1,V2)) | → | U31(isNatKind(activate(V1)),activate(V1),activate(V2)) | (36) |
isNatKind(n__0) | → | tt | (37) |
isNatKind(n__plus(V1,V2)) | → | U41(isNatKind(activate(V1)),activate(V2)) | (38) |
isNatKind(n__s(V1)) | → | U51(isNatKind(activate(V1))) | (39) |
isNatKind(n__x(V1,V2)) | → | U61(isNatKind(activate(V1)),activate(V2)) | (40) |
plus(N,0) | → | U71(isNat(N),N) | (41) |
plus(N,s(M)) | → | U81(isNat(M),M,N) | (42) |
x(N,0) | → | U91(isNat(N),N) | (43) |
x(N,s(M)) | → | U101(isNat(M),M,N) | (44) |
0 | → | n__0 | (45) |
plus(X1,X2) | → | n__plus(X1,X2) | (46) |
s(X) | → | n__s(X) | (47) |
x(X1,X2) | → | n__x(X1,X2) | (48) |
activate(n__0) | → | 0 | (49) |
activate(n__plus(X1,X2)) | → | plus(activate(X1),activate(X2)) | (50) |
activate(n__s(X)) | → | s(activate(X)) | (51) |
activate(n__x(X1,X2)) | → | x(activate(X1),activate(X2)) | (52) |
activate(X) | → | X | (53) |
There are 129 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
There are 118 ruless (increase limit for explicit display).
prec(U102#) | = | 9 | stat(U102#) | = | lex | |
prec(tt) | = | 7 | stat(tt) | = | mul | |
prec(U103#) | = | 9 | stat(U103#) | = | lex | |
prec(isNat) | = | 7 | stat(isNat) | = | lex | |
prec(U104#) | = | 9 | stat(U104#) | = | lex | |
prec(isNatKind) | = | 7 | stat(isNatKind) | = | lex | |
prec(plus#) | = | 7 | stat(plus#) | = | lex | |
prec(x) | = | 9 | stat(x) | = | lex | |
prec(0) | = | 7 | stat(0) | = | mul | |
prec(U71#) | = | 2 | stat(U71#) | = | mul | |
prec(U72#) | = | 1 | stat(U72#) | = | lex | |
prec(activate#) | = | 1 | stat(activate#) | = | lex | |
prec(n__plus) | = | 7 | stat(n__plus) | = | lex | |
prec(isNat#) | = | 0 | stat(isNat#) | = | lex | |
prec(U11#) | = | 7 | stat(U11#) | = | lex | |
prec(U12#) | = | 3 | stat(U12#) | = | mul | |
prec(U13#) | = | 3 | stat(U13#) | = | mul | |
prec(U14#) | = | 3 | stat(U14#) | = | mul | |
prec(U15#) | = | 3 | stat(U15#) | = | mul | |
prec(U41#) | = | 4 | stat(U41#) | = | mul | |
prec(n__s) | = | 1 | stat(n__s) | = | lex | |
prec(n__x) | = | 9 | stat(n__x) | = | lex | |
prec(x#) | = | 9 | stat(x#) | = | lex | |
prec(U91#) | = | 1 | stat(U91#) | = | lex | |
prec(U61#) | = | 8 | stat(U61#) | = | lex | |
prec(U21#) | = | 1 | stat(U21#) | = | lex | |
prec(U22#) | = | 1 | stat(U22#) | = | lex | |
prec(U31#) | = | 9 | stat(U31#) | = | lex | |
prec(U32#) | = | 7 | stat(U32#) | = | mul | |
prec(U33#) | = | 7 | stat(U33#) | = | mul | |
prec(U34#) | = | 7 | stat(U34#) | = | mul | |
prec(U35#) | = | 1 | stat(U35#) | = | lex | |
prec(s) | = | 1 | stat(s) | = | lex | |
prec(U101#) | = | 9 | stat(U101#) | = | lex | |
prec(U81#) | = | 7 | stat(U81#) | = | lex | |
prec(U82#) | = | 7 | stat(U82#) | = | lex | |
prec(U83#) | = | 7 | stat(U83#) | = | lex | |
prec(U84#) | = | 7 | stat(U84#) | = | lex | |
prec(n__0) | = | 7 | stat(n__0) | = | mul | |
prec(U102) | = | 9 | stat(U102) | = | lex | |
prec(U103) | = | 9 | stat(U103) | = | lex | |
prec(U104) | = | 9 | stat(U104) | = | lex | |
prec(plus) | = | 7 | stat(plus) | = | lex | |
prec(U71) | = | 6 | stat(U71) | = | lex | |
prec(U72) | = | 5 | stat(U72) | = | lex | |
prec(U101) | = | 9 | stat(U101) | = | lex | |
prec(U21) | = | 7 | stat(U21) | = | lex | |
prec(U31) | = | 7 | stat(U31) | = | lex | |
prec(U41) | = | 7 | stat(U41) | = | lex | |
prec(U51) | = | 7 | stat(U51) | = | lex | |
prec(U91) | = | 7 | stat(U91) | = | mul | |
prec(U62) | = | 7 | stat(U62) | = | lex | |
prec(U42) | = | 7 | stat(U42) | = | lex | |
prec(U12) | = | 7 | stat(U12) | = | lex | |
prec(U13) | = | 7 | stat(U13) | = | lex | |
prec(U23) | = | 7 | stat(U23) | = | lex | |
prec(U32) | = | 7 | stat(U32) | = | lex | |
prec(U34) | = | 7 | stat(U34) | = | lex | |
prec(U35) | = | 7 | stat(U35) | = | lex | |
prec(U16) | = | 7 | stat(U16) | = | lex | |
prec(U92) | = | 7 | stat(U92) | = | mul | |
prec(U81) | = | 7 | stat(U81) | = | lex | |
prec(U82) | = | 7 | stat(U82) | = | lex | |
prec(U83) | = | 7 | stat(U83) | = | lex | |
prec(U84) | = | 7 | stat(U84) | = | lex |
π(U102#) | = | [3,2,1] |
π(tt) | = | [] |
π(U103#) | = | [3,2,1] |
π(isNat) | = | [] |
π(activate) | = | 1 |
π(U104#) | = | [3,2,1] |
π(isNatKind) | = | [] |
π(plus#) | = | [2,1] |
π(x) | = | [1,2] |
π(0) | = | [] |
π(U71#) | = | [1,2] |
π(U72#) | = | [2] |
π(activate#) | = | [1] |
π(n__plus) | = | [2,1] |
π(isNat#) | = | [1] |
π(U11#) | = | [3,2] |
π(U12#) | = | [1,2,3] |
π(U13#) | = | [1,2,3] |
π(U14#) | = | [1,2,3] |
π(U15#) | = | [1,2] |
π(isNatKind#) | = | 1 |
π(U41#) | = | [1,2] |
π(n__s) | = | [1] |
π(n__x) | = | [1,2] |
π(x#) | = | [1,2] |
π(U91#) | = | [2] |
π(U61#) | = | [1,2] |
π(U21#) | = | [2] |
π(U22#) | = | [2] |
π(U31#) | = | [2,3] |
π(U32#) | = | [1,2,3] |
π(U33#) | = | [1,2,3] |
π(U34#) | = | [1,2,3] |
π(U35#) | = | [2] |
π(s) | = | [1] |
π(U101#) | = | [3,2,1] |
π(U81#) | = | [2,3,1] |
π(U82#) | = | [2,3,1] |
π(U83#) | = | [2,3,1] |
π(U84#) | = | [2,3] |
π(n__0) | = | [] |
π(U102) | = | [3,2,1] |
π(U103) | = | [3,2,1] |
π(U104) | = | [3,2,1] |
π(plus) | = | [2,1] |
π(U71) | = | [1,2] |
π(U72) | = | [2,1] |
π(U101) | = | [3,2,1] |
π(U11) | = | 1 |
π(U21) | = | [] |
π(U31) | = | [] |
π(U41) | = | [] |
π(U51) | = | [] |
π(U61) | = | 1 |
π(U91) | = | [] |
π(U62) | = | [] |
π(U42) | = | [] |
π(U12) | = | [] |
π(U13) | = | [] |
π(U14) | = | 1 |
π(U15) | = | 1 |
π(U22) | = | 1 |
π(U23) | = | [] |
π(U32) | = | [] |
π(U33) | = | 1 |
π(U34) | = | [] |
π(U35) | = | [] |
π(U36) | = | 1 |
π(U16) | = | [] |
π(U92) | = | [] |
π(U81) | = | [2,3,1] |
π(U82) | = | [2,3,1] |
π(U83) | = | [2,3,1] |
π(U84) | = | [2,3,1] |
There are 101 ruless (increase limit for explicit display).
could be deleted.The dependency pairs are split into 0 components.