(VAR M N V1 V2 )
(STRATEGY CONTEXTSENSITIVE
        (U101 1) 
        (tt ) 
        (U102 1) 
        (isNatKind ) 
        (U103 1) 
        (isNat ) 
        (U104 1) 
        (plus 1 2) 
        (x 1 2) 
        (U11 1) 
        (U12 1) 
        (U13 1) 
        (U14 1) 
        (U15 1) 
        (U16 1) 
        (U21 1) 
        (U22 1) 
        (U23 1) 
        (U31 1) 
        (U32 1) 
        (U33 1) 
        (U34 1) 
        (U35 1) 
        (U36 1) 
        (U41 1) 
        (U42 1) 
        (U51 1) 
        (U61 1) 
        (U62 1) 
        (U71 1) 
        (U72 1) 
        (U81 1) 
        (U82 1) 
        (U83 1) 
        (U84 1) 
        (s 1) 
        (U91 1) 
        (U92 1) 
        (0 ) 
)
(RULES 
        U101(tt, M, N) -> U102(isNatKind(M), M, N)
        U102(tt, M, N) -> U103(isNat(N), M, N)
        U103(tt, M, N) -> U104(isNatKind(N), M, N)
        U104(tt, M, N) -> plus(x(N, M), N)
        U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
        U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
        U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
        U14(tt, V1, V2) -> U15(isNat(V1), V2)
        U15(tt, V2) -> U16(isNat(V2))
        U16(tt) -> tt
        U21(tt, V1) -> U22(isNatKind(V1), V1)
        U22(tt, V1) -> U23(isNat(V1))
        U23(tt) -> tt
        U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
        U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
        U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
        U34(tt, V1, V2) -> U35(isNat(V1), V2)
        U35(tt, V2) -> U36(isNat(V2))
        U36(tt) -> tt
        U41(tt, V2) -> U42(isNatKind(V2))
        U42(tt) -> tt
        U51(tt) -> tt
        U61(tt, V2) -> U62(isNatKind(V2))
        U62(tt) -> tt
        U71(tt, N) -> U72(isNatKind(N), N)
        U72(tt, N) -> N
        U81(tt, M, N) -> U82(isNatKind(M), M, N)
        U82(tt, M, N) -> U83(isNat(N), M, N)
        U83(tt, M, N) -> U84(isNatKind(N), M, N)
        U84(tt, M, N) -> s(plus(N, M))
        U91(tt, N) -> U92(isNatKind(N))
        U92(tt) -> 0
        isNat(0) -> tt
        isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
        isNat(s(V1)) -> U21(isNatKind(V1), V1)
        isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
        isNatKind(0) -> tt
        isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
        isNatKind(s(V1)) -> U51(isNatKind(V1))
        isNatKind(x(V1, V2)) -> U61(isNatKind(V1), 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)
        
)