(VAR M N V1 V2 X )
(STRATEGY CONTEXTSENSITIVE
        (U11 1) 
        (tt ) 
        (U12 1) 
        (isNat ) 
        (U13 1) 
        (U21 1) 
        (U22 1) 
        (U31 1) 
        (U32 1) 
        (U33 1) 
        (U41 1) 
        (U51 1) 
        (s 1) 
        (plus 1 2) 
        (U61 1) 
        (0 ) 
        (U71 1) 
        (x 1 2) 
        (and 1) 
        (isNatKind ) 
)
(RULES 
        U11(tt, V1, V2) -> U12(isNat(V1), V2)
        U12(tt, V2) -> U13(isNat(V2))
        U13(tt) -> tt
        U21(tt, V1) -> U22(isNat(V1))
        U22(tt) -> tt
        U31(tt, V1, V2) -> U32(isNat(V1), V2)
        U32(tt, V2) -> U33(isNat(V2))
        U33(tt) -> tt
        U41(tt, N) -> N
        U51(tt, M, N) -> s(plus(N, M))
        U61(tt) -> 0
        U71(tt, M, N) -> plus(x(N, M), N)
        and(tt, X) -> X
        isNat(0) -> tt
        isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
        isNat(s(V1)) -> U21(isNatKind(V1), V1)
        isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
        isNatKind(0) -> tt
        isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
        isNatKind(s(V1)) -> isNatKind(V1)
        isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
        plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
        plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
        x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
        x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
        
)