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