NO
0.07/0.18	NO
0.07/0.18	
0.07/0.18	Problem:
0.07/0.18	 sel(0(),cons()) -> X
0.07/0.18	 sel(s(),cons()) -> sel(X,Z)
0.07/0.18	 dbl1(s()) -> s1(s1(dbl1(X)))
0.07/0.18	 sel1(0(),cons()) -> X
0.07/0.18	 sel1(s(),cons()) -> sel1(X,Z)
0.07/0.18	 quote(s()) -> s1(quote(X))
0.07/0.18	 dbl(0()) -> 0()
0.07/0.18	 dbl(s()) -> s()
0.07/0.18	 dbls(nil()) -> nil()
0.07/0.18	 dbls(cons()) -> cons()
0.07/0.18	 indx(nil()) -> nil()
0.07/0.18	 indx(cons()) -> cons()
0.07/0.18	 from() -> cons()
0.07/0.18	 dbl1(0()) -> 01()
0.07/0.18	 quote(0()) -> 01()
0.07/0.18	 quote(dbl(X)) -> dbl1(X)
0.07/0.18	 quote(sel(X,Y)) -> sel1(X,Y)
0.07/0.18	
0.07/0.18	Proof:
0.07/0.18	 Fresh Variable Processor:
0.07/0.18	  loop length: 1
0.07/0.18	  terms:
0.07/0.18	   sel(0(),cons())
0.07/0.18	  context: []
0.07/0.18	  substitution:
0.07/0.18	   X -> sel(0(),cons())
0.07/0.18	  Qed
0.07/0.18	EOF