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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(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)) -> dbl#(X) activate#(n__dbls(X)) -> dbls#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) activate#(n__indx(X1,X2)) -> indx#(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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X TDG 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)) -> dbl#(X) activate#(n__dbls(X)) -> dbls#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) activate#(n__indx(X1,X2)) -> indx#(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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X graph: from#(X) -> activate#(X) -> activate#(n__from(X)) -> from#(X) from#(X) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) from#(X) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) from#(X) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(X) from#(X) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(X) from#(X) -> activate#(X) -> activate#(n__s(X)) -> s#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__dbls(X)) -> dbls#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__dbl(X)) -> dbl#(X) indx#(cons(X,Y),Z) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__dbls(X)) -> dbls#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__dbl(X)) -> dbl#(X) indx#(cons(X,Y),Z) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(X) indx#(cons(X,Y),Z) -> activate#(X) -> activate#(n__s(X)) -> s#(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)) -> 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)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) -> sel#(0(),cons(X,Y)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__dbls(X)) -> dbls#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__dbl(X)) -> dbl#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(X) sel#(s(X),cons(Y,Z)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(X) sel#(0(),cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> from#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__dbls(X)) -> dbls#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__dbl(X)) -> dbl#(X) dbls#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(X) dbls#(cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) activate#(n__from(X)) -> from#(X) -> from#(X) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) -> indx#(cons(X,Y),Z) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) -> indx#(cons(X,Y),Z) -> activate#(Z) activate#(n__indx(X1,X2)) -> indx#(X1,X2) -> indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) activate#(n__sel(X1,X2)) -> sel#(X1,X2) -> sel#(s(X),cons(Y,Z)) -> activate#(X) 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#(0(),cons(X,Y)) -> activate#(X) activate#(n__dbls(X)) -> dbls#(X) -> dbls#(cons(X,Y)) -> activate#(X) activate#(n__dbls(X)) -> dbls#(X) -> dbls#(cons(X,Y)) -> activate#(Y) activate#(n__dbl(X)) -> dbl#(X) -> dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))) activate#(n__dbl(X)) -> dbl#(X) -> dbl#(s(X)) -> activate#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__indx(X1,X2)) -> indx#(X1,X2) dbl#(s(X)) -> activate#(X) -> activate#(n__sel(X1,X2)) -> sel#(X1,X2) dbl#(s(X)) -> activate#(X) -> activate#(n__dbls(X)) -> dbls#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) SCC Processor: #sccs: 1 #rules: 16 #arcs: 76/324 DPs: from#(X) -> activate#(X) activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) activate#(n__dbls(X)) -> dbls#(X) dbls#(cons(X,Y)) -> activate#(Y) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> 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)) dbls#(cons(X,Y)) -> activate#(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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [from#](x0) = x0 + 0, [indx#](x0, x1) = x0 + x1 + 0, [sel#](x0, x1) = 4x0 + x1, [dbls#](x0) = 4x0 + 0, [activate#](x0) = x0 + 0, [dbl#](x0) = x0, [n__from](x0) = x0 + 0, [from](x0) = x0 + 0, [n__indx](x0, x1) = 7x0 + 7x1, [n__sel](x0, x1) = 4x0 + x1, [indx](x0, x1) = 7x0 + 7x1, [sel](x0, x1) = 4x0 + x1, [n__dbls](x0) = 4x0, [cons](x0, x1) = x0 + x1, [dbls](x0) = 4x0, [nil] = 0, [n__s](x0) = x0 + 0, [n__dbl](x0) = x0, [activate](x0) = x0, [s](x0) = x0 + 0, [dbl](x0) = x0, [0] = 2 orientation: from#(X) = X + 0 >= X + 0 = activate#(X) activate#(n__dbl(X)) = X + 0 >= X = dbl#(X) dbl#(s(X)) = X + 0 >= X + 0 = activate#(X) activate#(n__dbls(X)) = 4X + 0 >= 4X + 0 = dbls#(X) dbls#(cons(X,Y)) = 4X + 4Y + 0 >= Y + 0 = activate#(Y) activate#(n__sel(X1,X2)) = 4X1 + X2 + 0 >= 4X1 + X2 = sel#(X1,X2) sel#(0(),cons(X,Y)) = X + Y + 6 >= X + 0 = activate#(X) activate#(n__indx(X1,X2)) = 7X1 + 7X2 + 0 >= X1 + X2 + 0 = indx#(X1,X2) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Y + 0 = activate#(Y) activate#(n__from(X)) = X + 0 >= X + 0 = from#(X) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Z + 0 = activate#(Z) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= X + 0 = activate#(X) sel#(s(X),cons(Y,Z)) = 4X + Y + Z + 4 >= Z + 0 = activate#(Z) sel#(s(X),cons(Y,Z)) = 4X + Y + Z + 4 >= X + 0 = activate#(X) sel#(s(X),cons(Y,Z)) = 4X + Y + Z + 4 >= 4X + Z = sel#(activate(X),activate(Z)) dbls#(cons(X,Y)) = 4X + 4Y + 0 >= X + 0 = activate#(X) dbl(0()) = 2 >= 2 = 0() dbl(s(X)) = X + 0 >= X + 0 = s(n__s(n__dbl(activate(X)))) dbls(nil()) = 4 >= 0 = nil() dbls(cons(X,Y)) = 4X + 4Y >= X + 4Y = cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) = X + Y + 6 >= X = activate(X) sel(s(X),cons(Y,Z)) = 4X + Y + Z + 4 >= 4X + Z = sel(activate(X),activate(Z)) indx(nil(),X) = 7X + 7 >= 0 = nil() indx(cons(X,Y),Z) = 7X + 7Y + 7Z >= 4X + 7Y + 7Z = cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) = X + 0 >= X + 0 = cons(activate(X),n__from(n__s(activate(X)))) s(X) = X + 0 >= X + 0 = n__s(X) dbl(X) = X >= X = n__dbl(X) dbls(X) = 4X >= 4X = n__dbls(X) sel(X1,X2) = 4X1 + X2 >= 4X1 + X2 = n__sel(X1,X2) indx(X1,X2) = 7X1 + 7X2 >= 7X1 + 7X2 = n__indx(X1,X2) from(X) = X + 0 >= X + 0 = n__from(X) activate(n__s(X)) = X + 0 >= X + 0 = s(X) activate(n__dbl(X)) = X >= X = dbl(X) activate(n__dbls(X)) = 4X >= 4X = dbls(X) activate(n__sel(X1,X2)) = 4X1 + X2 >= 4X1 + X2 = sel(X1,X2) activate(n__indx(X1,X2)) = 7X1 + 7X2 >= 7X1 + 7X2 = indx(X1,X2) activate(n__from(X)) = X + 0 >= X + 0 = from(X) activate(X) = X >= X = X problem: DPs: from#(X) -> activate#(X) activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) activate#(n__dbls(X)) -> dbls#(X) dbls#(cons(X,Y)) -> activate#(Y) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) dbls#(cons(X,Y)) -> activate#(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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [from#](x0) = x0 + 0, [indx#](x0, x1) = x0 + x1 + 0, [sel#](x0, x1) = x0 + x1 + 0, [dbls#](x0) = x0 + 0, [activate#](x0) = x0 + 0, [dbl#](x0) = x0 + 0, [n__from](x0) = x0 + 0, [from](x0) = x0 + 0, [n__indx](x0, x1) = x0 + x1 + 0, [n__sel](x0, x1) = x0 + x1 + 0, [indx](x0, x1) = x0 + x1 + 0, [sel](x0, x1) = x0 + x1 + 0, [n__dbls](x0) = 4x0 + 4, [cons](x0, x1) = x0 + x1 + 0, [dbls](x0) = 4x0 + 4, [nil] = 3, [n__s](x0) = x0 + 0, [n__dbl](x0) = 4x0 + 0, [activate](x0) = x0 + 0, [s](x0) = x0 + 0, [dbl](x0) = 4x0 + 0, [0] = 0 orientation: from#(X) = X + 0 >= X + 0 = activate#(X) activate#(n__dbl(X)) = 4X + 0 >= X + 0 = dbl#(X) dbl#(s(X)) = X + 0 >= X + 0 = activate#(X) activate#(n__dbls(X)) = 4X + 4 >= X + 0 = dbls#(X) dbls#(cons(X,Y)) = X + Y + 0 >= Y + 0 = activate#(Y) activate#(n__sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = sel#(X1,X2) sel#(0(),cons(X,Y)) = X + Y + 0 >= X + 0 = activate#(X) activate#(n__indx(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = indx#(X1,X2) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Y + 0 = activate#(Y) activate#(n__from(X)) = X + 0 >= X + 0 = from#(X) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Z + 0 = activate#(Z) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= X + 0 = activate#(X) sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= Z + 0 = activate#(Z) sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Z + 0 = sel#(activate(X),activate(Z)) dbls#(cons(X,Y)) = X + Y + 0 >= X + 0 = activate#(X) dbl(0()) = 4 >= 0 = 0() dbl(s(X)) = 4X + 4 >= 4X + 4 = s(n__s(n__dbl(activate(X)))) dbls(nil()) = 7 >= 3 = nil() dbls(cons(X,Y)) = 4X + 4Y + 4 >= 4X + 4Y + 4 = cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) = X + Y + 0 >= X + 0 = activate(X) sel(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Z + 0 = sel(activate(X),activate(Z)) indx(nil(),X) = X + 3 >= 3 = nil() indx(cons(X,Y),Z) = X + Y + Z + 0 >= X + Y + Z + 0 = cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) = X + 0 >= X + 0 = cons(activate(X),n__from(n__s(activate(X)))) s(X) = X + 0 >= X + 0 = n__s(X) dbl(X) = 4X + 0 >= 4X + 0 = n__dbl(X) dbls(X) = 4X + 4 >= 4X + 4 = n__dbls(X) sel(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__sel(X1,X2) indx(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__indx(X1,X2) from(X) = X + 0 >= X + 0 = n__from(X) activate(n__s(X)) = X + 0 >= X + 0 = s(X) activate(n__dbl(X)) = 4X + 0 >= 4X + 0 = dbl(X) activate(n__dbls(X)) = 4X + 4 >= 4X + 4 = dbls(X) activate(n__sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2) activate(n__indx(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = indx(X1,X2) activate(n__from(X)) = X + 0 >= X + 0 = from(X) activate(X) = X + 0 >= X = X problem: DPs: from#(X) -> activate#(X) activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) dbls#(cons(X,Y)) -> activate#(Y) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) dbls#(cons(X,Y)) -> activate#(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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X SCC Processor: #sccs: 1 #rules: 12 #arcs: 65/196 DPs: from#(X) -> activate#(X) activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__from(X)) -> from#(X) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [from#](x0) = 4x0, [indx#](x0, x1) = x0 + x1 + 0, [sel#](x0, x1) = x1, [activate#](x0) = x0, [dbl#](x0) = x0, [n__from](x0) = 6x0, [from](x0) = 6x0, [n__indx](x0, x1) = x0 + x1 + 0, [n__sel](x0, x1) = x1, [indx](x0, x1) = x0 + x1 + 0, [sel](x0, x1) = x1, [n__dbls](x0) = 2x0, [cons](x0, x1) = x0 + x1, [dbls](x0) = 2x0, [nil] = 4, [n__s](x0) = x0, [n__dbl](x0) = x0, [activate](x0) = x0, [s](x0) = x0, [dbl](x0) = x0, [0] = 0 orientation: from#(X) = 4X >= X = activate#(X) activate#(n__dbl(X)) = X >= X = dbl#(X) dbl#(s(X)) = X >= X = activate#(X) activate#(n__sel(X1,X2)) = X2 >= X2 = sel#(X1,X2) sel#(0(),cons(X,Y)) = X + Y >= X = activate#(X) activate#(n__indx(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = indx#(X1,X2) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Y = activate#(Y) activate#(n__from(X)) = 6X >= 4X = from#(X) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Z = activate#(Z) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= X = activate#(X) sel#(s(X),cons(Y,Z)) = Y + Z >= Z = activate#(Z) sel#(s(X),cons(Y,Z)) = Y + Z >= Z = sel#(activate(X),activate(Z)) dbl(0()) = 0 >= 0 = 0() dbl(s(X)) = X >= X = s(n__s(n__dbl(activate(X)))) dbls(nil()) = 6 >= 4 = nil() dbls(cons(X,Y)) = 2X + 2Y >= X + 2Y = cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) = X + Y >= X = activate(X) sel(s(X),cons(Y,Z)) = Y + Z >= Z = sel(activate(X),activate(Z)) indx(nil(),X) = X + 4 >= 4 = nil() indx(cons(X,Y),Z) = X + Y + Z + 0 >= Y + Z + 0 = cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) = 6X >= 6X = cons(activate(X),n__from(n__s(activate(X)))) s(X) = X >= X = n__s(X) dbl(X) = X >= X = n__dbl(X) dbls(X) = 2X >= 2X = n__dbls(X) sel(X1,X2) = X2 >= X2 = n__sel(X1,X2) indx(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__indx(X1,X2) from(X) = 6X >= 6X = n__from(X) activate(n__s(X)) = X >= X = s(X) activate(n__dbl(X)) = X >= X = dbl(X) activate(n__dbls(X)) = 2X >= 2X = dbls(X) activate(n__sel(X1,X2)) = X2 >= X2 = sel(X1,X2) activate(n__indx(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = indx(X1,X2) activate(n__from(X)) = 6X >= 6X = from(X) activate(X) = X >= X = X problem: DPs: activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) indx#(cons(X,Y),Z) -> activate#(Z) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [indx#](x0, x1) = x0 + 2x1, [sel#](x0, x1) = x0 + x1, [activate#](x0) = x0, [dbl#](x0) = x0, [n__from](x0) = x0, [from](x0) = x0, [n__indx](x0, x1) = x0 + 2x1, [n__sel](x0, x1) = x0 + x1, [indx](x0, x1) = x0 + 2x1, [sel](x0, x1) = x0 + x1, [n__dbls](x0) = x0 + 0, [cons](x0, x1) = x0 + x1, [dbls](x0) = x0 + 0, [nil] = 4, [n__s](x0) = x0, [n__dbl](x0) = x0, [activate](x0) = x0, [s](x0) = x0, [dbl](x0) = x0, [0] = 0 orientation: activate#(n__dbl(X)) = X >= X = dbl#(X) dbl#(s(X)) = X >= X = activate#(X) activate#(n__sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel#(X1,X2) sel#(0(),cons(X,Y)) = X + Y + 0 >= X = activate#(X) activate#(n__indx(X1,X2)) = X1 + 2X2 >= X1 + 2X2 = indx#(X1,X2) indx#(cons(X,Y),Z) = X + Y + 2Z >= Y = activate#(Y) indx#(cons(X,Y),Z) = X + Y + 2Z >= Z = activate#(Z) indx#(cons(X,Y),Z) = X + Y + 2Z >= X = activate#(X) sel#(s(X),cons(Y,Z)) = X + Y + Z >= Z = activate#(Z) sel#(s(X),cons(Y,Z)) = X + Y + Z >= X + Z = sel#(activate(X),activate(Z)) dbl(0()) = 0 >= 0 = 0() dbl(s(X)) = X >= X = s(n__s(n__dbl(activate(X)))) dbls(nil()) = 4 >= 4 = nil() dbls(cons(X,Y)) = X + Y + 0 >= X + Y + 0 = cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) = X + Y + 0 >= X = activate(X) sel(s(X),cons(Y,Z)) = X + Y + Z >= X + Z = sel(activate(X),activate(Z)) indx(nil(),X) = 2X + 4 >= 4 = nil() indx(cons(X,Y),Z) = X + Y + 2Z >= X + Y + 2Z = cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) = X >= X = cons(activate(X),n__from(n__s(activate(X)))) s(X) = X >= X = n__s(X) dbl(X) = X >= X = n__dbl(X) dbls(X) = X + 0 >= X + 0 = n__dbls(X) sel(X1,X2) = X1 + X2 >= X1 + X2 = n__sel(X1,X2) indx(X1,X2) = X1 + 2X2 >= X1 + 2X2 = n__indx(X1,X2) from(X) = X >= X = n__from(X) activate(n__s(X)) = X >= X = s(X) activate(n__dbl(X)) = X >= X = dbl(X) activate(n__dbls(X)) = X + 0 >= X + 0 = dbls(X) activate(n__sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(X1,X2) activate(n__indx(X1,X2)) = X1 + 2X2 >= X1 + 2X2 = indx(X1,X2) activate(n__from(X)) = X >= X = from(X) activate(X) = X >= X = X problem: DPs: activate#(n__dbl(X)) -> dbl#(X) dbl#(s(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [indx#](x0, x1) = x0 + x1, [sel#](x0, x1) = x0 + x1 + 0, [activate#](x0) = x0, [dbl#](x0) = x0, [n__from](x0) = 2x0 + 2, [from](x0) = 2x0 + 2, [n__indx](x0, x1) = x0 + x1, [n__sel](x0, x1) = x0 + x1 + 0, [indx](x0, x1) = x0 + x1, [sel](x0, x1) = x0 + x1 + 0, [n__dbls](x0) = 2x0 + 6, [cons](x0, x1) = x0 + x1 + 0, [dbls](x0) = 2x0 + 6, [nil] = 5, [n__s](x0) = x0 + 0, [n__dbl](x0) = 2x0, [activate](x0) = x0 + 0, [s](x0) = x0 + 0, [dbl](x0) = 2x0, [0] = 0 orientation: activate#(n__dbl(X)) = 2X >= X = dbl#(X) dbl#(s(X)) = X + 0 >= X = activate#(X) activate#(n__sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = sel#(X1,X2) sel#(0(),cons(X,Y)) = X + Y + 0 >= X = activate#(X) activate#(n__indx(X1,X2)) = X1 + X2 >= X1 + X2 = indx#(X1,X2) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= Y = activate#(Y) indx#(cons(X,Y),Z) = X + Y + Z + 0 >= X = activate#(X) sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= Z = activate#(Z) sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Z + 0 = sel#(activate(X),activate(Z)) dbl(0()) = 2 >= 0 = 0() dbl(s(X)) = 2X + 2 >= 2X + 2 = s(n__s(n__dbl(activate(X)))) dbls(nil()) = 7 >= 5 = nil() dbls(cons(X,Y)) = 2X + 2Y + 6 >= 2X + 2Y + 6 = cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) = X + Y + 0 >= X + 0 = activate(X) sel(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Z + 0 = sel(activate(X),activate(Z)) indx(nil(),X) = X + 5 >= 5 = nil() indx(cons(X,Y),Z) = X + Y + Z + 0 >= X + Y + Z + 0 = cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) = 2X + 2 >= 2X + 2 = cons(activate(X),n__from(n__s(activate(X)))) s(X) = X + 0 >= X + 0 = n__s(X) dbl(X) = 2X >= 2X = n__dbl(X) dbls(X) = 2X + 6 >= 2X + 6 = n__dbls(X) sel(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__sel(X1,X2) indx(X1,X2) = X1 + X2 >= X1 + X2 = n__indx(X1,X2) from(X) = 2X + 2 >= 2X + 2 = n__from(X) activate(n__s(X)) = X + 0 >= X + 0 = s(X) activate(n__dbl(X)) = 2X + 0 >= 2X = dbl(X) activate(n__dbls(X)) = 2X + 6 >= 2X + 6 = dbls(X) activate(n__sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2) activate(n__indx(X1,X2)) = X1 + X2 + 0 >= X1 + X2 = indx(X1,X2) activate(n__from(X)) = 2X + 2 >= 2X + 2 = from(X) activate(X) = X + 0 >= X = X problem: DPs: dbl#(s(X)) -> activate#(X) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(Y) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X SCC Processor: #sccs: 1 #rules: 7 #arcs: 39/64 DPs: indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__sel(X1,X2)) -> sel#(X1,X2) sel#(0(),cons(X,Y)) -> activate#(X) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [indx#](x0, x1) = x0 + 0, [sel#](x0, x1) = 1x1, [activate#](x0) = x0, [n__from](x0) = 1x0 + 6, [from](x0) = 1x0 + 6, [n__indx](x0, x1) = x0 + 7x1 + 0, [n__sel](x0, x1) = 4x1, [indx](x0, x1) = x0 + 7x1 + 0, [sel](x0, x1) = 4x1, [n__dbls](x0) = 1x0 + 4, [cons](x0, x1) = x0 + x1, [dbls](x0) = 1x0 + 4, [nil] = 0, [n__s](x0) = 5, [n__dbl](x0) = 1x0, [activate](x0) = x0, [s](x0) = 5, [dbl](x0) = 1x0, [0] = 0 orientation: indx#(cons(X,Y),Z) = X + Y + 0 >= Y = activate#(Y) activate#(n__sel(X1,X2)) = 4X2 >= 1X2 = sel#(X1,X2) sel#(0(),cons(X,Y)) = 1X + 1Y >= X = activate#(X) activate#(n__indx(X1,X2)) = X1 + 7X2 + 0 >= X1 + 0 = indx#(X1,X2) indx#(cons(X,Y),Z) = X + Y + 0 >= X = activate#(X) sel#(s(X),cons(Y,Z)) = 1Y + 1Z >= Z = activate#(Z) sel#(s(X),cons(Y,Z)) = 1Y + 1Z >= 1Z = sel#(activate(X),activate(Z)) dbl(0()) = 1 >= 0 = 0() dbl(s(X)) = 6 >= 5 = s(n__s(n__dbl(activate(X)))) dbls(nil()) = 4 >= 0 = nil() dbls(cons(X,Y)) = 1X + 1Y + 4 >= 1X + 1Y + 4 = cons(n__dbl(activate(X)),n__dbls(activate(Y))) sel(0(),cons(X,Y)) = 4X + 4Y >= X = activate(X) sel(s(X),cons(Y,Z)) = 4Y + 4Z >= 4Z = sel(activate(X),activate(Z)) indx(nil(),X) = 7X + 0 >= 0 = nil() indx(cons(X,Y),Z) = X + Y + 7Z + 0 >= Y + 7Z + 0 = cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) from(X) = 1X + 6 >= X + 6 = cons(activate(X),n__from(n__s(activate(X)))) s(X) = 5 >= 5 = n__s(X) dbl(X) = 1X >= 1X = n__dbl(X) dbls(X) = 1X + 4 >= 1X + 4 = n__dbls(X) sel(X1,X2) = 4X2 >= 4X2 = n__sel(X1,X2) indx(X1,X2) = X1 + 7X2 + 0 >= X1 + 7X2 + 0 = n__indx(X1,X2) from(X) = 1X + 6 >= 1X + 6 = n__from(X) activate(n__s(X)) = 5 >= 5 = s(X) activate(n__dbl(X)) = 1X >= 1X = dbl(X) activate(n__dbls(X)) = 1X + 4 >= 1X + 4 = dbls(X) activate(n__sel(X1,X2)) = 4X2 >= 4X2 = sel(X1,X2) activate(n__indx(X1,X2)) = X1 + 7X2 + 0 >= X1 + 7X2 + 0 = indx(X1,X2) activate(n__from(X)) = 1X + 6 >= 1X + 6 = from(X) activate(X) = X >= X = X problem: DPs: indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(X) sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X SCC Processor: #sccs: 2 #rules: 4 #arcs: 16/16 DPs: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z)) 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Open DPs: indx#(cons(X,Y),Z) -> activate#(Y) activate#(n__indx(X1,X2)) -> indx#(X1,X2) indx#(cons(X,Y),Z) -> activate#(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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Subterm Criterion Processor: simple projection: pi(activate#) = 0 pi(indx#) = 0 problem: DPs: 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(X) activate(n__dbls(X)) -> dbls(X) activate(n__sel(X1,X2)) -> sel(X1,X2) activate(n__indx(X1,X2)) -> indx(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Qed