MAYBE Time: 0.410292 TRS: { U102(tt(), M, N) -> U103(isNat activate N, activate M, activate N), 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), activate X -> X, 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), U101(tt(), M, N) -> U102(isNatKind activate M, activate M, activate N), U103(tt(), M, N) -> U104(isNatKind activate N, activate M, activate N), 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), U104(tt(), M, N) -> plus(x(activate N, activate M), activate N), plus(N, s M) -> U81(isNat M, M, N), plus(N, 0()) -> U71(isNat N, N), plus(X1, X2) -> n__plus(X1, X2), x(N, s M) -> U101(isNat M, M, N), x(N, 0()) -> U91(isNat N, N), x(X1, X2) -> n__x(X1, X2), U12(tt(), V1, V2) -> U13(isNatKind activate V2, activate V1, activate V2), U11(tt(), V1, V2) -> U12(isNatKind activate V1, 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(), U22(tt(), V1) -> U23 isNat activate V1, U21(tt(), V1) -> U22(isNatKind activate V1, activate V1), U23 tt() -> tt(), U32(tt(), V1, V2) -> U33(isNatKind activate V2, activate V1, activate V2), U31(tt(), V1, V2) -> U32(isNatKind activate V1, 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(), U42 tt() -> tt(), U41(tt(), V2) -> U42 isNatKind activate V2, U51 tt() -> tt(), U62 tt() -> tt(), U61(tt(), V2) -> U62 isNatKind activate V2, U72(tt(), N) -> activate N, U71(tt(), N) -> U72(isNatKind activate N, 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), U83(tt(), M, N) -> U84(isNatKind activate N, activate M, activate N), U84(tt(), M, N) -> s plus(activate N, activate M), s X -> n__s X, U92 tt() -> 0(), U91(tt(), N) -> U92 isNatKind activate N, 0() -> n__0()} DP: DP: { U102#(tt(), M, N) -> activate# M, U102#(tt(), M, N) -> activate# N, U102#(tt(), M, N) -> U103#(isNat activate N, activate M, activate N), U102#(tt(), M, N) -> isNat# activate N, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1, isNatKind# n__plus(V1, V2) -> activate# V2, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2), isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> U51# isNatKind activate V1, isNatKind# n__x(V1, V2) -> isNatKind# activate V1, isNatKind# n__x(V1, V2) -> activate# V1, isNatKind# n__x(V1, V2) -> activate# V2, isNatKind# n__x(V1, V2) -> U61#(isNatKind activate V1, activate V2), 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), U101#(tt(), M, N) -> U102#(isNatKind activate M, activate M, activate N), U101#(tt(), M, N) -> isNatKind# activate M, U101#(tt(), M, N) -> activate# M, U101#(tt(), M, N) -> activate# N, U103#(tt(), M, N) -> isNatKind# activate N, U103#(tt(), M, N) -> activate# M, U103#(tt(), M, N) -> activate# N, U103#(tt(), M, N) -> U104#(isNatKind activate N, activate M, activate N), isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNat# n__plus(V1, V2) -> activate# V1, isNat# n__plus(V1, V2) -> activate# V2, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2), isNat# n__s V1 -> isNatKind# activate V1, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), isNat# n__x(V1, V2) -> isNatKind# activate V1, isNat# n__x(V1, V2) -> activate# V1, isNat# n__x(V1, V2) -> activate# V2, isNat# n__x(V1, V2) -> U31#(isNatKind activate V1, activate V1, activate V2), U104#(tt(), M, N) -> activate# M, U104#(tt(), M, N) -> activate# N, U104#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), U104#(tt(), M, N) -> x#(activate N, activate M), plus#(N, s M) -> isNat# M, plus#(N, s M) -> U81#(isNat M, M, N), plus#(N, 0()) -> isNat# N, plus#(N, 0()) -> U71#(isNat N, N), x#(N, s M) -> U101#(isNat M, M, N), x#(N, s M) -> isNat# M, x#(N, 0()) -> isNat# N, x#(N, 0()) -> U91#(isNat N, N), U12#(tt(), V1, V2) -> isNatKind# activate V2, U12#(tt(), V1, V2) -> activate# V1, U12#(tt(), V1, V2) -> activate# V2, U12#(tt(), V1, V2) -> U13#(isNatKind activate V2, activate V1, activate V2), U11#(tt(), V1, V2) -> isNatKind# activate V1, U11#(tt(), V1, V2) -> activate# V1, U11#(tt(), V1, V2) -> activate# V2, U11#(tt(), V1, V2) -> U12#(isNatKind activate V1, activate V1, activate V2), U13#(tt(), V1, V2) -> isNatKind# activate V2, U13#(tt(), V1, V2) -> activate# V1, U13#(tt(), V1, V2) -> activate# V2, U13#(tt(), V1, V2) -> U14#(isNatKind activate V2, activate V1, activate V2), U14#(tt(), V1, V2) -> activate# V1, U14#(tt(), V1, V2) -> activate# V2, 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, U22#(tt(), V1) -> activate# V1, U22#(tt(), V1) -> isNat# activate V1, U22#(tt(), V1) -> U23# isNat activate V1, U21#(tt(), V1) -> isNatKind# activate V1, U21#(tt(), V1) -> activate# V1, U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U32#(tt(), V1, V2) -> isNatKind# activate V2, U32#(tt(), V1, V2) -> activate# V1, U32#(tt(), V1, V2) -> activate# V2, U32#(tt(), V1, V2) -> U33#(isNatKind activate V2, activate V1, activate V2), U31#(tt(), V1, V2) -> isNatKind# activate V1, U31#(tt(), V1, V2) -> activate# V1, U31#(tt(), V1, V2) -> activate# V2, U31#(tt(), V1, V2) -> U32#(isNatKind activate V1, activate V1, activate V2), U33#(tt(), V1, V2) -> isNatKind# activate V2, U33#(tt(), V1, V2) -> activate# V1, U33#(tt(), V1, V2) -> activate# V2, U33#(tt(), V1, V2) -> U34#(isNatKind activate V2, activate V1, activate V2), U34#(tt(), V1, V2) -> activate# V1, U34#(tt(), V1, V2) -> activate# V2, 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) -> isNatKind# activate V2, U41#(tt(), V2) -> activate# V2, U41#(tt(), V2) -> U42# isNatKind activate V2, U61#(tt(), V2) -> isNatKind# activate V2, U61#(tt(), V2) -> activate# V2, U61#(tt(), V2) -> U62# isNatKind activate V2, U72#(tt(), N) -> activate# N, U71#(tt(), N) -> isNatKind# activate N, U71#(tt(), N) -> activate# N, U71#(tt(), N) -> U72#(isNatKind activate N, 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), U81#(tt(), M, N) -> isNatKind# activate M, U81#(tt(), M, N) -> activate# M, U81#(tt(), M, N) -> activate# N, U81#(tt(), M, N) -> U82#(isNatKind activate M, activate M, activate N), U83#(tt(), M, N) -> isNatKind# activate N, U83#(tt(), M, N) -> activate# M, U83#(tt(), M, N) -> 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), U92# tt() -> 0#(), U91#(tt(), N) -> isNatKind# activate N, U91#(tt(), N) -> activate# N, U91#(tt(), N) -> U92# isNatKind activate N} TRS: { U102(tt(), M, N) -> U103(isNat activate N, activate M, activate N), 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), activate X -> X, 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), U101(tt(), M, N) -> U102(isNatKind activate M, activate M, activate N), U103(tt(), M, N) -> U104(isNatKind activate N, activate M, activate N), 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), U104(tt(), M, N) -> plus(x(activate N, activate M), activate N), plus(N, s M) -> U81(isNat M, M, N), plus(N, 0()) -> U71(isNat N, N), plus(X1, X2) -> n__plus(X1, X2), x(N, s M) -> U101(isNat M, M, N), x(N, 0()) -> U91(isNat N, N), x(X1, X2) -> n__x(X1, X2), U12(tt(), V1, V2) -> U13(isNatKind activate V2, activate V1, activate V2), U11(tt(), V1, V2) -> U12(isNatKind activate V1, 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(), U22(tt(), V1) -> U23 isNat activate V1, U21(tt(), V1) -> U22(isNatKind activate V1, activate V1), U23 tt() -> tt(), U32(tt(), V1, V2) -> U33(isNatKind activate V2, activate V1, activate V2), U31(tt(), V1, V2) -> U32(isNatKind activate V1, 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(), U42 tt() -> tt(), U41(tt(), V2) -> U42 isNatKind activate V2, U51 tt() -> tt(), U62 tt() -> tt(), U61(tt(), V2) -> U62 isNatKind activate V2, U72(tt(), N) -> activate N, U71(tt(), N) -> U72(isNatKind activate N, 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), U83(tt(), M, N) -> U84(isNatKind activate N, activate M, activate N), U84(tt(), M, N) -> s plus(activate N, activate M), s X -> n__s X, U92 tt() -> 0(), U91(tt(), N) -> U92 isNatKind activate N, 0() -> n__0()} UR: { U102(tt(), M, N) -> U103(isNat activate N, activate M, activate N), 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), activate X -> X, 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), U101(tt(), M, N) -> U102(isNatKind activate M, activate M, activate N), U103(tt(), M, N) -> U104(isNatKind activate N, activate M, activate N), 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), U104(tt(), M, N) -> plus(x(activate N, activate M), activate N), plus(N, s M) -> U81(isNat M, M, N), plus(N, 0()) -> U71(isNat N, N), plus(X1, X2) -> n__plus(X1, X2), x(N, s M) -> U101(isNat M, M, N), x(N, 0()) -> U91(isNat N, N), x(X1, X2) -> n__x(X1, X2), U12(tt(), V1, V2) -> U13(isNatKind activate V2, activate V1, activate V2), U11(tt(), V1, V2) -> U12(isNatKind activate V1, 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(), U22(tt(), V1) -> U23 isNat activate V1, U21(tt(), V1) -> U22(isNatKind activate V1, activate V1), U23 tt() -> tt(), U32(tt(), V1, V2) -> U33(isNatKind activate V2, activate V1, activate V2), U31(tt(), V1, V2) -> U32(isNatKind activate V1, 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(), U42 tt() -> tt(), U41(tt(), V2) -> U42 isNatKind activate V2, U51 tt() -> tt(), U62 tt() -> tt(), U61(tt(), V2) -> U62 isNatKind activate V2, U72(tt(), N) -> activate N, U71(tt(), N) -> U72(isNatKind activate N, 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), U83(tt(), M, N) -> U84(isNatKind activate N, activate M, activate N), U84(tt(), M, N) -> s plus(activate N, activate M), s X -> n__s X, U92 tt() -> 0(), U91(tt(), N) -> U92 isNatKind activate N, 0() -> n__0(), a(x, y) -> x, a(x, y) -> y} EDG: { (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (x#(N, s M) -> U101#(isNat M, M, N), U101#(tt(), M, N) -> activate# N) (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) -> isNatKind# activate M) (x#(N, s M) -> U101#(isNat M, M, N), U101#(tt(), M, N) -> U102#(isNatKind activate M, activate M, activate N)) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (U13#(tt(), V1, V2) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# 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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (U32#(tt(), V1, V2) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (U35#(tt(), V2) -> isNat# activate V2, isNat# n__x(V1, V2) -> activate# V1) (U35#(tt(), V2) -> isNat# activate V2, isNat# n__x(V1, V2) -> isNatKind# activate V1) (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 -> activate# V1) (U35#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> isNatKind# 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) -> activate# V2) (U35#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V1) (U35#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> isNatKind# activate V1) (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) -> activate# V2) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__x(V1, V2) -> activate# V1) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__x(V1, V2) -> isNatKind# activate V1) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__s V1 -> U51# isNatKind activate V1) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__s V1 -> activate# V1) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__s V1 -> isNatKind# 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) -> activate# V2) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> activate# V1) (U61#(tt(), V2) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (isNat# n__x(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (U14#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# 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) -> activate# V2) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__x(V1, V2) -> activate# V1) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__x(V1, V2) -> isNatKind# activate V1) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> U51# isNatKind activate V1) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# 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) -> activate# V2) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1) (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (U34#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (U103#(tt(), M, N) -> isNatKind# activate N, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (U82#(tt(), M, N) -> isNat# activate N, isNat# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__x(V1, V2) -> activate# V1) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__x(V1, V2) -> isNatKind# activate V1) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__s V1 -> U51# isNatKind activate V1) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__s V1 -> activate# V1) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__s V1 -> isNatKind# 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) -> activate# V2) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__plus(V1, V2) -> activate# V1) (U91#(tt(), N) -> isNatKind# activate N, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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 -> 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__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (U81#(tt(), M, N) -> isNatKind# activate M, isNatKind# n__plus(V1, V2) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (isNatKind# n__x(V1, V2) -> U61#(isNatKind activate V1, activate V2), U61#(tt(), V2) -> isNatKind# activate V2) (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) -> 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) (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) (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) (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) -> 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) (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) -> activate# N) (plus#(N, 0()) -> U71#(isNat N, N), U71#(tt(), N) -> isNatKind# activate N) (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#()) (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#()) (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) -> activate# V2) (plus#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> activate# V1) (plus#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> isNatKind# activate V1) (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 -> activate# V1) (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNatKind# 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) -> activate# V2) (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1) (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNatKind# activate V1) (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#()) (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#()) (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) -> activate# N) (U102#(tt(), M, N) -> U103#(isNat activate N, activate M, activate N), U103#(tt(), M, N) -> activate# M) (U102#(tt(), M, N) -> U103#(isNat activate N, activate M, 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) -> x#(activate N, activate M)) (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) -> activate# N) (U103#(tt(), M, N) -> U104#(isNatKind activate N, activate M, activate N), U104#(tt(), M, N) -> activate# M) (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) -> activate# V2) (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) -> isNatKind# activate V1) (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) -> activate# V2) (U11#(tt(), V1, V2) -> U12#(isNatKind activate V1, activate V1, activate V2), U12#(tt(), V1, V2) -> activate# V1) (U11#(tt(), V1, V2) -> U12#(isNatKind activate V1, activate V1, activate V2), U12#(tt(), V1, V2) -> isNatKind# 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)) (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) -> U33#(isNatKind activate V2, activate V1, 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) -> 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# V2) (U33#(tt(), V1, V2) -> U34#(isNatKind activate V2, activate V1, activate V2), U34#(tt(), V1, V2) -> activate# V1) (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) (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) (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) (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#()) (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#()) (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) -> activate# V2) (plus#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> activate# V1) (plus#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> isNatKind# activate V1) (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1)) (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> activate# V1) (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> isNatKind# 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) -> activate# V2) (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V1) (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> isNatKind# activate V1) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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#()) (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) -> activate# V1, activate# n__0() -> 0#()) (U33#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U33#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X) (U33#(tt(), V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (U32#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#()) (U32#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U32#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X) (U32#(tt(), V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (U22#(tt(), V1) -> activate# V1, activate# n__0() -> 0#()) (U22#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U22#(tt(), V1) -> activate# V1, activate# n__s X -> s# X) (U22#(tt(), V1) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (U13#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#()) (U13#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X) (U13#(tt(), V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (U12#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#()) (U12#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X) (U12#(tt(), V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#()) (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X) (isNat# n__s V1 -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (isNatKind# n__x(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatKind# n__x(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (isNatKind# n__x(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatKind# n__x(V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2)) (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2)) (U84#(tt(), M, N) -> activate# N, activate# n__0() -> 0#()) (U84#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U84#(tt(), M, N) -> activate# N, activate# n__s X -> s# X) (U84#(tt(), M, N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2)) (U81#(tt(), M, N) -> activate# N, activate# n__0() -> 0#()) (U81#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U81#(tt(), M, N) -> activate# N, activate# n__s X -> s# X) (U81#(tt(), M, N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2)) (U71#(tt(), N) -> activate# N, activate# n__0() -> 0#()) (U71#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U71#(tt(), N) -> activate# N, activate# n__s X -> s# X) (U71#(tt(), N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2)) (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, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (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__s V1 -> U21#(isNatKind activate V1, activate V1)) (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__x(V1, V2) -> U31#(isNatKind activate V1, activate V1, activate V2)) (U104#(tt(), M, N) -> activate# N, activate# n__0() -> 0#()) (U104#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U104#(tt(), M, N) -> activate# N, activate# n__s X -> s# X) (U104#(tt(), M, N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2)) (U101#(tt(), M, N) -> activate# N, activate# n__0() -> 0#()) (U101#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U101#(tt(), M, N) -> activate# N, activate# n__s X -> s# X) (U101#(tt(), M, N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2)) (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()) -> isNat# N) (activate# n__x(X1, X2) -> x#(X1, X2), x#(N, 0()) -> U91#(isNat N, N)) (U83#(tt(), M, N) -> U84#(isNatKind activate N, activate M, activate N), U84#(tt(), M, 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) -> plus#(activate N, activate M)) (U83#(tt(), M, N) -> U84#(isNatKind activate N, activate M, activate N), U84#(tt(), M, N) -> s# plus(activate N, activate M)) (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# M) (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) -> U84#(isNatKind activate N, activate M, activate N)) (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# V1) (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) -> U33#(isNatKind activate V2, activate V1, activate V2)) (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) -> 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) -> U15#(isNat 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# V1) (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) -> U14#(isNatKind activate V2, 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) -> U11#(isNatKind activate V1, activate V1, activate V2), U11#(tt(), V1, V2) -> U12#(isNatKind activate V1, activate V1, activate V2)) (U101#(tt(), M, N) -> U102#(isNatKind activate M, activate M, activate N), U102#(tt(), M, N) -> activate# M) (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) -> 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) (U84#(tt(), M, N) -> activate# M, activate# n__0() -> 0#()) (U84#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U84#(tt(), M, N) -> activate# M, activate# n__s X -> s# X) (U84#(tt(), M, N) -> activate# M, activate# n__x(X1, X2) -> x#(X1, X2)) (U81#(tt(), M, N) -> activate# M, activate# n__0() -> 0#()) (U81#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U81#(tt(), M, N) -> activate# M, activate# n__s X -> s# X) (U81#(tt(), M, N) -> activate# M, activate# n__x(X1, X2) -> x#(X1, X2)) (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) -> isNat# M, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (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__s V1 -> U21#(isNatKind activate V1, activate V1)) (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__x(V1, V2) -> U31#(isNatKind activate V1, activate V1, activate V2)) (U104#(tt(), M, N) -> activate# M, activate# n__0() -> 0#()) (U104#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U104#(tt(), M, N) -> activate# M, activate# n__s X -> s# X) (U104#(tt(), M, N) -> activate# M, activate# n__x(X1, X2) -> x#(X1, X2)) (U101#(tt(), M, N) -> activate# M, activate# n__0() -> 0#()) (U101#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U101#(tt(), M, N) -> activate# M, activate# n__s X -> s# X) (U101#(tt(), M, N) -> activate# M, activate# n__x(X1, X2) -> x#(X1, X2)) (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()) -> U91#(isNat N, N), U91#(tt(), N) -> U92# isNatKind activate N) (U71#(tt(), N) -> U72#(isNatKind activate N, activate N), U72#(tt(), N) -> activate# N) (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> 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) -> U23# isNat activate V1) (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()) -> isNat# N) (U104#(tt(), M, N) -> x#(activate N, activate M), x#(N, 0()) -> U91#(isNat N, N)) (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 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1)) (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) -> U41#(isNatKind activate V1, activate V2), U41#(tt(), V2) -> U42# isNatKind 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) -> isNatKind# activate M, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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) -> isNatKind# activate N, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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) -> isNatKind# activate N, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(isNatKind 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) -> 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__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__s V1 -> U21#(isNatKind activate V1, activate V1)) (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__x(V1, V2) -> U31#(isNatKind activate V1, 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) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(isNatKind 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) -> isNat# activate V1, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (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__s V1 -> U21#(isNatKind activate V1, activate V1)) (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__x(V1, V2) -> U31#(isNatKind activate V1, 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) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(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) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(isNatKind 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) -> isNat# activate V2, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2)) (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__s V1 -> U21#(isNatKind activate V1, activate V1)) (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__x(V1, V2) -> U31#(isNatKind activate V1, 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) -> isNatKind# activate V2, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2)) (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__s V1 -> U51# isNatKind activate V1) (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__x(V1, V2) -> U61#(isNatKind activate V1, activate V2)) (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) -> U81#(isNat M, M, N), U81#(tt(), M, N) -> U82#(isNatKind activate M, activate M, activate N)) (U61#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U61#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U61#(tt(), V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (U35#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U35#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U35#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U35#(tt(), V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (U33#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#()) (U33#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U33#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X) (U33#(tt(), V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (U32#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#()) (U32#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U32#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X) (U32#(tt(), V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (U14#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#()) (U14#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X) (U14#(tt(), V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (U11#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#()) (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X) (U11#(tt(), V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (isNat# n__x(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNat# n__x(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (isNat# n__x(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNat# n__x(V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (isNatKind# n__x(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatKind# n__x(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2)) (isNatKind# n__x(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatKind# n__x(V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2)) (U91#(tt(), N) -> U92# isNatKind activate N, U92# tt() -> 0#()) } STATUS: arrows: 0.956686 SCCS (1): Scc: { U102#(tt(), M, N) -> activate# M, U102#(tt(), M, N) -> activate# N, U102#(tt(), M, N) -> U103#(isNat activate N, activate M, activate N), U102#(tt(), M, N) -> isNat# activate N, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1, isNatKind# n__plus(V1, V2) -> activate# V2, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2), isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__x(V1, V2) -> isNatKind# activate V1, isNatKind# n__x(V1, V2) -> activate# V1, isNatKind# n__x(V1, V2) -> activate# V2, isNatKind# n__x(V1, V2) -> U61#(isNatKind activate V1, activate V2), activate# n__plus(X1, X2) -> plus#(X1, X2), activate# n__x(X1, X2) -> x#(X1, X2), U101#(tt(), M, N) -> U102#(isNatKind activate M, activate M, activate N), U101#(tt(), M, N) -> isNatKind# activate M, U101#(tt(), M, N) -> activate# M, U101#(tt(), M, N) -> activate# N, U103#(tt(), M, N) -> isNatKind# activate N, U103#(tt(), M, N) -> activate# M, U103#(tt(), M, N) -> activate# N, U103#(tt(), M, N) -> U104#(isNatKind activate N, activate M, activate N), isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNat# n__plus(V1, V2) -> activate# V1, isNat# n__plus(V1, V2) -> activate# V2, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2), isNat# n__s V1 -> isNatKind# activate V1, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), isNat# n__x(V1, V2) -> isNatKind# activate V1, isNat# n__x(V1, V2) -> activate# V1, isNat# n__x(V1, V2) -> activate# V2, isNat# n__x(V1, V2) -> U31#(isNatKind activate V1, activate V1, activate V2), U104#(tt(), M, N) -> activate# M, U104#(tt(), M, N) -> activate# N, U104#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), U104#(tt(), M, N) -> x#(activate N, activate M), plus#(N, s M) -> isNat# M, plus#(N, s M) -> U81#(isNat M, M, N), plus#(N, 0()) -> isNat# N, plus#(N, 0()) -> U71#(isNat N, N), x#(N, s M) -> U101#(isNat M, M, N), x#(N, s M) -> isNat# M, x#(N, 0()) -> isNat# N, x#(N, 0()) -> U91#(isNat N, N), U12#(tt(), V1, V2) -> isNatKind# activate V2, U12#(tt(), V1, V2) -> activate# V1, U12#(tt(), V1, V2) -> activate# V2, U12#(tt(), V1, V2) -> U13#(isNatKind activate V2, activate V1, activate V2), U11#(tt(), V1, V2) -> isNatKind# activate V1, U11#(tt(), V1, V2) -> activate# V1, U11#(tt(), V1, V2) -> activate# V2, U11#(tt(), V1, V2) -> U12#(isNatKind activate V1, activate V1, activate V2), U13#(tt(), V1, V2) -> isNatKind# activate V2, U13#(tt(), V1, V2) -> activate# V1, U13#(tt(), V1, V2) -> activate# V2, U13#(tt(), V1, V2) -> U14#(isNatKind activate V2, activate V1, activate V2), U14#(tt(), V1, V2) -> activate# V1, U14#(tt(), V1, V2) -> activate# V2, 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, U22#(tt(), V1) -> activate# V1, U22#(tt(), V1) -> isNat# activate V1, U21#(tt(), V1) -> isNatKind# activate V1, U21#(tt(), V1) -> activate# V1, U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U32#(tt(), V1, V2) -> isNatKind# activate V2, U32#(tt(), V1, V2) -> activate# V1, U32#(tt(), V1, V2) -> activate# V2, U32#(tt(), V1, V2) -> U33#(isNatKind activate V2, activate V1, activate V2), U31#(tt(), V1, V2) -> isNatKind# activate V1, U31#(tt(), V1, V2) -> activate# V1, U31#(tt(), V1, V2) -> activate# V2, U31#(tt(), V1, V2) -> U32#(isNatKind activate V1, activate V1, activate V2), U33#(tt(), V1, V2) -> isNatKind# activate V2, U33#(tt(), V1, V2) -> activate# V1, U33#(tt(), V1, V2) -> activate# V2, U33#(tt(), V1, V2) -> U34#(isNatKind activate V2, activate V1, activate V2), U34#(tt(), V1, V2) -> activate# V1, U34#(tt(), V1, V2) -> activate# V2, 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, U41#(tt(), V2) -> isNatKind# activate V2, U41#(tt(), V2) -> activate# V2, U61#(tt(), V2) -> isNatKind# activate V2, U61#(tt(), V2) -> activate# V2, U72#(tt(), N) -> activate# N, U71#(tt(), N) -> isNatKind# activate N, U71#(tt(), N) -> activate# N, U71#(tt(), N) -> U72#(isNatKind activate N, 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), U81#(tt(), M, N) -> isNatKind# activate M, U81#(tt(), M, N) -> activate# M, U81#(tt(), M, N) -> activate# N, U81#(tt(), M, N) -> U82#(isNatKind activate M, activate M, activate N), U83#(tt(), M, N) -> isNatKind# activate N, U83#(tt(), M, N) -> activate# M, U83#(tt(), M, N) -> 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), U91#(tt(), N) -> isNatKind# activate N, U91#(tt(), N) -> activate# N} SCC (113): Strict: { U102#(tt(), M, N) -> activate# M, U102#(tt(), M, N) -> activate# N, U102#(tt(), M, N) -> U103#(isNat activate N, activate M, activate N), U102#(tt(), M, N) -> isNat# activate N, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1, isNatKind# n__plus(V1, V2) -> activate# V2, isNatKind# n__plus(V1, V2) -> U41#(isNatKind activate V1, activate V2), isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__x(V1, V2) -> isNatKind# activate V1, isNatKind# n__x(V1, V2) -> activate# V1, isNatKind# n__x(V1, V2) -> activate# V2, isNatKind# n__x(V1, V2) -> U61#(isNatKind activate V1, activate V2), activate# n__plus(X1, X2) -> plus#(X1, X2), activate# n__x(X1, X2) -> x#(X1, X2), U101#(tt(), M, N) -> U102#(isNatKind activate M, activate M, activate N), U101#(tt(), M, N) -> isNatKind# activate M, U101#(tt(), M, N) -> activate# M, U101#(tt(), M, N) -> activate# N, U103#(tt(), M, N) -> isNatKind# activate N, U103#(tt(), M, N) -> activate# M, U103#(tt(), M, N) -> activate# N, U103#(tt(), M, N) -> U104#(isNatKind activate N, activate M, activate N), isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNat# n__plus(V1, V2) -> activate# V1, isNat# n__plus(V1, V2) -> activate# V2, isNat# n__plus(V1, V2) -> U11#(isNatKind activate V1, activate V1, activate V2), isNat# n__s V1 -> isNatKind# activate V1, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), isNat# n__x(V1, V2) -> isNatKind# activate V1, isNat# n__x(V1, V2) -> activate# V1, isNat# n__x(V1, V2) -> activate# V2, isNat# n__x(V1, V2) -> U31#(isNatKind activate V1, activate V1, activate V2), U104#(tt(), M, N) -> activate# M, U104#(tt(), M, N) -> activate# N, U104#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), U104#(tt(), M, N) -> x#(activate N, activate M), plus#(N, s M) -> isNat# M, plus#(N, s M) -> U81#(isNat M, M, N), plus#(N, 0()) -> isNat# N, plus#(N, 0()) -> U71#(isNat N, N), x#(N, s M) -> U101#(isNat M, M, N), x#(N, s M) -> isNat# M, x#(N, 0()) -> isNat# N, x#(N, 0()) -> U91#(isNat N, N), U12#(tt(), V1, V2) -> isNatKind# activate V2, U12#(tt(), V1, V2) -> activate# V1, U12#(tt(), V1, V2) -> activate# V2, U12#(tt(), V1, V2) -> U13#(isNatKind activate V2, activate V1, activate V2), U11#(tt(), V1, V2) -> isNatKind# activate V1, U11#(tt(), V1, V2) -> activate# V1, U11#(tt(), V1, V2) -> activate# V2, U11#(tt(), V1, V2) -> U12#(isNatKind activate V1, activate V1, activate V2), U13#(tt(), V1, V2) -> isNatKind# activate V2, U13#(tt(), V1, V2) -> activate# V1, U13#(tt(), V1, V2) -> activate# V2, U13#(tt(), V1, V2) -> U14#(isNatKind activate V2, activate V1, activate V2), U14#(tt(), V1, V2) -> activate# V1, U14#(tt(), V1, V2) -> activate# V2, 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, U22#(tt(), V1) -> activate# V1, U22#(tt(), V1) -> isNat# activate V1, U21#(tt(), V1) -> isNatKind# activate V1, U21#(tt(), V1) -> activate# V1, U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U32#(tt(), V1, V2) -> isNatKind# activate V2, U32#(tt(), V1, V2) -> activate# V1, U32#(tt(), V1, V2) -> activate# V2, U32#(tt(), V1, V2) -> U33#(isNatKind activate V2, activate V1, activate V2), U31#(tt(), V1, V2) -> isNatKind# activate V1, U31#(tt(), V1, V2) -> activate# V1, U31#(tt(), V1, V2) -> activate# V2, U31#(tt(), V1, V2) -> U32#(isNatKind activate V1, activate V1, activate V2), U33#(tt(), V1, V2) -> isNatKind# activate V2, U33#(tt(), V1, V2) -> activate# V1, U33#(tt(), V1, V2) -> activate# V2, U33#(tt(), V1, V2) -> U34#(isNatKind activate V2, activate V1, activate V2), U34#(tt(), V1, V2) -> activate# V1, U34#(tt(), V1, V2) -> activate# V2, 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, U41#(tt(), V2) -> isNatKind# activate V2, U41#(tt(), V2) -> activate# V2, U61#(tt(), V2) -> isNatKind# activate V2, U61#(tt(), V2) -> activate# V2, U72#(tt(), N) -> activate# N, U71#(tt(), N) -> isNatKind# activate N, U71#(tt(), N) -> activate# N, U71#(tt(), N) -> U72#(isNatKind activate N, 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), U81#(tt(), M, N) -> isNatKind# activate M, U81#(tt(), M, N) -> activate# M, U81#(tt(), M, N) -> activate# N, U81#(tt(), M, N) -> U82#(isNatKind activate M, activate M, activate N), U83#(tt(), M, N) -> isNatKind# activate N, U83#(tt(), M, N) -> activate# M, U83#(tt(), M, N) -> 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), U91#(tt(), N) -> isNatKind# activate N, U91#(tt(), N) -> activate# N} Weak: { U102(tt(), M, N) -> U103(isNat activate N, activate M, activate N), 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), activate X -> X, 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), U101(tt(), M, N) -> U102(isNatKind activate M, activate M, activate N), U103(tt(), M, N) -> U104(isNatKind activate N, activate M, activate N), 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), U104(tt(), M, N) -> plus(x(activate N, activate M), activate N), plus(N, s M) -> U81(isNat M, M, N), plus(N, 0()) -> U71(isNat N, N), plus(X1, X2) -> n__plus(X1, X2), x(N, s M) -> U101(isNat M, M, N), x(N, 0()) -> U91(isNat N, N), x(X1, X2) -> n__x(X1, X2), U12(tt(), V1, V2) -> U13(isNatKind activate V2, activate V1, activate V2), U11(tt(), V1, V2) -> U12(isNatKind activate V1, 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(), U22(tt(), V1) -> U23 isNat activate V1, U21(tt(), V1) -> U22(isNatKind activate V1, activate V1), U23 tt() -> tt(), U32(tt(), V1, V2) -> U33(isNatKind activate V2, activate V1, activate V2), U31(tt(), V1, V2) -> U32(isNatKind activate V1, 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(), U42 tt() -> tt(), U41(tt(), V2) -> U42 isNatKind activate V2, U51 tt() -> tt(), U62 tt() -> tt(), U61(tt(), V2) -> U62 isNatKind activate V2, U72(tt(), N) -> activate N, U71(tt(), N) -> U72(isNatKind activate N, 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), U83(tt(), M, N) -> U84(isNatKind activate N, activate M, activate N), U84(tt(), M, N) -> s plus(activate N, activate M), s X -> n__s X, U92 tt() -> 0(), U91(tt(), N) -> U92 isNatKind activate N, 0() -> n__0()} Fail