(VAR M N X )
(RULES 
        U11(tt) -> N
        U21(tt) -> s(plus(N, M))
        U41(tt) -> plus(x(N, M), N)
        and(tt) -> X
        U31(tt) -> 0
        isNat -> tt
        isNat -> and(isNat)
        isNat -> isNat
        plus(N, 0) -> U11(isNat)
        plus(N, s(M)) -> U21(and(isNat))
        x(N, 0) -> U31(isNat)
        x(N, s(M)) -> U41(and(isNat))
        
)