NO 0.08/0.18 NO 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 sel(s(X),cons(Y)) -> sel(X,Z) 0.08/0.18 sel1(s(X),cons(Y)) -> sel1(X,Z) 0.08/0.18 first1(s(X),cons(Y)) -> cons1(quote(),first1(X,Z)) 0.08/0.18 quote() -> sel1(X,Z) 0.08/0.18 quote1() -> first1(X,Z) 0.08/0.18 sel(0(),cons(X)) -> X 0.08/0.18 first(0(),Z) -> nil() 0.08/0.18 first(s(X),cons(Y)) -> cons(Y) 0.08/0.18 from(X) -> cons(X) 0.08/0.18 sel1(0(),cons(X)) -> quote() 0.08/0.18 first1(0(),Z) -> nil1() 0.08/0.18 quote() -> 01() 0.08/0.18 quote1() -> cons1(quote(),quote1()) 0.08/0.18 quote1() -> nil1() 0.08/0.18 quote() -> s1(quote()) 0.08/0.18 unquote(01()) -> 0() 0.08/0.18 unquote(s1(X)) -> s(unquote(X)) 0.08/0.18 unquote1(nil1()) -> nil() 0.08/0.18 unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) 0.08/0.18 fcons(X,Z) -> cons(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 sel(s(X),cons(Y)) 0.08/0.18 context: sel(X,[]) 0.08/0.18 substitution: 0.08/0.18 Z -> sel(s(X),cons(Y)) 0.08/0.18 Qed 0.08/0.19 EOF