MAYBE Problem: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Proof: DP Processor: DPs: a__sel#(0(),cons(X,Y)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) mark#(dbl(X)) -> mark#(X) mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(dbls(X)) -> mark#(X) mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(indx(X1,X2)) -> mark#(X1) mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(from(X)) -> a__from#(X) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) TDG Processor: DPs: a__sel#(0(),cons(X,Y)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) mark#(dbl(X)) -> mark#(X) mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(dbls(X)) -> mark#(X) mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(indx(X1,X2)) -> mark#(X1) mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(from(X)) -> a__from#(X) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) graph: mark#(indx(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> a__from#(X) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(indx(X1,X2)) -> mark#(X1) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(indx(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> a__from#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(indx(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbls(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> a__from#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(indx(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbls(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(s(X),cons(Y,Z)) -> mark#(X) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(s(X),cons(Y,Z)) -> mark#(Z) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(0(),cons(X,Y)) -> mark#(X) mark#(dbls(X)) -> mark#(X) -> mark#(from(X)) -> a__from#(X) mark#(dbls(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(dbls(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1) mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(dbls(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(dbls(X)) -> mark#(X) -> mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(dbls(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X) mark#(dbls(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(dbls(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X) mark#(dbl(X)) -> mark#(X) -> mark#(from(X)) -> a__from#(X) mark#(dbl(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) mark#(dbl(X)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1) mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(dbl(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> a__dbls#(mark(X)) mark#(dbl(X)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X) mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X)) mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(from(X)) -> a__from#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(indx(X1,X2)) -> mark#(X1) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(dbls(X)) -> a__dbls#(mark(X)) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(dbls(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(dbl(X)) -> a__dbl#(mark(X)) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(dbl(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(from(X)) -> a__from#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(dbls(X)) -> a__dbls#(mark(X)) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X)) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) -> a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) -> a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) -> a__sel#(s(X),cons(Y,Z)) -> mark#(Z) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) -> a__sel#(0(),cons(X,Y)) -> mark#(X) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(from(X)) -> a__from#(X) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(indx(X1,X2)) -> a__indx#(mark(X1),X2) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(indx(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(dbls(X)) -> a__dbls#(mark(X)) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(dbls(X)) -> mark#(X) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X)) a__sel#(0(),cons(X,Y)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X) SCC Processor: #sccs: 1 #rules: 10 #arcs: 88/196 DPs: mark#(indx(X1,X2)) -> mark#(X1) mark#(dbl(X)) -> mark#(X) mark#(dbls(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Y)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__sel#](x0, x1) = x0 + x1 + 0, [from](x0) = 4x0 + 5, [a__from](x0) = 4x0 + 5, [indx](x0, x1) = x0 + 1x1, [sel](x0, x1) = x0 + x1 + 0, [a__indx](x0, x1) = x0 + 1x1, [mark](x0) = x0, [a__sel](x0, x1) = x0 + x1 + 0, [dbls](x0) = 4x0 + 4, [cons](x0, x1) = x0 + x1 + 0, [a__dbls](x0) = 4x0 + 4, [nil] = 0, [dbl](x0) = x0 + 1, [s](x0) = x0 + 1, [a__dbl](x0) = x0 + 1, [0] = 0 orientation: mark#(indx(X1,X2)) = X1 + 1X2 >= X1 = mark#(X1) mark#(dbl(X)) = X + 1 >= X = mark#(X) mark#(dbls(X)) = 4X + 4 >= X = mark#(X) mark#(sel(X1,X2)) = X1 + X2 + 0 >= X2 = mark#(X2) mark#(sel(X1,X2)) = X1 + X2 + 0 >= X1 = mark#(X1) mark#(sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Y)) = X + Y + 0 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + Y + Z + 1 >= Z = mark#(Z) a__sel#(s(X),cons(Y,Z)) = X + Y + Z + 1 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + Y + Z + 1 >= X + Z + 0 = a__sel#(mark(X),mark(Z)) a__dbl(0()) = 1 >= 0 = 0() a__dbl(s(X)) = X + 1 >= X + 1 = s(s(dbl(X))) a__dbls(nil()) = 4 >= 0 = nil() a__dbls(cons(X,Y)) = 4X + 4Y + 4 >= X + 4Y + 4 = cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) = X + Y + 0 >= X = mark(X) a__sel(s(X),cons(Y,Z)) = X + Y + Z + 1 >= X + Z + 0 = a__sel(mark(X),mark(Z)) a__indx(nil(),X) = 1X + 0 >= 0 = nil() a__indx(cons(X,Y),Z) = X + Y + 1Z + 0 >= X + Y + 1Z + 0 = cons(sel(X,Z),indx(Y,Z)) a__from(X) = 4X + 5 >= 4X + 5 = cons(X,from(s(X))) mark(dbl(X)) = X + 1 >= X + 1 = a__dbl(mark(X)) mark(dbls(X)) = 4X + 4 >= 4X + 4 = a__dbls(mark(X)) mark(sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) = X1 + 1X2 >= X1 + 1X2 = a__indx(mark(X1),X2) mark(from(X)) = 4X + 5 >= 4X + 5 = a__from(X) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X + 1 >= X + 1 = s(X) mark(nil()) = 0 >= 0 = nil() mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2) a__dbl(X) = X + 1 >= X + 1 = dbl(X) a__dbls(X) = 4X + 4 >= 4X + 4 = dbls(X) a__sel(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2) a__indx(X1,X2) = X1 + 1X2 >= X1 + 1X2 = indx(X1,X2) a__from(X) = 4X + 5 >= 4X + 5 = from(X) problem: DPs: mark#(indx(X1,X2)) -> mark#(X1) mark#(dbl(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Y)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__sel#](x0, x1) = x0 + 2x1 + 0, [from](x0) = x0 + 6, [a__from](x0) = x0 + 6, [indx](x0, x1) = 2x0 + 4x1 + 5, [sel](x0, x1) = x0 + 2x1 + 3, [a__indx](x0, x1) = 2x0 + 4x1 + 5, [mark](x0) = x0 + 0, [a__sel](x0, x1) = x0 + 2x1 + 3, [dbls](x0) = 4x0 + 4, [cons](x0, x1) = x0 + x1, [a__dbls](x0) = 4x0 + 4, [nil] = 2, [dbl](x0) = x0, [s](x0) = x0 + 2, [a__dbl](x0) = x0 + 0, [0] = 6 orientation: mark#(indx(X1,X2)) = 2X1 + 4X2 + 5 >= X1 = mark#(X1) mark#(dbl(X)) = X >= X = mark#(X) mark#(sel(X1,X2)) = X1 + 2X2 + 3 >= X2 = mark#(X2) mark#(sel(X1,X2)) = X1 + 2X2 + 3 >= X1 = mark#(X1) mark#(sel(X1,X2)) = X1 + 2X2 + 3 >= X1 + 2X2 + 2 = a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Y)) = 2X + 2Y + 6 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + 2Y + 2Z + 2 >= Z = mark#(Z) a__sel#(s(X),cons(Y,Z)) = X + 2Y + 2Z + 2 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + 2Y + 2Z + 2 >= X + 2Z + 2 = a__sel#(mark(X),mark(Z)) a__dbl(0()) = 6 >= 6 = 0() a__dbl(s(X)) = X + 2 >= X + 2 = s(s(dbl(X))) a__dbls(nil()) = 6 >= 2 = nil() a__dbls(cons(X,Y)) = 4X + 4Y + 4 >= X + 4Y + 4 = cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) = 2X + 2Y + 6 >= X + 0 = mark(X) a__sel(s(X),cons(Y,Z)) = X + 2Y + 2Z + 3 >= X + 2Z + 3 = a__sel(mark(X),mark(Z)) a__indx(nil(),X) = 4X + 5 >= 2 = nil() a__indx(cons(X,Y),Z) = 2X + 2Y + 4Z + 5 >= X + 2Y + 4Z + 5 = cons(sel(X,Z),indx(Y,Z)) a__from(X) = X + 6 >= X + 6 = cons(X,from(s(X))) mark(dbl(X)) = X + 0 >= X + 0 = a__dbl(mark(X)) mark(dbls(X)) = 4X + 4 >= 4X + 4 = a__dbls(mark(X)) mark(sel(X1,X2)) = X1 + 2X2 + 3 >= X1 + 2X2 + 3 = a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) = 2X1 + 4X2 + 5 >= 2X1 + 4X2 + 5 = a__indx(mark(X1),X2) mark(from(X)) = X + 6 >= X + 6 = a__from(X) mark(0()) = 6 >= 6 = 0() mark(s(X)) = X + 2 >= X + 2 = s(X) mark(nil()) = 2 >= 2 = nil() mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 = cons(X1,X2) a__dbl(X) = X + 0 >= X = dbl(X) a__dbls(X) = 4X + 4 >= 4X + 4 = dbls(X) a__sel(X1,X2) = X1 + 2X2 + 3 >= X1 + 2X2 + 3 = sel(X1,X2) a__indx(X1,X2) = 2X1 + 4X2 + 5 >= 2X1 + 4X2 + 5 = indx(X1,X2) a__from(X) = X + 6 >= X + 6 = from(X) problem: DPs: mark#(dbl(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__sel#](x0, x1) = 7x0 + 4x1, [from](x0) = 4x0 + 0, [a__from](x0) = 4x0 + 0, [indx](x0, x1) = 7x0 + 4x1, [sel](x0, x1) = 7x0 + 4x1 + 0, [a__indx](x0, x1) = 7x0 + 4x1, [mark](x0) = x0, [a__sel](x0, x1) = 7x0 + 4x1 + 0, [dbls](x0) = 6x0 + 0, [cons](x0, x1) = x0 + x1 + 0, [a__dbls](x0) = 6x0 + 0, [nil] = 0, [dbl](x0) = x0 + 2, [s](x0) = x0, [a__dbl](x0) = x0 + 2, [0] = 0 orientation: mark#(dbl(X)) = X + 2 >= X = mark#(X) mark#(sel(X1,X2)) = 7X1 + 4X2 + 0 >= X1 = mark#(X1) mark#(sel(X1,X2)) = 7X1 + 4X2 + 0 >= 7X1 + 4X2 = a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) = 7X + 4Y + 4Z + 4 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = 7X + 4Y + 4Z + 4 >= 7X + 4Z = a__sel#(mark(X),mark(Z)) a__dbl(0()) = 2 >= 0 = 0() a__dbl(s(X)) = X + 2 >= X + 2 = s(s(dbl(X))) a__dbls(nil()) = 6 >= 0 = nil() a__dbls(cons(X,Y)) = 6X + 6Y + 6 >= X + 6Y + 2 = cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) = 4X + 4Y + 7 >= X = mark(X) a__sel(s(X),cons(Y,Z)) = 7X + 4Y + 4Z + 4 >= 7X + 4Z + 0 = a__sel(mark(X),mark(Z)) a__indx(nil(),X) = 4X + 7 >= 0 = nil() a__indx(cons(X,Y),Z) = 7X + 7Y + 4Z + 7 >= 7X + 7Y + 4Z + 0 = cons(sel(X,Z),indx(Y,Z)) a__from(X) = 4X + 0 >= 4X + 0 = cons(X,from(s(X))) mark(dbl(X)) = X + 2 >= X + 2 = a__dbl(mark(X)) mark(dbls(X)) = 6X + 0 >= 6X + 0 = a__dbls(mark(X)) mark(sel(X1,X2)) = 7X1 + 4X2 + 0 >= 7X1 + 4X2 + 0 = a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) = 7X1 + 4X2 >= 7X1 + 4X2 = a__indx(mark(X1),X2) mark(from(X)) = 4X + 0 >= 4X + 0 = a__from(X) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X >= X = s(X) mark(nil()) = 0 >= 0 = nil() mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2) a__dbl(X) = X + 2 >= X + 2 = dbl(X) a__dbls(X) = 6X + 0 >= 6X + 0 = dbls(X) a__sel(X1,X2) = 7X1 + 4X2 + 0 >= 7X1 + 4X2 + 0 = sel(X1,X2) a__indx(X1,X2) = 7X1 + 4X2 >= 7X1 + 4X2 = indx(X1,X2) a__from(X) = 4X + 0 >= 4X + 0 = from(X) problem: DPs: mark#(dbl(X)) -> mark#(X) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) SCC Processor: #sccs: 2 #rules: 2 #arcs: 56/9 DPs: mark#(dbl(X)) -> mark#(X) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Subterm Criterion Processor: simple projection: pi(mark#) = 0 problem: DPs: TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Qed DPs: a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__dbls(nil()) -> nil() a__dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) a__sel(0(),cons(X,Y)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) a__indx(nil(),X) -> nil() a__indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) a__from(X) -> cons(X,from(s(X))) mark(dbl(X)) -> a__dbl(mark(X)) mark(dbls(X)) -> a__dbls(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(indx(X1,X2)) -> a__indx(mark(X1),X2) mark(from(X)) -> a__from(X) mark(0()) -> 0() mark(s(X)) -> s(X) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(X1,X2) a__dbl(X) -> dbl(X) a__dbls(X) -> dbls(X) a__sel(X1,X2) -> sel(X1,X2) a__indx(X1,X2) -> indx(X1,X2) a__from(X) -> from(X) Open