NO 0.08/0.17 NO 0.08/0.17 0.08/0.17 Problem: 0.08/0.17 after(s(N),cons(X)) -> after(N,XS) 0.08/0.17 from(X) -> cons(X) 0.08/0.17 after(0(),XS) -> XS 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 after(s(N),cons(X)) 0.08/0.17 context: after(N,[]) 0.08/0.17 substitution: 0.08/0.17 XS -> after(s(N),cons(X)) 0.08/0.17 Qed 0.08/0.17 EOF