MAYBE Problem: dbl(0()) -> 0() dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) dbls(nil()) -> nil() dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) -> activate(X) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) indx(nil(),X) -> nil() indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) -> cons(activate(X),n__from(n__s(activate(X)))) s(X) -> n__s(X) dbl(X) -> n__dbl(X) dbls(X) -> n__dbls(X) sel(X1,X2) -> n__sel(X1,X2) indx(X1,X2) -> n__indx(X1,X2) from(X) -> n__from(X) activate(n__s(X)) -> s(X) activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__from(X)) -> from(X) activate(X) -> X Proof: DP Processor: DPs: dbl#(s(X)) -> activate#(X) dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))) dbls#(cons(X,Y)) -> activate#(Y) dbls#(cons(X,Y)) -> activate#(X) sel#(0(),cons(X,Y)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) indx#(cons(X,Y),Z) -> activate#(Y) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(X) from#(X) -> activate#(X) activate#(n__s(X)) -> s#(X) activate#(n__dbl(X)) -> activate#(X) activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__dbls(X)) -> activate#(X) activate#(n__dbls(X)) -> dbls#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__from(X)) -> from#(X) TRS: dbl(0()) -> 0() dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) dbls(nil()) -> nil() dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) -> activate(X) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) indx(nil(),X) -> nil() indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) -> cons(activate(X),n__from(n__s(activate(X)))) s(X) -> n__s(X) dbl(X) -> n__dbl(X) dbls(X) -> n__dbls(X) sel(X1,X2) -> n__sel(X1,X2) indx(X1,X2) -> n__indx(X1,X2) from(X) -> n__from(X) activate(n__s(X)) -> s(X) activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__from(X)) -> from(X) activate(X) -> X EDG Processor: DPs: dbl#(s(X)) -> activate#(X) dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))) dbls#(cons(X,Y)) -> activate#(Y) dbls#(cons(X,Y)) -> activate#(X) sel#(0(),cons(X,Y)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) indx#(cons(X,Y),Z) -> activate#(Y) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(X) from#(X) -> activate#(X) activate#(n__s(X)) -> s#(X) activate#(n__dbl(X)) -> activate#(X) activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__dbls(X)) -> activate#(X) activate#(n__dbls(X)) -> dbls#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__from(X)) -> from#(X) TRS: dbl(0()) -> 0() dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) dbls(nil()) -> nil() dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) -> activate(X) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) indx(nil(),X) -> nil() indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) -> cons(activate(X),n__from(n__s(activate(X)))) s(X) -> n__s(X) dbl(X) -> n__dbl(X) dbls(X) -> n__dbls(X) sel(X1,X2) -> n__sel(X1,X2) indx(X1,X2) -> n__indx(X1,X2) from(X) -> n__from(X) activate(n__s(X)) -> s(X) activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__from(X)) -> from(X) activate(X) -> X graph: from#(X) -> activate#(X) -> activate#(n__s(X)) -> s#(X) from#(X) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) from#(X) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) from#(X) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) from#(X) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) from#(X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) from#(X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) from#(X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) from#(X) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) from#(X) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) from#(X) -> activate#(X) -> activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__dbl(X)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__dbl(X)) -> dbl#(activate(X)) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__dbls(X)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__dbls(X)) -> dbls#(activate(X)) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X2) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> activate#(X1) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__indx(X1,X2)) -> activate#(X1) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__dbl(X)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__dbl(X)) -> dbl#(activate(X)) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__dbls(X)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__dbls(X)) -> dbls#(activate(X)) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> activate#(X2) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> activate#(X1) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__indx(X1,X2)) -> activate#(X1) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__s(X)) -> s#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__from(X)) -> from#(X) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) -> sel#(0(),cons(X,Y)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) -> sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) -> sel#(s(X),cons(Y,Z)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) -> sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__dbl(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__dbl(X)) -> dbl#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__dbls(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__dbls(X)) -> dbls#(activate(X)) 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)) -> activate#(Z) -> activate#(n__indx(X1,X2)) -> activate#(X1) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__dbl(X)) -> activate#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__dbl(X)) -> dbl#(activate(X)) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__dbls(X)) -> activate#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__dbls(X)) -> dbls#(activate(X)) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> activate#(X2) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> activate#(X1) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__indx(X1,X2)) -> activate#(X1) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> from#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) activate#(n__from(X)) -> from#(X) -> from#(X) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) -> indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) -> indx#(cons(X,Y),Z) -> activate#(Z) activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) -> indx#(cons(X,Y),Z) -> activate#(X) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(X) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__dbl(X)) -> activate#(X) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__dbls(X)) -> activate#(X) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__dbls(X)) -> dbls#(activate(X)) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__indx(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(X) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) -> sel#(0(),cons(X,Y)) -> activate#(X) 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)) -> activate#(X) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) -> sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(X) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__dbl(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__dbls(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__dbls(X)) -> dbls#(activate(X)) 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#(X2) -> activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__sel(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> from#(X) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(X) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__dbl(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__dbls(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__dbls(X)) -> dbls#(activate(X)) 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)) -> activate#(X1) -> activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__sel(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(X) activate#(n__dbls(X)) -> dbls#(activate(X)) -> dbls#(cons(X,Y)) -> activate#(Y) activate#(n__dbls(X)) -> dbls#(activate(X)) -> dbls#(cons(X,Y)) -> activate#(X) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__dbls(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) activate#(n__dbl(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) activate#(n__dbl(X)) -> dbl#(activate(X)) -> dbl#(s(X)) -> activate#(X) activate#(n__dbl(X)) -> dbl#(activate(X)) -> dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))) dbl#(s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__dbl(X)) -> activate#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(activate(X)) dbl#(s(X)) -> activate#(X) -> activate#(n__dbls(X)) -> activate#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(activate(X)) dbl#(s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X2) dbl#(s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> activate#(X1) dbl#(s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) dbl#(s(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> activate#(X1) dbl#(s(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) dbl#(s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) SCC Processor: #sccs: 1 #rules: 21 #arcs: 181/529 DPs: from#(X) -> activate#(X) activate#(n__from(X)) -> from#(X) activate#(n__indx(X1,X2)) -> indx#(activate(X1),X2) indx#(cons(X,Y),Z) -> activate#(X) activate#(n__indx(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2)) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) sel#(s(X),cons(Y,Z)) -> activate#(X) activate#(n__sel(X1,X2)) -> activate#(X1) activate#(n__sel(X1,X2)) -> activate#(X2) activate#(n__dbls(X)) -> dbls#(activate(X)) dbls#(cons(X,Y)) -> activate#(X) activate#(n__dbls(X)) -> activate#(X) activate#(n__dbl(X)) -> dbl#(activate(X)) dbl#(s(X)) -> activate#(X) activate#(n__dbl(X)) -> activate#(X) dbls#(cons(X,Y)) -> activate#(Y) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(0(),cons(X,Y)) -> activate#(X) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(Y) TRS: dbl(0()) -> 0() dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) dbls(nil()) -> nil() dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) -> activate(X) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) indx(nil(),X) -> nil() indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) -> cons(activate(X),n__from(n__s(activate(X)))) s(X) -> n__s(X) dbl(X) -> n__dbl(X) dbls(X) -> n__dbls(X) sel(X1,X2) -> n__sel(X1,X2) indx(X1,X2) -> n__indx(X1,X2) from(X) -> n__from(X) activate(n__s(X)) -> s(X) activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__from(X)) -> from(X) activate(X) -> X Open