MAYBE Problem: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Proof: DP Processor: DPs: a__from#(X) -> mark#(X) a__first#(s(X),cons(Y,Z)) -> mark#(Y) a__sel#(0(),cons(X,Z)) -> 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#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) mark#(first(X1,X2)) -> mark#(X2) mark#(first(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) TDG Processor: DPs: a__from#(X) -> mark#(X) a__first#(s(X),cons(Y,Z)) -> mark#(Y) a__sel#(0(),cons(X,Z)) -> 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#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) mark#(first(X1,X2)) -> mark#(X2) mark#(first(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) graph: a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(from(X)) -> a__from#(mark(X)) a__sel#(0(),cons(X,Z)) -> mark#(X) -> mark#(from(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,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(s(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(cons(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#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(first(X1,X2)) -> mark#(X1) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(first(X1,X2)) -> mark#(X2) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(from(X)) -> a__from#(mark(X)) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) -> mark#(from(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(cons(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#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(from(X)) -> a__from#(mark(X)) a__sel#(s(X),cons(Y,Z)) -> mark#(X) -> mark#(from(X)) -> mark#(X) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(s(X)) -> mark#(X) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(cons(X1,X2)) -> mark#(X1) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(sel(X1,X2)) -> mark#(X1) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(sel(X1,X2)) -> mark#(X2) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(first(X1,X2)) -> mark#(X1) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(first(X1,X2)) -> mark#(X2) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(from(X)) -> a__from#(mark(X)) a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(from(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,Z)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(cons(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#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(first(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(first(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> a__from#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(cons(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#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> a__from#(mark(X)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X) mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) -> a__first#(s(X),cons(Y,Z)) -> mark#(Y) mark#(first(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(first(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(first(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(first(X1,X2)) -> mark#(X2) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(first(X1,X2)) -> mark#(X2) -> mark#(first(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> mark#(X2) -> mark#(first(X1,X2)) -> mark#(X2) mark#(first(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> a__from#(mark(X)) mark#(first(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X) mark#(first(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(first(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(first(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(first(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(first(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> mark#(X1) mark#(first(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> mark#(X2) mark#(first(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> a__from#(mark(X)) mark#(first(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(first(X1,X2)) -> mark#(X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> a__from#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X) mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(from(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(from(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(from(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(from(X)) -> mark#(X) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(from(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1) mark#(from(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2) mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> a__from#(mark(X)) mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) -> a__from#(X) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> a__from#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X) a__from#(X) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__from#(X) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) a__from#(X) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__from#(X) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__from#(X) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__from#(X) -> mark#(X) -> mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) a__from#(X) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1) a__from#(X) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2) a__from#(X) -> mark#(X) -> mark#(from(X)) -> a__from#(mark(X)) a__from#(X) -> mark#(X) -> mark#(from(X)) -> mark#(X) Arctic Interpretation Processor: dimension: 1 interpretation: [a__sel#](x0, x1) = x0 + x1 + 0, [a__first#](x0, x1) = x0 + x1 + 0, [mark#](x0) = x0 + 0, [a__from#](x0) = x0 + 0, [sel](x0, x1) = x0 + x1 + 0, [a__sel](x0, x1) = x0 + x1 + 0, [first](x0, x1) = 2x0 + 1x1 + 2, [nil] = 2, [a__first](x0, x1) = 2x0 + 1x1 + 2, [0] = 0, [cons](x0, x1) = x0 + x1 + 0, [from](x0) = x0 + 0, [s](x0) = x0 + 0, [mark](x0) = x0 + 0, [a__from](x0) = x0 + 0 orientation: a__from#(X) = X + 0 >= X + 0 = mark#(X) a__first#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= Y + 0 = mark#(Y) a__sel#(0(),cons(X,Z)) = X + Z + 0 >= X + 0 = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= Z + 0 = mark#(Z) a__sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + 0 = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Z + 0 = a__sel#(mark(X),mark(Z)) mark#(from(X)) = X + 0 >= X + 0 = mark#(X) mark#(from(X)) = X + 0 >= X + 0 = a__from#(mark(X)) mark#(first(X1,X2)) = 2X1 + 1X2 + 2 >= X2 + 0 = mark#(X2) mark#(first(X1,X2)) = 2X1 + 1X2 + 2 >= X1 + 0 = mark#(X1) mark#(first(X1,X2)) = 2X1 + 1X2 + 2 >= X1 + X2 + 0 = a__first#(mark(X1),mark(X2)) mark#(sel(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = mark#(X2) mark#(sel(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1) mark#(sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__sel#(mark(X1),mark(X2)) mark#(cons(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1) mark#(s(X)) = X + 0 >= X + 0 = mark#(X) a__from(X) = X + 0 >= X + 0 = cons(mark(X),from(s(X))) a__first(0(),Z) = 1Z + 2 >= 2 = nil() a__first(s(X),cons(Y,Z)) = 2X + 1Y + 1Z + 2 >= 2X + Y + 1Z + 2 = cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) = X + Z + 0 >= X + 0 = mark(X) a__sel(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Z + 0 = a__sel(mark(X),mark(Z)) mark(from(X)) = X + 0 >= X + 0 = a__from(mark(X)) mark(first(X1,X2)) = 2X1 + 1X2 + 2 >= 2X1 + 1X2 + 2 = a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(mark(X1),X2) mark(s(X)) = X + 0 >= X + 0 = s(mark(X)) mark(0()) = 0 >= 0 = 0() mark(nil()) = 2 >= 2 = nil() a__from(X) = X + 0 >= X + 0 = from(X) a__first(X1,X2) = 2X1 + 1X2 + 2 >= 2X1 + 1X2 + 2 = first(X1,X2) a__sel(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = sel(X1,X2) problem: DPs: a__from#(X) -> mark#(X) a__first#(s(X),cons(Y,Z)) -> mark#(Y) a__sel#(0(),cons(X,Z)) -> 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#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(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#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) SCC Processor: #sccs: 1 #rules: 12 #arcs: 130/169 DPs: a__sel#(0(),cons(X,Z)) -> mark#(X) mark#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) a__from#(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#(s(X),cons(Y,Z)) -> mark#(Z) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Arctic Interpretation Processor: dimension: 1 interpretation: [a__sel#](x0, x1) = x0 + 2x1 + 4, [mark#](x0) = x0 + 4, [a__from#](x0) = x0 + 4, [sel](x0, x1) = 1x0 + 2x1 + 0, [a__sel](x0, x1) = 1x0 + 2x1 + 0, [first](x0, x1) = x0 + x1, [nil] = 0, [a__first](x0, x1) = x0 + x1, [0] = 5, [cons](x0, x1) = x0 + x1, [from](x0) = x0 + 0, [s](x0) = x0 + 0, [mark](x0) = x0, [a__from](x0) = x0 + 0 orientation: a__sel#(0(),cons(X,Z)) = 2X + 2Z + 5 >= X + 4 = mark#(X) mark#(from(X)) = X + 4 >= X + 4 = mark#(X) mark#(from(X)) = X + 4 >= X + 4 = a__from#(mark(X)) a__from#(X) = X + 4 >= X + 4 = mark#(X) mark#(sel(X1,X2)) = 1X1 + 2X2 + 4 >= X2 + 4 = mark#(X2) mark#(sel(X1,X2)) = 1X1 + 2X2 + 4 >= X1 + 4 = mark#(X1) mark#(sel(X1,X2)) = 1X1 + 2X2 + 4 >= X1 + 2X2 + 4 = a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) = X + 2Y + 2Z + 4 >= Z + 4 = mark#(Z) mark#(cons(X1,X2)) = X1 + X2 + 4 >= X1 + 4 = mark#(X1) mark#(s(X)) = X + 4 >= X + 4 = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + 2Y + 2Z + 4 >= X + 4 = mark#(X) a__sel#(s(X),cons(Y,Z)) = X + 2Y + 2Z + 4 >= X + 2Z + 4 = a__sel#(mark(X),mark(Z)) a__from(X) = X + 0 >= X + 0 = cons(mark(X),from(s(X))) a__first(0(),Z) = Z + 5 >= 0 = nil() a__first(s(X),cons(Y,Z)) = X + Y + Z + 0 >= X + Y + Z = cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) = 2X + 2Z + 6 >= X = mark(X) a__sel(s(X),cons(Y,Z)) = 1X + 2Y + 2Z + 1 >= 1X + 2Z + 0 = a__sel(mark(X),mark(Z)) mark(from(X)) = X + 0 >= X + 0 = a__from(mark(X)) mark(first(X1,X2)) = X1 + X2 >= X1 + X2 = a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) = 1X1 + 2X2 + 0 >= 1X1 + 2X2 + 0 = a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(mark(X1),X2) mark(s(X)) = X + 0 >= X + 0 = s(mark(X)) mark(0()) = 5 >= 5 = 0() mark(nil()) = 0 >= 0 = nil() a__from(X) = X + 0 >= X + 0 = from(X) a__first(X1,X2) = X1 + X2 >= X1 + X2 = first(X1,X2) a__sel(X1,X2) = 1X1 + 2X2 + 0 >= 1X1 + 2X2 + 0 = sel(X1,X2) problem: DPs: mark#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) a__from#(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#(s(X),cons(Y,Z)) -> mark#(Z) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Arctic Interpretation Processor: dimension: 1 interpretation: [a__sel#](x0, x1) = 7x0 + x1 + 0, [mark#](x0) = x0, [a__from#](x0) = x0 + 0, [sel](x0, x1) = 7x0 + x1 + 0, [a__sel](x0, x1) = 7x0 + x1 + 0, [first](x0, x1) = x1 + 0, [nil] = 0, [a__first](x0, x1) = x1 + 0, [0] = 0, [cons](x0, x1) = x0 + x1 + 0, [from](x0) = x0 + 0, [s](x0) = x0, [mark](x0) = x0, [a__from](x0) = x0 + 0 orientation: mark#(from(X)) = X + 0 >= X = mark#(X) mark#(from(X)) = X + 0 >= X + 0 = a__from#(mark(X)) a__from#(X) = X + 0 >= X = mark#(X) mark#(sel(X1,X2)) = 7X1 + X2 + 0 >= X2 = mark#(X2) mark#(sel(X1,X2)) = 7X1 + X2 + 0 >= X1 = mark#(X1) mark#(sel(X1,X2)) = 7X1 + X2 + 0 >= 7X1 + X2 + 0 = a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) = 7X + Y + Z + 0 >= Z = mark#(Z) mark#(cons(X1,X2)) = X1 + X2 + 0 >= X1 = mark#(X1) mark#(s(X)) = X >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = 7X + Y + Z + 0 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = 7X + Y + Z + 0 >= 7X + Z + 0 = a__sel#(mark(X),mark(Z)) a__from(X) = X + 0 >= X + 0 = cons(mark(X),from(s(X))) a__first(0(),Z) = Z + 0 >= 0 = nil() a__first(s(X),cons(Y,Z)) = Y + Z + 0 >= Y + Z + 0 = cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) = X + Z + 7 >= X = mark(X) a__sel(s(X),cons(Y,Z)) = 7X + Y + Z + 0 >= 7X + Z + 0 = a__sel(mark(X),mark(Z)) mark(from(X)) = X + 0 >= X + 0 = a__from(mark(X)) mark(first(X1,X2)) = X2 + 0 >= X2 + 0 = a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) = 7X1 + X2 + 0 >= 7X1 + X2 + 0 = a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(mark(X1),X2) mark(s(X)) = X >= X = s(mark(X)) mark(0()) = 0 >= 0 = 0() mark(nil()) = 0 >= 0 = nil() a__from(X) = X + 0 >= X + 0 = from(X) a__first(X1,X2) = X2 + 0 >= X2 + 0 = first(X1,X2) a__sel(X1,X2) = 7X1 + X2 + 0 >= 7X1 + X2 + 0 = sel(X1,X2) problem: DPs: mark#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) a__from#(X) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Arctic Interpretation Processor: dimension: 1 interpretation: [a__sel#](x0, x1) = x1, [mark#](x0) = x0, [a__from#](x0) = x0 + 0, [sel](x0, x1) = 1x1 + 0, [a__sel](x0, x1) = 1x1 + 0, [first](x0, x1) = 5x0 + 2x1 + 2, [nil] = 1, [a__first](x0, x1) = 5x0 + 2x1 + 2, [0] = 1, [cons](x0, x1) = x0 + x1, [from](x0) = x0 + 0, [s](x0) = x0 + 0, [mark](x0) = x0, [a__from](x0) = x0 + 0 orientation: mark#(from(X)) = X + 0 >= X = mark#(X) mark#(from(X)) = X + 0 >= X + 0 = a__from#(mark(X)) a__from#(X) = X + 0 >= X = mark#(X) mark#(sel(X1,X2)) = 1X2 + 0 >= X2 = mark#(X2) mark#(sel(X1,X2)) = 1X2 + 0 >= X2 = a__sel#(mark(X1),mark(X2)) a__sel#(s(X),cons(Y,Z)) = Y + Z >= Z = mark#(Z) mark#(cons(X1,X2)) = X1 + X2 >= X1 = mark#(X1) mark#(s(X)) = X + 0 >= X = mark#(X) a__sel#(s(X),cons(Y,Z)) = Y + Z >= Z = a__sel#(mark(X),mark(Z)) a__from(X) = X + 0 >= X + 0 = cons(mark(X),from(s(X))) a__first(0(),Z) = 2Z + 6 >= 1 = nil() a__first(s(X),cons(Y,Z)) = 5X + 2Y + 2Z + 5 >= 5X + Y + 2Z + 2 = cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) = 1X + 1Z + 0 >= X = mark(X) a__sel(s(X),cons(Y,Z)) = 1Y + 1Z + 0 >= 1Z + 0 = a__sel(mark(X),mark(Z)) mark(from(X)) = X + 0 >= X + 0 = a__from(mark(X)) mark(first(X1,X2)) = 5X1 + 2X2 + 2 >= 5X1 + 2X2 + 2 = a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) = 1X2 + 0 >= 1X2 + 0 = a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(mark(X1),X2) mark(s(X)) = X + 0 >= X + 0 = s(mark(X)) mark(0()) = 1 >= 1 = 0() mark(nil()) = 1 >= 1 = nil() a__from(X) = X + 0 >= X + 0 = from(X) a__first(X1,X2) = 5X1 + 2X2 + 2 >= 5X1 + 2X2 + 2 = first(X1,X2) a__sel(X1,X2) = 1X2 + 0 >= 1X2 + 0 = sel(X1,X2) problem: DPs: mark#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) a__from#(X) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> mark#(Z) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) SCC Processor: #sccs: 2 #rules: 6 #arcs: 72/49 DPs: a__sel#(s(X),cons(Y,Z)) -> a__sel#(mark(X),mark(Z)) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Open DPs: mark#(from(X)) -> mark#(X) mark#(from(X)) -> a__from#(mark(X)) a__from#(X) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__from#](x0) = x0 + 0, [sel](x0, x1) = 2x0 + 3x1, [a__sel](x0, x1) = 2x0 + 3x1, [first](x0, x1) = 2x1 + 6, [nil] = 0, [a__first](x0, x1) = 2x1 + 6, [0] = 4, [cons](x0, x1) = 1x0 + x1 + 0, [from](x0) = 1x0 + 4, [s](x0) = x0 + 0, [mark](x0) = x0, [a__from](x0) = 1x0 + 4 orientation: mark#(from(X)) = 1X + 4 >= X = mark#(X) mark#(from(X)) = 1X + 4 >= X + 0 = a__from#(mark(X)) a__from#(X) = X + 0 >= X = mark#(X) mark#(cons(X1,X2)) = 1X1 + X2 + 0 >= X1 = mark#(X1) mark#(s(X)) = X + 0 >= X = mark#(X) a__from(X) = 1X + 4 >= 1X + 4 = cons(mark(X),from(s(X))) a__first(0(),Z) = 2Z + 6 >= 0 = nil() a__first(s(X),cons(Y,Z)) = 3Y + 2Z + 6 >= 1Y + 2Z + 6 = cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) = 4X + 3Z + 6 >= X = mark(X) a__sel(s(X),cons(Y,Z)) = 2X + 4Y + 3Z + 3 >= 2X + 3Z = a__sel(mark(X),mark(Z)) mark(from(X)) = 1X + 4 >= 1X + 4 = a__from(mark(X)) mark(first(X1,X2)) = 2X2 + 6 >= 2X2 + 6 = a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) = 2X1 + 3X2 >= 2X1 + 3X2 = a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = cons(mark(X1),X2) mark(s(X)) = X + 0 >= X + 0 = s(mark(X)) mark(0()) = 4 >= 4 = 0() mark(nil()) = 0 >= 0 = nil() a__from(X) = 1X + 4 >= 1X + 4 = from(X) a__first(X1,X2) = 2X2 + 6 >= 2X2 + 6 = first(X1,X2) a__sel(X1,X2) = 2X1 + 3X2 >= 2X1 + 3X2 = sel(X1,X2) problem: DPs: a__from#(X) -> mark#(X) mark#(s(X)) -> mark#(X) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) SCC Processor: #sccs: 1 #rules: 1 #arcs: 17/4 DPs: mark#(s(X)) -> mark#(X) TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Subterm Criterion Processor: simple projection: pi(mark#) = 0 problem: DPs: TRS: a__from(X) -> cons(mark(X),from(s(X))) a__first(0(),Z) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) a__sel(0(),cons(X,Z)) -> mark(X) a__sel(s(X),cons(Y,Z)) -> a__sel(mark(X),mark(Z)) mark(from(X)) -> a__from(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(nil()) -> nil() a__from(X) -> from(X) a__first(X1,X2) -> first(X1,X2) a__sel(X1,X2) -> sel(X1,X2) Qed