(VAR x xs )
(RULES 
        and(tt, tt) -> tt
        is_nat(0) -> tt
        is_nat(s(x)) -> is_nat(x)
        is_natlist(nil) -> tt
        is_natlist(cons(x, xs)) -> and(is_nat(x), is_natlist(xs))
        from(x) -> fromCond(is_natlist(x), x)
        fromCond(tt, cons(x, xs)) -> from(cons(s(x), cons(x, xs)))
        
)