MAYBE Problem: U101(tt(),M,N) -> U102(isNatKind(activate(M)),activate(M),activate(N)) U102(tt(),M,N) -> U103(isNat(activate(N)),activate(M),activate(N)) U103(tt(),M,N) -> U104(isNatKind(activate(N)),activate(M),activate(N)) U104(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) U15(tt(),V2) -> U16(isNat(activate(V2))) U16(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V1,V2) -> U32(isNatKind(activate(V1)),activate(V1),activate(V2)) U32(tt(),V1,V2) -> U33(isNatKind(activate(V2)),activate(V1),activate(V2)) U33(tt(),V1,V2) -> U34(isNatKind(activate(V2)),activate(V1),activate(V2)) U34(tt(),V1,V2) -> U35(isNat(activate(V1)),activate(V2)) U35(tt(),V2) -> U36(isNat(activate(V2))) U36(tt()) -> tt() U41(tt(),V2) -> U42(isNatKind(activate(V2))) U42(tt()) -> tt() U51(tt()) -> tt() U61(tt(),V2) -> U62(isNatKind(activate(V2))) U62(tt()) -> tt() U71(tt(),N) -> U72(isNatKind(activate(N)),activate(N)) U72(tt(),N) -> activate(N) U81(tt(),M,N) -> U82(isNatKind(activate(M)),activate(M),activate(N)) U82(tt(),M,N) -> U83(isNat(activate(N)),activate(M),activate(N)) U83(tt(),M,N) -> U84(isNatKind(activate(N)),activate(M),activate(N)) U84(tt(),M,N) -> s(plus(activate(N),activate(M))) U91(tt(),N) -> U92(isNatKind(activate(N))) U92(tt()) -> 0() isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNat(n__x(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__plus(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V2)) isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1))) isNatKind(n__x(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2)) plus(N,0()) -> U71(isNat(N),N) plus(N,s(M)) -> U81(isNat(M),M,N) x(N,0()) -> U91(isNat(N),N) x(N,s(M)) -> U101(isNat(M),M,N) 0() -> n__0() plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) activate(n__0()) -> 0() activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) activate(n__x(X1,X2)) -> x(X1,X2) activate(X) -> X Proof: DP Processor: DPs: U101#(tt(),M,N) -> activate#(N) U101#(tt(),M,N) -> activate#(M) U101#(tt(),M,N) -> isNatKind#(activate(M)) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) U102#(tt(),M,N) -> activate#(M) U102#(tt(),M,N) -> activate#(N) U102#(tt(),M,N) -> isNat#(activate(N)) U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) U103#(tt(),M,N) -> activate#(M) U103#(tt(),M,N) -> activate#(N) U103#(tt(),M,N) -> isNatKind#(activate(N)) U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) U104#(tt(),M,N) -> activate#(M) U104#(tt(),M,N) -> activate#(N) U104#(tt(),M,N) -> x#(activate(N),activate(M)) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) U11#(tt(),V1,V2) -> activate#(V2) U11#(tt(),V1,V2) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) U12#(tt(),V1,V2) -> activate#(V1) U12#(tt(),V1,V2) -> activate#(V2) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) U13#(tt(),V1,V2) -> activate#(V1) U13#(tt(),V1,V2) -> activate#(V2) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) U14#(tt(),V1,V2) -> activate#(V2) U14#(tt(),V1,V2) -> activate#(V1) U14#(tt(),V1,V2) -> isNat#(activate(V1)) U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) U15#(tt(),V2) -> activate#(V2) U15#(tt(),V2) -> isNat#(activate(V2)) U15#(tt(),V2) -> U16#(isNat(activate(V2))) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) U22#(tt(),V1) -> U23#(isNat(activate(V1))) U31#(tt(),V1,V2) -> activate#(V2) U31#(tt(),V1,V2) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) U32#(tt(),V1,V2) -> activate#(V1) U32#(tt(),V1,V2) -> activate#(V2) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) U33#(tt(),V1,V2) -> activate#(V1) U33#(tt(),V1,V2) -> activate#(V2) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) U34#(tt(),V1,V2) -> activate#(V2) U34#(tt(),V1,V2) -> activate#(V1) U34#(tt(),V1,V2) -> isNat#(activate(V1)) U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) U35#(tt(),V2) -> activate#(V2) U35#(tt(),V2) -> isNat#(activate(V2)) U35#(tt(),V2) -> U36#(isNat(activate(V2))) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNatKind#(activate(V2)) U41#(tt(),V2) -> U42#(isNatKind(activate(V2))) U61#(tt(),V2) -> activate#(V2) U61#(tt(),V2) -> isNatKind#(activate(V2)) U61#(tt(),V2) -> U62#(isNatKind(activate(V2))) U71#(tt(),N) -> activate#(N) U71#(tt(),N) -> isNatKind#(activate(N)) U71#(tt(),N) -> U72#(isNatKind(activate(N)),activate(N)) U72#(tt(),N) -> activate#(N) U81#(tt(),M,N) -> activate#(N) U81#(tt(),M,N) -> activate#(M) U81#(tt(),M,N) -> isNatKind#(activate(M)) U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) U82#(tt(),M,N) -> activate#(M) U82#(tt(),M,N) -> activate#(N) U82#(tt(),M,N) -> isNat#(activate(N)) U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) U83#(tt(),M,N) -> activate#(M) U83#(tt(),M,N) -> activate#(N) U83#(tt(),M,N) -> isNatKind#(activate(N)) U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) U84#(tt(),M,N) -> activate#(M) U84#(tt(),M,N) -> activate#(N) U84#(tt(),M,N) -> plus#(activate(N),activate(M)) U84#(tt(),M,N) -> s#(plus(activate(N),activate(M))) U91#(tt(),N) -> activate#(N) U91#(tt(),N) -> isNatKind#(activate(N)) U91#(tt(),N) -> U92#(isNatKind(activate(N))) U92#(tt()) -> 0#() isNat#(n__plus(V1,V2)) -> activate#(V2) isNat#(n__plus(V1,V2)) -> activate#(V1) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) isNat#(n__x(V1,V2)) -> activate#(V2) isNat#(n__x(V1,V2)) -> activate#(V1) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNatKind#(n__x(V1,V2)) -> activate#(V2) isNatKind#(n__x(V1,V2)) -> activate#(V1) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) plus#(N,0()) -> isNat#(N) plus#(N,0()) -> U71#(isNat(N),N) plus#(N,s(M)) -> isNat#(M) plus#(N,s(M)) -> U81#(isNat(M),M,N) x#(N,0()) -> isNat#(N) x#(N,0()) -> U91#(isNat(N),N) x#(N,s(M)) -> isNat#(M) x#(N,s(M)) -> U101#(isNat(M),M,N) activate#(n__0()) -> 0#() activate#(n__plus(X1,X2)) -> plus#(X1,X2) activate#(n__s(X)) -> s#(X) activate#(n__x(X1,X2)) -> x#(X1,X2) TRS: U101(tt(),M,N) -> U102(isNatKind(activate(M)),activate(M),activate(N)) U102(tt(),M,N) -> U103(isNat(activate(N)),activate(M),activate(N)) U103(tt(),M,N) -> U104(isNatKind(activate(N)),activate(M),activate(N)) U104(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) U15(tt(),V2) -> U16(isNat(activate(V2))) U16(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V1,V2) -> U32(isNatKind(activate(V1)),activate(V1),activate(V2)) U32(tt(),V1,V2) -> U33(isNatKind(activate(V2)),activate(V1),activate(V2)) U33(tt(),V1,V2) -> U34(isNatKind(activate(V2)),activate(V1),activate(V2)) U34(tt(),V1,V2) -> U35(isNat(activate(V1)),activate(V2)) U35(tt(),V2) -> U36(isNat(activate(V2))) U36(tt()) -> tt() U41(tt(),V2) -> U42(isNatKind(activate(V2))) U42(tt()) -> tt() U51(tt()) -> tt() U61(tt(),V2) -> U62(isNatKind(activate(V2))) U62(tt()) -> tt() U71(tt(),N) -> U72(isNatKind(activate(N)),activate(N)) U72(tt(),N) -> activate(N) U81(tt(),M,N) -> U82(isNatKind(activate(M)),activate(M),activate(N)) U82(tt(),M,N) -> U83(isNat(activate(N)),activate(M),activate(N)) U83(tt(),M,N) -> U84(isNatKind(activate(N)),activate(M),activate(N)) U84(tt(),M,N) -> s(plus(activate(N),activate(M))) U91(tt(),N) -> U92(isNatKind(activate(N))) U92(tt()) -> 0() isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNat(n__x(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__plus(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V2)) isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1))) isNatKind(n__x(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2)) plus(N,0()) -> U71(isNat(N),N) plus(N,s(M)) -> U81(isNat(M),M,N) x(N,0()) -> U91(isNat(N),N) x(N,s(M)) -> U101(isNat(M),M,N) 0() -> n__0() plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) activate(n__0()) -> 0() activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) activate(n__x(X1,X2)) -> x(X1,X2) activate(X) -> X TDG Processor: DPs: U101#(tt(),M,N) -> activate#(N) U101#(tt(),M,N) -> activate#(M) U101#(tt(),M,N) -> isNatKind#(activate(M)) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) U102#(tt(),M,N) -> activate#(M) U102#(tt(),M,N) -> activate#(N) U102#(tt(),M,N) -> isNat#(activate(N)) U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) U103#(tt(),M,N) -> activate#(M) U103#(tt(),M,N) -> activate#(N) U103#(tt(),M,N) -> isNatKind#(activate(N)) U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) U104#(tt(),M,N) -> activate#(M) U104#(tt(),M,N) -> activate#(N) U104#(tt(),M,N) -> x#(activate(N),activate(M)) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) U11#(tt(),V1,V2) -> activate#(V2) U11#(tt(),V1,V2) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) U12#(tt(),V1,V2) -> activate#(V1) U12#(tt(),V1,V2) -> activate#(V2) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) U13#(tt(),V1,V2) -> activate#(V1) U13#(tt(),V1,V2) -> activate#(V2) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) U14#(tt(),V1,V2) -> activate#(V2) U14#(tt(),V1,V2) -> activate#(V1) U14#(tt(),V1,V2) -> isNat#(activate(V1)) U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) U15#(tt(),V2) -> activate#(V2) U15#(tt(),V2) -> isNat#(activate(V2)) U15#(tt(),V2) -> U16#(isNat(activate(V2))) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) U22#(tt(),V1) -> U23#(isNat(activate(V1))) U31#(tt(),V1,V2) -> activate#(V2) U31#(tt(),V1,V2) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) U32#(tt(),V1,V2) -> activate#(V1) U32#(tt(),V1,V2) -> activate#(V2) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) U33#(tt(),V1,V2) -> activate#(V1) U33#(tt(),V1,V2) -> activate#(V2) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) U34#(tt(),V1,V2) -> activate#(V2) U34#(tt(),V1,V2) -> activate#(V1) U34#(tt(),V1,V2) -> isNat#(activate(V1)) U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) U35#(tt(),V2) -> activate#(V2) U35#(tt(),V2) -> isNat#(activate(V2)) U35#(tt(),V2) -> U36#(isNat(activate(V2))) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNatKind#(activate(V2)) U41#(tt(),V2) -> U42#(isNatKind(activate(V2))) U61#(tt(),V2) -> activate#(V2) U61#(tt(),V2) -> isNatKind#(activate(V2)) U61#(tt(),V2) -> U62#(isNatKind(activate(V2))) U71#(tt(),N) -> activate#(N) U71#(tt(),N) -> isNatKind#(activate(N)) U71#(tt(),N) -> U72#(isNatKind(activate(N)),activate(N)) U72#(tt(),N) -> activate#(N) U81#(tt(),M,N) -> activate#(N) U81#(tt(),M,N) -> activate#(M) U81#(tt(),M,N) -> isNatKind#(activate(M)) U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) U82#(tt(),M,N) -> activate#(M) U82#(tt(),M,N) -> activate#(N) U82#(tt(),M,N) -> isNat#(activate(N)) U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) U83#(tt(),M,N) -> activate#(M) U83#(tt(),M,N) -> activate#(N) U83#(tt(),M,N) -> isNatKind#(activate(N)) U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) U84#(tt(),M,N) -> activate#(M) U84#(tt(),M,N) -> activate#(N) U84#(tt(),M,N) -> plus#(activate(N),activate(M)) U84#(tt(),M,N) -> s#(plus(activate(N),activate(M))) U91#(tt(),N) -> activate#(N) U91#(tt(),N) -> isNatKind#(activate(N)) U91#(tt(),N) -> U92#(isNatKind(activate(N))) U92#(tt()) -> 0#() isNat#(n__plus(V1,V2)) -> activate#(V2) isNat#(n__plus(V1,V2)) -> activate#(V1) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) isNat#(n__x(V1,V2)) -> activate#(V2) isNat#(n__x(V1,V2)) -> activate#(V1) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNatKind#(n__x(V1,V2)) -> activate#(V2) isNatKind#(n__x(V1,V2)) -> activate#(V1) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) plus#(N,0()) -> isNat#(N) plus#(N,0()) -> U71#(isNat(N),N) plus#(N,s(M)) -> isNat#(M) plus#(N,s(M)) -> U81#(isNat(M),M,N) x#(N,0()) -> isNat#(N) x#(N,0()) -> U91#(isNat(N),N) x#(N,s(M)) -> isNat#(M) x#(N,s(M)) -> U101#(isNat(M),M,N) activate#(n__0()) -> 0#() activate#(n__plus(X1,X2)) -> plus#(X1,X2) activate#(n__s(X)) -> s#(X) activate#(n__x(X1,X2)) -> x#(X1,X2) TRS: U101(tt(),M,N) -> U102(isNatKind(activate(M)),activate(M),activate(N)) U102(tt(),M,N) -> U103(isNat(activate(N)),activate(M),activate(N)) U103(tt(),M,N) -> U104(isNatKind(activate(N)),activate(M),activate(N)) U104(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) U15(tt(),V2) -> U16(isNat(activate(V2))) U16(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V1,V2) -> U32(isNatKind(activate(V1)),activate(V1),activate(V2)) U32(tt(),V1,V2) -> U33(isNatKind(activate(V2)),activate(V1),activate(V2)) U33(tt(),V1,V2) -> U34(isNatKind(activate(V2)),activate(V1),activate(V2)) U34(tt(),V1,V2) -> U35(isNat(activate(V1)),activate(V2)) U35(tt(),V2) -> U36(isNat(activate(V2))) U36(tt()) -> tt() U41(tt(),V2) -> U42(isNatKind(activate(V2))) U42(tt()) -> tt() U51(tt()) -> tt() U61(tt(),V2) -> U62(isNatKind(activate(V2))) U62(tt()) -> tt() U71(tt(),N) -> U72(isNatKind(activate(N)),activate(N)) U72(tt(),N) -> activate(N) U81(tt(),M,N) -> U82(isNatKind(activate(M)),activate(M),activate(N)) U82(tt(),M,N) -> U83(isNat(activate(N)),activate(M),activate(N)) U83(tt(),M,N) -> U84(isNatKind(activate(N)),activate(M),activate(N)) U84(tt(),M,N) -> s(plus(activate(N),activate(M))) U91(tt(),N) -> U92(isNatKind(activate(N))) U92(tt()) -> 0() isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNat(n__x(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__plus(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V2)) isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1))) isNatKind(n__x(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2)) plus(N,0()) -> U71(isNat(N),N) plus(N,s(M)) -> U81(isNat(M),M,N) x(N,0()) -> U91(isNat(N),N) x(N,s(M)) -> U101(isNat(M),M,N) 0() -> n__0() plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) activate(n__0()) -> 0() activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) activate(n__x(X1,X2)) -> x(X1,X2) activate(X) -> X graph: U91#(tt(),N) -> U92#(isNatKind(activate(N))) -> U92#(tt()) -> 0#() U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> activate#(V1) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U91#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U91#(tt(),N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U91#(tt(),N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U91#(tt(),N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U91#(tt(),N) -> activate#(N) -> activate#(n__0()) -> 0#() U84#(tt(),M,N) -> plus#(activate(N),activate(M)) -> plus#(N,s(M)) -> U81#(isNat(M),M,N) U84#(tt(),M,N) -> plus#(activate(N),activate(M)) -> plus#(N,s(M)) -> isNat#(M) U84#(tt(),M,N) -> plus#(activate(N),activate(M)) -> plus#(N,0()) -> U71#(isNat(N),N) U84#(tt(),M,N) -> plus#(activate(N),activate(M)) -> plus#(N,0()) -> isNat#(N) U84#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U84#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U84#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U84#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U84#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U84#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U84#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U84#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) -> U84#(tt(),M,N) -> s#(plus(activate(N),activate(M))) U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) -> U84#(tt(),M,N) -> plus#(activate(N),activate(M)) U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) -> U84#(tt(),M,N) -> activate#(N) U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) -> U84#(tt(),M,N) -> activate#(M) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> activate#(V1) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U83#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U83#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U83#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U83#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U83#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U83#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U83#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U83#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U83#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) -> U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) -> U83#(tt(),M,N) -> isNatKind#(activate(N)) U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) -> U83#(tt(),M,N) -> activate#(N) U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) -> U83#(tt(),M,N) -> activate#(M) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> activate#(V1) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U82#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U82#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U82#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U82#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U82#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U82#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U82#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U82#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U82#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) -> U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) -> U82#(tt(),M,N) -> isNat#(activate(N)) U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) -> U82#(tt(),M,N) -> activate#(N) U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) -> U82#(tt(),M,N) -> activate#(M) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__s(V1)) -> activate#(V1) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U81#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U81#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U81#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U81#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U81#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U81#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U81#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U81#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U81#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() U72#(tt(),N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U72#(tt(),N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U72#(tt(),N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U72#(tt(),N) -> activate#(N) -> activate#(n__0()) -> 0#() U71#(tt(),N) -> U72#(isNatKind(activate(N)),activate(N)) -> U72#(tt(),N) -> activate#(N) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> activate#(V1) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U71#(tt(),N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U71#(tt(),N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U71#(tt(),N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U71#(tt(),N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U71#(tt(),N) -> activate#(N) -> activate#(n__0()) -> 0#() U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> activate#(V1) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U61#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U61#(tt(),V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U61#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U61#(tt(),V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U61#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> activate#(V1) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U41#(tt(),V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U41#(tt(),V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U41#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U41#(tt(),V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U41#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__s(V1)) -> activate#(V1) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U35#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U35#(tt(),V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U35#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U35#(tt(),V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U35#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) -> U35#(tt(),V2) -> U36#(isNat(activate(V2))) U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) -> U35#(tt(),V2) -> isNat#(activate(V2)) U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) -> U35#(tt(),V2) -> activate#(V2) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> activate#(V1) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U34#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U34#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U34#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U34#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U34#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U34#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U34#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U34#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U34#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U34#(tt(),V1,V2) -> isNat#(activate(V1)) U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U34#(tt(),V1,V2) -> activate#(V1) U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U34#(tt(),V1,V2) -> activate#(V2) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> activate#(V1) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U33#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U33#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U33#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U33#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U33#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U33#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U33#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U33#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U33#(tt(),V1,V2) -> activate#(V2) U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U33#(tt(),V1,V2) -> activate#(V1) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> activate#(V1) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U32#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U32#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U32#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U32#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U32#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U32#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U32#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U32#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U32#(tt(),V1,V2) -> activate#(V2) U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U32#(tt(),V1,V2) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U31#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U31#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U31#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U31#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U31#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U31#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U31#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U31#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U22#(tt(),V1) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U22#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U22#(tt(),V1) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U22#(tt(),V1) -> activate#(V1) -> activate#(n__0()) -> 0#() U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) -> U22#(tt(),V1) -> U23#(isNat(activate(V1))) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) -> U22#(tt(),V1) -> isNat#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) -> U22#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U21#(tt(),V1) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U21#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U21#(tt(),V1) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U21#(tt(),V1) -> activate#(V1) -> activate#(n__0()) -> 0#() U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__s(V1)) -> activate#(V1) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U15#(tt(),V2) -> isNat#(activate(V2)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U15#(tt(),V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U15#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U15#(tt(),V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U15#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) -> U15#(tt(),V2) -> U16#(isNat(activate(V2))) U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) -> U15#(tt(),V2) -> isNat#(activate(V2)) U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) -> U15#(tt(),V2) -> activate#(V2) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> activate#(V1) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U14#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U14#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U14#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U14#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U14#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U14#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U14#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U14#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U14#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U14#(tt(),V1,V2) -> isNat#(activate(V1)) U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U14#(tt(),V1,V2) -> activate#(V1) U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U14#(tt(),V1,V2) -> activate#(V2) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> activate#(V1) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U13#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U13#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U13#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U13#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U13#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U13#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U13#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U13#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U13#(tt(),V1,V2) -> activate#(V2) U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) -> U13#(tt(),V1,V2) -> activate#(V1) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__s(V1)) -> activate#(V1) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U12#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U12#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U12#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U12#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U12#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U12#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U12#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U12#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U12#(tt(),V1,V2) -> activate#(V2) U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U12#(tt(),V1,V2) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U11#(tt(),V1,V2) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U11#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) U11#(tt(),V1,V2) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U11#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U11#(tt(),V1,V2) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U11#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) U11#(tt(),V1,V2) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U11#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() plus#(N,0()) -> U71#(isNat(N),N) -> U71#(tt(),N) -> U72#(isNatKind(activate(N)),activate(N)) plus#(N,0()) -> U71#(isNat(N),N) -> U71#(tt(),N) -> isNatKind#(activate(N)) plus#(N,0()) -> U71#(isNat(N),N) -> U71#(tt(),N) -> activate#(N) plus#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) plus#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) plus#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> activate#(V1) plus#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> activate#(V2) plus#(N,0()) -> isNat#(N) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) plus#(N,0()) -> isNat#(N) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) plus#(N,0()) -> isNat#(N) -> isNat#(n__s(V1)) -> activate#(V1) plus#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) plus#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) plus#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> activate#(V1) plus#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> activate#(V2) plus#(N,s(M)) -> U81#(isNat(M),M,N) -> U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) plus#(N,s(M)) -> U81#(isNat(M),M,N) -> U81#(tt(),M,N) -> isNatKind#(activate(M)) plus#(N,s(M)) -> U81#(isNat(M),M,N) -> U81#(tt(),M,N) -> activate#(M) plus#(N,s(M)) -> U81#(isNat(M),M,N) -> U81#(tt(),M,N) -> activate#(N) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> activate#(V1) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> activate#(V2) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__s(V1)) -> activate#(V1) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> activate#(V1) plus#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> activate#(V2) x#(N,0()) -> U91#(isNat(N),N) -> U91#(tt(),N) -> U92#(isNatKind(activate(N))) x#(N,0()) -> U91#(isNat(N),N) -> U91#(tt(),N) -> isNatKind#(activate(N)) x#(N,0()) -> U91#(isNat(N),N) -> U91#(tt(),N) -> activate#(N) x#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) x#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) x#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> activate#(V1) x#(N,0()) -> isNat#(N) -> isNat#(n__x(V1,V2)) -> activate#(V2) x#(N,0()) -> isNat#(N) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) x#(N,0()) -> isNat#(N) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) x#(N,0()) -> isNat#(N) -> isNat#(n__s(V1)) -> activate#(V1) x#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) x#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) x#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> activate#(V1) x#(N,0()) -> isNat#(N) -> isNat#(n__plus(V1,V2)) -> activate#(V2) x#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) x#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) x#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> activate#(V1) x#(N,s(M)) -> isNat#(M) -> isNat#(n__x(V1,V2)) -> activate#(V2) x#(N,s(M)) -> isNat#(M) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) x#(N,s(M)) -> isNat#(M) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) x#(N,s(M)) -> isNat#(M) -> isNat#(n__s(V1)) -> activate#(V1) x#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) x#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) x#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> activate#(V1) x#(N,s(M)) -> isNat#(M) -> isNat#(n__plus(V1,V2)) -> activate#(V2) x#(N,s(M)) -> U101#(isNat(M),M,N) -> U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) x#(N,s(M)) -> U101#(isNat(M),M,N) -> U101#(tt(),M,N) -> isNatKind#(activate(M)) x#(N,s(M)) -> U101#(isNat(M),M,N) -> U101#(tt(),M,N) -> activate#(M) x#(N,s(M)) -> U101#(isNat(M),M,N) -> U101#(tt(),M,N) -> activate#(N) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) -> plus#(N,s(M)) -> U81#(isNat(M),M,N) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) -> plus#(N,s(M)) -> isNat#(M) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) -> plus#(N,0()) -> U71#(isNat(N),N) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) -> plus#(N,0()) -> isNat#(N) U104#(tt(),M,N) -> x#(activate(N),activate(M)) -> x#(N,s(M)) -> U101#(isNat(M),M,N) U104#(tt(),M,N) -> x#(activate(N),activate(M)) -> x#(N,s(M)) -> isNat#(M) U104#(tt(),M,N) -> x#(activate(N),activate(M)) -> x#(N,0()) -> U91#(isNat(N),N) U104#(tt(),M,N) -> x#(activate(N),activate(M)) -> x#(N,0()) -> isNat#(N) U104#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U104#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U104#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U104#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U104#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U104#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U104#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U104#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) -> U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) -> U104#(tt(),M,N) -> x#(activate(N),activate(M)) U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) -> U104#(tt(),M,N) -> activate#(N) U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) -> U104#(tt(),M,N) -> activate#(M) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> activate#(V1) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U103#(tt(),M,N) -> isNatKind#(activate(N)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U103#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U103#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U103#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U103#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U103#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U103#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U103#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U103#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U31#(tt(),V1,V2) -> activate#(V1) isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U31#(tt(),V1,V2) -> activate#(V2) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNat#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNat#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isNat#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNat#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNat#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNat#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNat#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNat#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) -> U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) -> U21#(tt(),V1) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) -> U21#(tt(),V1) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U11#(tt(),V1,V2) -> activate#(V1) isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U11#(tt(),V1,V2) -> activate#(V2) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNat#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNat#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isNat#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNat#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNat#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNat#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNat#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNat#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) -> U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) -> U103#(tt(),M,N) -> isNatKind#(activate(N)) U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) -> U103#(tt(),M,N) -> activate#(N) U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) -> U103#(tt(),M,N) -> activate#(M) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> activate#(V1) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__x(V1,V2)) -> activate#(V2) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> activate#(V1) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> activate#(V1) U102#(tt(),M,N) -> isNat#(activate(N)) -> isNat#(n__plus(V1,V2)) -> activate#(V2) U102#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U102#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U102#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U102#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U102#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U102#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U102#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U102#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) -> U61#(tt(),V2) -> U62#(isNatKind(activate(V2))) isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) -> U61#(tt(),V2) -> isNatKind#(activate(V2)) isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) -> U61#(tt(),V2) -> activate#(V2) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNatKind#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNatKind#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isNatKind#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNatKind#(n__x(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNatKind#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNatKind#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNatKind#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNatKind#(n__x(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) -> U41#(tt(),V2) -> U42#(isNatKind(activate(V2))) isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) -> U41#(tt(),V2) -> isNatKind#(activate(V2)) isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) -> U41#(tt(),V2) -> activate#(V2) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) isNatKind#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNatKind#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(X) isNatKind#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNatKind#(n__plus(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNatKind#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__x(X1,X2)) -> x#(X1,X2) isNatKind#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(X) isNatKind#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) isNatKind#(n__plus(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() activate#(n__x(X1,X2)) -> x#(X1,X2) -> x#(N,s(M)) -> U101#(isNat(M),M,N) activate#(n__x(X1,X2)) -> x#(X1,X2) -> x#(N,s(M)) -> isNat#(M) activate#(n__x(X1,X2)) -> x#(X1,X2) -> x#(N,0()) -> U91#(isNat(N),N) activate#(n__x(X1,X2)) -> x#(X1,X2) -> x#(N,0()) -> isNat#(N) activate#(n__plus(X1,X2)) -> plus#(X1,X2) -> plus#(N,s(M)) -> U81#(isNat(M),M,N) activate#(n__plus(X1,X2)) -> plus#(X1,X2) -> plus#(N,s(M)) -> isNat#(M) activate#(n__plus(X1,X2)) -> plus#(X1,X2) -> plus#(N,0()) -> U71#(isNat(N),N) activate#(n__plus(X1,X2)) -> plus#(X1,X2) -> plus#(N,0()) -> isNat#(N) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) -> U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) -> U102#(tt(),M,N) -> isNat#(activate(N)) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) -> U102#(tt(),M,N) -> activate#(N) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) -> U102#(tt(),M,N) -> activate#(M) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> activate#(V1) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__x(V1,V2)) -> activate#(V2) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__s(V1)) -> activate#(V1) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V1) U101#(tt(),M,N) -> isNatKind#(activate(M)) -> isNatKind#(n__plus(V1,V2)) -> activate#(V2) U101#(tt(),M,N) -> activate#(N) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U101#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X) U101#(tt(),M,N) -> activate#(N) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U101#(tt(),M,N) -> activate#(N) -> activate#(n__0()) -> 0#() U101#(tt(),M,N) -> activate#(M) -> activate#(n__x(X1,X2)) -> x#(X1,X2) U101#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X) U101#(tt(),M,N) -> activate#(M) -> activate#(n__plus(X1,X2)) -> plus#(X1,X2) U101#(tt(),M,N) -> activate#(M) -> activate#(n__0()) -> 0#() SCC Processor: #sccs: 1 #rules: 113 #arcs: 666/15376 DPs: U91#(tt(),N) -> isNatKind#(activate(N)) isNatKind#(n__plus(V1,V2)) -> activate#(V2) activate#(n__plus(X1,X2)) -> plus#(X1,X2) plus#(N,0()) -> isNat#(N) isNat#(n__plus(V1,V2)) -> activate#(V2) activate#(n__x(X1,X2)) -> x#(X1,X2) x#(N,0()) -> isNat#(N) isNat#(n__plus(V1,V2)) -> activate#(V1) isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> activate#(V1) isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__plus(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V2)) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNatKind#(activate(V2)) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> activate#(V2) isNatKind#(n__x(V1,V2)) -> activate#(V1) isNatKind#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__x(V1,V2)) -> U61#(isNatKind(activate(V1)),activate(V2)) U61#(tt(),V2) -> activate#(V2) U61#(tt(),V2) -> isNatKind#(activate(V2)) isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) U11#(tt(),V1,V2) -> activate#(V2) U11#(tt(),V1,V2) -> activate#(V1) U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) U12#(tt(),V1,V2) -> activate#(V1) U12#(tt(),V1,V2) -> activate#(V2) U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) U13#(tt(),V1,V2) -> activate#(V1) U13#(tt(),V1,V2) -> activate#(V2) U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) U14#(tt(),V1,V2) -> activate#(V2) U14#(tt(),V1,V2) -> activate#(V1) U14#(tt(),V1,V2) -> isNat#(activate(V1)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) isNat#(n__x(V1,V2)) -> activate#(V2) isNat#(n__x(V1,V2)) -> activate#(V1) isNat#(n__x(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__x(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V1),activate(V2)) U31#(tt(),V1,V2) -> activate#(V2) U31#(tt(),V1,V2) -> activate#(V1) U31#(tt(),V1,V2) -> isNatKind#(activate(V1)) U31#(tt(),V1,V2) -> U32#(isNatKind(activate(V1)),activate(V1),activate(V2)) U32#(tt(),V1,V2) -> activate#(V1) U32#(tt(),V1,V2) -> activate#(V2) U32#(tt(),V1,V2) -> isNatKind#(activate(V2)) U32#(tt(),V1,V2) -> U33#(isNatKind(activate(V2)),activate(V1),activate(V2)) U33#(tt(),V1,V2) -> activate#(V1) U33#(tt(),V1,V2) -> activate#(V2) U33#(tt(),V1,V2) -> isNatKind#(activate(V2)) U33#(tt(),V1,V2) -> U34#(isNatKind(activate(V2)),activate(V1),activate(V2)) U34#(tt(),V1,V2) -> activate#(V2) U34#(tt(),V1,V2) -> activate#(V1) U34#(tt(),V1,V2) -> isNat#(activate(V1)) U34#(tt(),V1,V2) -> U35#(isNat(activate(V1)),activate(V2)) U35#(tt(),V2) -> activate#(V2) U35#(tt(),V2) -> isNat#(activate(V2)) U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) U15#(tt(),V2) -> activate#(V2) U15#(tt(),V2) -> isNat#(activate(V2)) x#(N,0()) -> U91#(isNat(N),N) U91#(tt(),N) -> activate#(N) x#(N,s(M)) -> isNat#(M) x#(N,s(M)) -> U101#(isNat(M),M,N) U101#(tt(),M,N) -> activate#(N) U101#(tt(),M,N) -> activate#(M) U101#(tt(),M,N) -> isNatKind#(activate(M)) U101#(tt(),M,N) -> U102#(isNatKind(activate(M)),activate(M),activate(N)) U102#(tt(),M,N) -> activate#(M) U102#(tt(),M,N) -> activate#(N) U102#(tt(),M,N) -> isNat#(activate(N)) U102#(tt(),M,N) -> U103#(isNat(activate(N)),activate(M),activate(N)) U103#(tt(),M,N) -> activate#(M) U103#(tt(),M,N) -> activate#(N) U103#(tt(),M,N) -> isNatKind#(activate(N)) U103#(tt(),M,N) -> U104#(isNatKind(activate(N)),activate(M),activate(N)) U104#(tt(),M,N) -> activate#(M) U104#(tt(),M,N) -> activate#(N) U104#(tt(),M,N) -> x#(activate(N),activate(M)) U104#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) plus#(N,0()) -> U71#(isNat(N),N) U71#(tt(),N) -> activate#(N) U71#(tt(),N) -> isNatKind#(activate(N)) U71#(tt(),N) -> U72#(isNatKind(activate(N)),activate(N)) U72#(tt(),N) -> activate#(N) plus#(N,s(M)) -> isNat#(M) plus#(N,s(M)) -> U81#(isNat(M),M,N) U81#(tt(),M,N) -> activate#(N) U81#(tt(),M,N) -> activate#(M) U81#(tt(),M,N) -> isNatKind#(activate(M)) U81#(tt(),M,N) -> U82#(isNatKind(activate(M)),activate(M),activate(N)) U82#(tt(),M,N) -> activate#(M) U82#(tt(),M,N) -> activate#(N) U82#(tt(),M,N) -> isNat#(activate(N)) U82#(tt(),M,N) -> U83#(isNat(activate(N)),activate(M),activate(N)) U83#(tt(),M,N) -> activate#(M) U83#(tt(),M,N) -> activate#(N) U83#(tt(),M,N) -> isNatKind#(activate(N)) U83#(tt(),M,N) -> U84#(isNatKind(activate(N)),activate(M),activate(N)) U84#(tt(),M,N) -> activate#(M) U84#(tt(),M,N) -> activate#(N) U84#(tt(),M,N) -> plus#(activate(N),activate(M)) TRS: U101(tt(),M,N) -> U102(isNatKind(activate(M)),activate(M),activate(N)) U102(tt(),M,N) -> U103(isNat(activate(N)),activate(M),activate(N)) U103(tt(),M,N) -> U104(isNatKind(activate(N)),activate(M),activate(N)) U104(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) U15(tt(),V2) -> U16(isNat(activate(V2))) U16(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V1,V2) -> U32(isNatKind(activate(V1)),activate(V1),activate(V2)) U32(tt(),V1,V2) -> U33(isNatKind(activate(V2)),activate(V1),activate(V2)) U33(tt(),V1,V2) -> U34(isNatKind(activate(V2)),activate(V1),activate(V2)) U34(tt(),V1,V2) -> U35(isNat(activate(V1)),activate(V2)) U35(tt(),V2) -> U36(isNat(activate(V2))) U36(tt()) -> tt() U41(tt(),V2) -> U42(isNatKind(activate(V2))) U42(tt()) -> tt() U51(tt()) -> tt() U61(tt(),V2) -> U62(isNatKind(activate(V2))) U62(tt()) -> tt() U71(tt(),N) -> U72(isNatKind(activate(N)),activate(N)) U72(tt(),N) -> activate(N) U81(tt(),M,N) -> U82(isNatKind(activate(M)),activate(M),activate(N)) U82(tt(),M,N) -> U83(isNat(activate(N)),activate(M),activate(N)) U83(tt(),M,N) -> U84(isNatKind(activate(N)),activate(M),activate(N)) U84(tt(),M,N) -> s(plus(activate(N),activate(M))) U91(tt(),N) -> U92(isNatKind(activate(N))) U92(tt()) -> 0() isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNat(n__x(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__plus(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V2)) isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1))) isNatKind(n__x(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2)) plus(N,0()) -> U71(isNat(N),N) plus(N,s(M)) -> U81(isNat(M),M,N) x(N,0()) -> U91(isNat(N),N) x(N,s(M)) -> U101(isNat(M),M,N) 0() -> n__0() plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) activate(n__0()) -> 0() activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) activate(n__x(X1,X2)) -> x(X1,X2) activate(X) -> X Open