NO
0.08/0.18	NO
0.08/0.18	
0.08/0.18	Problem:
0.08/0.18	 tail(cons(X)) -> L
0.08/0.18	 incr(nil()) -> nil()
0.08/0.18	 incr(cons(X)) -> cons(s(X))
0.08/0.18	 adx(nil()) -> nil()
0.08/0.18	 adx(cons(X)) -> incr(cons(X))
0.08/0.18	 nats() -> adx(zeros())
0.08/0.18	 zeros() -> cons(0())
0.08/0.18	 head(cons(X)) -> 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	   L -> tail(cons(X))
0.08/0.18	  Qed
0.08/0.18	EOF