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 pairNs() -> cons(0()) 0.08/0.17 oddNs() -> incr(pairNs()) 0.08/0.17 incr(cons(X)) -> cons(s(X)) 0.08/0.17 take(0(),XS) -> nil() 0.08/0.17 take(s(N),cons(X)) -> cons(X) 0.08/0.17 zip(nil(),XS) -> nil() 0.08/0.17 zip(X,nil()) -> nil() 0.08/0.17 zip(cons(X),cons(Y)) -> cons(pair(X,Y)) 0.08/0.17 repItems(nil()) -> nil() 0.08/0.17 repItems(cons(X)) -> cons(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.17 EOF