MAYBE Problem: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Proof: DP Processor: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) first#(0(),Z) -> nil#() first#(s(X),cons(Y,Z)) -> activate#(Z) first#(s(X),cons(Y,Z)) -> cons#(Y,n__first(X,activate(Z))) from#(X) -> cons#(X,n__from(n__s(X))) sel1#(s(X),cons(Y,Z)) -> activate#(Z) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) sel1#(0(),cons(X,Z)) -> quote#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) first1#(s(X),cons(Y,Z)) -> quote#(Y) quote1#(n__cons(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) quote1#(n__cons(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote#(activate(X)) quote#(n__s(X)) -> activate#(X) quote#(n__s(X)) -> quote#(activate(X)) quote#(n__sel(X,Z)) -> activate#(Z) quote#(n__sel(X,Z)) -> activate#(X) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) quote1#(n__first(X,Z)) -> activate#(Z) quote1#(n__first(X,Z)) -> activate#(X) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) unquote#(01()) -> 0#() unquote#(s1(X)) -> unquote#(X) unquote#(s1(X)) -> s#(unquote(X)) unquote1#(nil1()) -> nil#() unquote1#(cons1(X,Z)) -> unquote1#(Z) unquote1#(cons1(X,Z)) -> unquote#(X) unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z)) fcons#(X,Z) -> cons#(X,Z) activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Usable Rule Processor: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) first#(0(),Z) -> nil#() first#(s(X),cons(Y,Z)) -> activate#(Z) first#(s(X),cons(Y,Z)) -> cons#(Y,n__first(X,activate(Z))) from#(X) -> cons#(X,n__from(n__s(X))) sel1#(s(X),cons(Y,Z)) -> activate#(Z) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) sel1#(0(),cons(X,Z)) -> quote#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) first1#(s(X),cons(Y,Z)) -> quote#(Y) quote1#(n__cons(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) quote1#(n__cons(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote#(activate(X)) quote#(n__s(X)) -> activate#(X) quote#(n__s(X)) -> quote#(activate(X)) quote#(n__sel(X,Z)) -> activate#(Z) quote#(n__sel(X,Z)) -> activate#(X) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) quote1#(n__first(X,Z)) -> activate#(Z) quote1#(n__first(X,Z)) -> activate#(X) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) unquote#(01()) -> 0#() unquote#(s1(X)) -> unquote#(X) unquote#(s1(X)) -> s#(unquote(X)) unquote1#(nil1()) -> nil#() unquote1#(cons1(X,Z)) -> unquote1#(Z) unquote1#(cons1(X,Z)) -> unquote#(X) unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z)) fcons#(X,Z) -> cons#(X,Z) activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) TRS: f41(x,y) -> x f41(x,y) -> y activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) EDG Processor: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) first#(0(),Z) -> nil#() first#(s(X),cons(Y,Z)) -> activate#(Z) first#(s(X),cons(Y,Z)) -> cons#(Y,n__first(X,activate(Z))) from#(X) -> cons#(X,n__from(n__s(X))) sel1#(s(X),cons(Y,Z)) -> activate#(Z) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) sel1#(0(),cons(X,Z)) -> quote#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) first1#(s(X),cons(Y,Z)) -> quote#(Y) quote1#(n__cons(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) quote1#(n__cons(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote#(activate(X)) quote#(n__s(X)) -> activate#(X) quote#(n__s(X)) -> quote#(activate(X)) quote#(n__sel(X,Z)) -> activate#(Z) quote#(n__sel(X,Z)) -> activate#(X) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) quote1#(n__first(X,Z)) -> activate#(Z) quote1#(n__first(X,Z)) -> activate#(X) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) unquote#(01()) -> 0#() unquote#(s1(X)) -> unquote#(X) unquote#(s1(X)) -> s#(unquote(X)) unquote1#(nil1()) -> nil#() unquote1#(cons1(X,Z)) -> unquote1#(Z) unquote1#(cons1(X,Z)) -> unquote#(X) unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z)) fcons#(X,Z) -> cons#(X,Z) activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) TRS: f41(x,y) -> x f41(x,y) -> y activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) graph: unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z)) -> fcons#(X,Z) -> cons#(X,Z) unquote1#(cons1(X,Z)) -> unquote1#(Z) -> unquote1#(nil1()) -> nil#() unquote1#(cons1(X,Z)) -> unquote1#(Z) -> unquote1#(cons1(X,Z)) -> unquote1#(Z) unquote1#(cons1(X,Z)) -> unquote1#(Z) -> unquote1#(cons1(X,Z)) -> unquote#(X) unquote1#(cons1(X,Z)) -> unquote1#(Z) -> unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z)) unquote1#(cons1(X,Z)) -> unquote#(X) -> unquote#(01()) -> 0#() unquote1#(cons1(X,Z)) -> unquote#(X) -> unquote#(s1(X)) -> unquote#(X) unquote1#(cons1(X,Z)) -> unquote#(X) -> unquote#(s1(X)) -> s#(unquote(X)) unquote#(s1(X)) -> unquote#(X) -> unquote#(01()) -> 0#() unquote#(s1(X)) -> unquote#(X) -> unquote#(s1(X)) -> unquote#(X) unquote#(s1(X)) -> unquote#(X) -> unquote#(s1(X)) -> s#(unquote(X)) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__cons(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__cons(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__cons(X,Z)) -> quote#(activate(X)) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__first(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__first(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) -> quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) quote1#(n__cons(X,Z)) -> quote#(activate(X)) -> quote#(n__s(X)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote#(activate(X)) -> quote#(n__s(X)) -> quote#(activate(X)) quote1#(n__cons(X,Z)) -> quote#(activate(X)) -> quote#(n__sel(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote#(activate(X)) -> quote#(n__sel(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote#(activate(X)) -> quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X2) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X1) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__0()) -> 0#() quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) -> first1#(s(X),cons(Y,Z)) -> activate#(Z) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) -> first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) -> first1#(s(X),cons(Y,Z)) -> quote#(Y) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X2) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X1) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__0()) -> 0#() quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) -> first1#(s(X),cons(Y,Z)) -> activate#(Z) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) -> first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) -> first1#(s(X),cons(Y,Z)) -> quote#(Y) first1#(s(X),cons(Y,Z)) -> quote#(Y) -> quote#(n__s(X)) -> activate#(X) first1#(s(X),cons(Y,Z)) -> quote#(Y) -> quote#(n__s(X)) -> quote#(activate(X)) first1#(s(X),cons(Y,Z)) -> quote#(Y) -> quote#(n__sel(X,Z)) -> activate#(Z) first1#(s(X),cons(Y,Z)) -> quote#(Y) -> quote#(n__sel(X,Z)) -> activate#(X) first1#(s(X),cons(Y,Z)) -> quote#(Y) -> quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) -> sel1#(s(X),cons(Y,Z)) -> activate#(Z) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) -> sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) -> sel1#(0(),cons(X,Z)) -> quote#(X) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X2) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X1) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__0()) -> 0#() quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) quote#(n__s(X)) -> quote#(activate(X)) -> quote#(n__s(X)) -> activate#(X) quote#(n__s(X)) -> quote#(activate(X)) -> quote#(n__s(X)) -> quote#(activate(X)) quote#(n__s(X)) -> quote#(activate(X)) -> quote#(n__sel(X,Z)) -> activate#(Z) quote#(n__s(X)) -> quote#(activate(X)) -> quote#(n__sel(X,Z)) -> activate#(X) quote#(n__s(X)) -> quote#(activate(X)) -> quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) quote#(n__s(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X2) quote#(n__s(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X1) quote#(n__s(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) quote#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) quote#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) quote#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) quote#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) quote#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() quote#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) quote#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) quote#(n__s(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) quote#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) quote#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel1#(0(),cons(X,Z)) -> quote#(X) -> quote#(n__s(X)) -> activate#(X) sel1#(0(),cons(X,Z)) -> quote#(X) -> quote#(n__s(X)) -> quote#(activate(X)) sel1#(0(),cons(X,Z)) -> quote#(X) -> quote#(n__sel(X,Z)) -> activate#(Z) sel1#(0(),cons(X,Z)) -> quote#(X) -> quote#(n__sel(X,Z)) -> activate#(X) sel1#(0(),cons(X,Z)) -> quote#(X) -> quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) -> sel1#(s(X),cons(Y,Z)) -> activate#(Z) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) -> sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) -> sel1#(0(),cons(X,Z)) -> quote#(X) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__0()) -> 0#() activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__nil()) -> nil#() activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__nil()) -> nil#() activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) -> sel#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) -> sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__nil()) -> nil#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__from(X)) -> from#(activate(X)) -> from#(X) -> cons#(X,n__from(n__s(X))) activate#(n__from(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() activate#(n__from(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() activate#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) -> first#(0(),Z) -> nil#() activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) -> first#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) -> first#(s(X),cons(Y,Z)) -> cons#(Y,n__first(X,activate(Z))) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> activate#(X) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__0()) -> 0#() activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__nil()) -> nil#() activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X2) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__nil()) -> nil#() activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> activate#(X1) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) -> sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) -> sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) Restore Modifier: DPs: sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) first#(0(),Z) -> nil#() first#(s(X),cons(Y,Z)) -> activate#(Z) first#(s(X),cons(Y,Z)) -> cons#(Y,n__first(X,activate(Z))) from#(X) -> cons#(X,n__from(n__s(X))) sel1#(s(X),cons(Y,Z)) -> activate#(Z) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) sel1#(0(),cons(X,Z)) -> quote#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) first1#(s(X),cons(Y,Z)) -> quote#(Y) quote1#(n__cons(X,Z)) -> activate#(Z) quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) quote1#(n__cons(X,Z)) -> activate#(X) quote1#(n__cons(X,Z)) -> quote#(activate(X)) quote#(n__s(X)) -> activate#(X) quote#(n__s(X)) -> quote#(activate(X)) quote#(n__sel(X,Z)) -> activate#(Z) quote#(n__sel(X,Z)) -> activate#(X) quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) quote1#(n__first(X,Z)) -> activate#(Z) quote1#(n__first(X,Z)) -> activate#(X) quote1#(n__first(X,Z)) -> first1#(activate(X),activate(Z)) unquote#(01()) -> 0#() unquote#(s1(X)) -> unquote#(X) unquote#(s1(X)) -> s#(unquote(X)) unquote1#(nil1()) -> nil#() unquote1#(cons1(X,Z)) -> unquote1#(Z) unquote1#(cons1(X,Z)) -> unquote#(X) unquote1#(cons1(X,Z)) -> fcons#(unquote(X),unquote1(Z)) fcons#(X,Z) -> cons#(X,Z) activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X SCC Processor: #sccs: 6 #rules: 20 #arcs: 310/2116 DPs: quote1#(n__cons(X,Z)) -> quote1#(activate(Z)) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Open DPs: first1#(s(X),cons(Y,Z)) -> first1#(X,activate(Z)) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Open DPs: quote#(n__sel(X,Z)) -> sel1#(activate(X),activate(Z)) sel1#(0(),cons(X,Z)) -> quote#(X) quote#(n__s(X)) -> quote#(activate(X)) sel1#(s(X),cons(Y,Z)) -> sel1#(X,activate(Z)) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Open DPs: activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) sel#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) first#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> activate#(X2) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Open DPs: unquote1#(cons1(X,Z)) -> unquote1#(Z) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Open DPs: unquote#(s1(X)) -> unquote#(X) TRS: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel(0(),cons(X,Z)) -> X first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(n__s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) quote(n__0()) -> 01() quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__nil()) -> nil1() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(nil1()) -> nil() unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(X) -> X Open