NO 0.08/0.17 NO 0.08/0.17 0.08/0.17 Problem: 0.08/0.17 tail(cons(X)) -> XS 0.08/0.17 nats() -> cons(0()) 0.08/0.17 pairs() -> cons(0()) 0.08/0.17 odds() -> incr(pairs()) 0.08/0.17 incr(cons(X)) -> cons(s(X)) 0.08/0.17 head(cons(X)) -> X 0.08/0.17 0.08/0.17 Proof: 0.08/0.17 Fresh Variable Processor: 0.08/0.17 loop length: 1 0.08/0.17 terms: 0.08/0.17 tail(cons(X)) 0.08/0.17 context: [] 0.08/0.17 substitution: 0.08/0.17 XS -> tail(cons(X)) 0.08/0.17 Qed 0.08/0.18 EOF