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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,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) -> s#(X) from#(X) -> cons#(X,n__from(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)) -> first#(X1,X2) activate#(n__from(X)) -> from#(X) activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> cons#(X1,X2) activate#(n__nil()) -> nil#() activate#(n__s(X)) -> s#(X) activate#(n__sel(X1,X2)) -> sel#(X1,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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(X) -> X CDG 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) -> s#(X) from#(X) -> cons#(X,n__from(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)) -> first#(X1,X2) activate#(n__from(X)) -> from#(X) activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> cons#(X1,X2) activate#(n__nil()) -> nil#() activate#(n__s(X)) -> s#(X) activate#(n__sel(X1,X2)) -> sel#(X1,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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(X) -> X 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)) -> first#(X1,X2) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) quote1#(n__cons(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(X1,X2) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__0()) -> 0#() quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) quote1#(n__cons(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,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)) -> first#(X1,X2) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) quote1#(n__first(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(X1,X2) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__0()) -> 0#() quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) quote1#(n__first(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,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)) -> first#(X1,X2) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(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)) -> cons#(X1,X2) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) first1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,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)) -> first#(X1,X2) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__0()) -> 0#() quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) quote#(n__sel(X,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__first(X1,X2)) -> first#(X1,X2) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__0()) -> 0#() quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) quote#(n__sel(X,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,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)) -> first#(X1,X2) quote#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) quote#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() quote#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2) quote#(n__s(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() quote#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) quote#(n__s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,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)) -> first#(X1,X2) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(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)) -> cons#(X1,X2) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) sel1#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(X1,X2) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(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)) -> cons#(X1,X2) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) first#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__from(X)) -> from#(X) -> from#(X) -> s#(X) activate#(n__from(X)) -> from#(X) -> from#(X) -> cons#(X,n__from(s(X))) activate#(n__first(X1,X2)) -> first#(X1,X2) -> first#(0(),Z) -> nil#() activate#(n__first(X1,X2)) -> first#(X1,X2) -> first#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__first(X1,X2)) -> first#(X1,X2) -> first#(s(X),cons(Y,Z)) -> cons#(Y,n__first(X,activate(Z))) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__first(X1,X2)) -> first#(X1,X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(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)) -> cons#(X1,X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__nil()) -> nil#() sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,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)) SCC Processor: #sccs: 6 #rules: 13 #arcs: 136/1600 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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(X) -> X Open DPs: activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) sel#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__first(X1,X2)) -> first#(X1,X2) first#(s(X),cons(Y,Z)) -> 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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,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(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) 0() -> n__0() cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(X) -> X Open