NO
0.08/0.17	NO
0.08/0.17	
0.08/0.17	Problem:
0.08/0.17	 hd(cons()) -> X
0.08/0.17	 tl(cons()) -> Y
0.08/0.17	 nats() -> adx(zeros())
0.08/0.17	 zeros() -> cons()
0.08/0.17	 incr(cons()) -> cons()
0.08/0.17	 adx(cons()) -> incr(cons())
0.08/0.17	
0.08/0.17	Proof:
0.08/0.17	 Fresh Variable Processor: loop length: 1
0.08/0.17	                           terms:
0.08/0.17	                            hd(cons())
0.08/0.17	                           context: []
0.08/0.17	                           substitution:
0.08/0.17	                            X -> hd(cons())
0.08/0.17	  Qed
0.08/0.18	EOF