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