NO 0.08/0.18 NO 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 tail(cons(X)) -> XS 0.08/0.18 pairNs() -> cons(0()) 0.08/0.18 oddNs() -> incr(pairNs()) 0.08/0.18 incr(cons(X)) -> cons(s(X)) 0.08/0.18 take(0(),XS) -> nil() 0.08/0.18 take(s(N),cons(X)) -> cons(X) 0.08/0.18 zip(nil(),XS) -> nil() 0.08/0.18 zip(X,nil()) -> nil() 0.08/0.18 zip(cons(X),cons(Y)) -> cons(pair(X,Y)) 0.08/0.18 repItems(nil()) -> nil() 0.08/0.18 repItems(cons(X)) -> cons(X) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Fresh Variable Processor: 0.08/0.18 loop length: 1 0.08/0.18 terms: 0.08/0.18 tail(cons(X)) 0.08/0.18 context: [] 0.08/0.18 substitution: 0.08/0.18 XS -> tail(cons(X)) 0.08/0.18 Qed 0.08/0.18 EOF