MAYBE Problem: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X Proof: DP Processor: DPs: eq#(n__s(X),n__s(Y)) -> activate#(Y) eq#(n__s(X),n__s(Y)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) length#(nil()) -> 0#() length#(cons(X,L)) -> activate#(L) length#(cons(X,L)) -> s#(n__length(activate(L))) activate#(n__0()) -> 0#() activate#(n__s(X)) -> s#(X) activate#(n__inf(X)) -> activate#(X) activate#(n__inf(X)) -> inf#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X TDG Processor: DPs: eq#(n__s(X),n__s(Y)) -> activate#(Y) eq#(n__s(X),n__s(Y)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) length#(nil()) -> 0#() length#(cons(X,L)) -> activate#(L) length#(cons(X,L)) -> s#(n__length(activate(L))) activate#(n__0()) -> 0#() activate#(n__s(X)) -> s#(X) activate#(n__inf(X)) -> activate#(X) activate#(n__inf(X)) -> inf#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X graph: length#(cons(X,L)) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) length#(cons(X,L)) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) length#(cons(X,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) length#(cons(X,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) length#(cons(X,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) length#(cons(X,L)) -> activate#(L) -> activate#(n__inf(X)) -> inf#(activate(X)) length#(cons(X,L)) -> activate#(L) -> activate#(n__inf(X)) -> activate#(X) length#(cons(X,L)) -> activate#(L) -> activate#(n__s(X)) -> s#(X) length#(cons(X,L)) -> activate#(L) -> activate#(n__0()) -> 0#() take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__length(X)) -> length#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__length(X)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__take(X1,X2)) -> activate#(X1) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__take(X1,X2)) -> activate#(X2) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__inf(X)) -> inf#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__inf(X)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) take#(s(X),cons(Y,L)) -> activate#(Y) -> activate#(n__0()) -> 0#() take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__inf(X)) -> inf#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__inf(X)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) take#(s(X),cons(Y,L)) -> activate#(X) -> activate#(n__0()) -> 0#() take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X1) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__take(X1,X2)) -> activate#(X2) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__inf(X)) -> inf#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__inf(X)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__s(X)) -> s#(X) take#(s(X),cons(Y,L)) -> activate#(L) -> activate#(n__0()) -> 0#() activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(X,L)) -> s#(n__length(activate(L))) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(X,L)) -> activate#(L) activate#(n__length(X)) -> length#(activate(X)) -> length#(nil()) -> 0#() activate#(n__length(X)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__length(X)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__length(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__length(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__length(X)) -> activate#(X) -> activate#(n__inf(X)) -> inf#(activate(X)) activate#(n__length(X)) -> activate#(X) -> activate#(n__inf(X)) -> activate#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(X),cons(Y,L)) -> activate#(Y) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(X),cons(Y,L)) -> activate#(X) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) -> take#(s(X),cons(Y,L)) -> activate#(L) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__length(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__inf(X)) -> inf#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__inf(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(X) activate#(n__take(X1,X2)) -> activate#(X2) -> activate#(n__0()) -> 0#() activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__inf(X)) -> inf#(activate(X)) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__inf(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(X) activate#(n__take(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__inf(X)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__inf(X)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) activate#(n__inf(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) activate#(n__inf(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__inf(X)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__inf(X)) -> activate#(X) -> activate#(n__inf(X)) -> inf#(activate(X)) activate#(n__inf(X)) -> activate#(X) -> activate#(n__inf(X)) -> activate#(X) activate#(n__inf(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) activate#(n__inf(X)) -> activate#(X) -> activate#(n__0()) -> 0#() eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__length(X)) -> length#(activate(X)) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__length(X)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__take(X1,X2)) -> activate#(X1) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__take(X1,X2)) -> activate#(X2) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__inf(X)) -> inf#(activate(X)) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__inf(X)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) eq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X1) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__take(X1,X2)) -> activate#(X2) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__inf(X)) -> inf#(activate(X)) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__inf(X)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) eq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__0()) -> 0#() eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) -> eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) -> eq#(n__s(X),n__s(Y)) -> activate#(X) eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) -> eq#(n__s(X),n__s(Y)) -> activate#(Y) SCC Processor: #sccs: 2 #rules: 11 #arcs: 99/324 DPs: eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y)) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X Open DPs: length#(cons(X,L)) -> activate#(L) activate#(n__inf(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(L) activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [length#](x0) = x0 + 0, [take#](x0, x1) = x0 + x1 + 0, [activate#](x0) = x0 + 0, [n__length](x0) = 1x0 + 1, [length](x0) = 1x0 + 1, [n__take](x0, x1) = x0 + x1 + 0, [s](x0) = x0 + 0, [nil] = 0, [take](x0, x1) = x0 + x1 + 0, [0] = 1, [cons](x0, x1) = x0 + x1, [n__inf](x0) = x0, [inf](x0) = x0 + 0, [false] = 4, [activate](x0) = x0 + 0, [n__s](x0) = x0, [true] = 0, [eq](x0, x1) = 8, [n__0] = 1 orientation: length#(cons(X,L)) = L + X + 0 >= L + 0 = activate#(L) activate#(n__inf(X)) = X + 0 >= X + 0 = activate#(X) activate#(n__take(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = activate#(X2) activate#(n__take(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = activate#(X1) activate#(n__take(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) = L + X + Y + 0 >= L + 0 = activate#(L) activate#(n__length(X)) = 1X + 1 >= X + 0 = activate#(X) activate#(n__length(X)) = 1X + 1 >= X + 0 = length#(activate(X)) take#(s(X),cons(Y,L)) = L + X + Y + 0 >= X + 0 = activate#(X) take#(s(X),cons(Y,L)) = L + X + Y + 0 >= Y + 0 = activate#(Y) eq(n__0(),n__0()) = 8 >= 0 = true() eq(n__s(X),n__s(Y)) = 8 >= 8 = eq(activate(X),activate(Y)) eq(X,Y) = 8 >= 4 = false() inf(X) = X + 0 >= X = cons(X,n__inf(n__s(X))) take(0(),X) = X + 1 >= 0 = nil() take(s(X),cons(Y,L)) = L + X + Y + 0 >= L + X + Y + 0 = cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) = 1 >= 1 = 0() length(cons(X,L)) = 1L + 1X + 1 >= 1L + 1 = s(n__length(activate(L))) 0() = 1 >= 1 = n__0() s(X) = X + 0 >= X = n__s(X) inf(X) = X + 0 >= X = n__inf(X) take(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__take(X1,X2) length(X) = 1X + 1 >= 1X + 1 = n__length(X) activate(n__0()) = 1 >= 1 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(X) activate(n__inf(X)) = X + 0 >= X + 0 = inf(activate(X)) activate(n__take(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = take(activate(X1),activate(X2)) activate(n__length(X)) = 1X + 1 >= 1X + 1 = length(activate(X)) activate(X) = X + 0 >= X = X problem: DPs: length#(cons(X,L)) -> activate#(L) activate#(n__inf(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X SCC Processor: #sccs: 1 #rules: 7 #arcs: 52/64 DPs: activate#(n__inf(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> activate#(X1) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [take#](x0, x1) = 4x0 + 4x1 + 5, [activate#](x0) = 4x0 + 0, [n__length](x0) = 7, [length](x0) = 7, [n__take](x0, x1) = 2x0 + x1 + 3, [s](x0) = x0 + 0, [nil] = 2, [take](x0, x1) = 2x0 + x1 + 3, [0] = 0, [cons](x0, x1) = x0 + x1 + 0, [n__inf](x0) = x0 + 0, [inf](x0) = x0 + 0, [false] = 0, [activate](x0) = x0 + 0, [n__s](x0) = x0 + 0, [true] = 5, [eq](x0, x1) = 5x1 + 0, [n__0] = 0 orientation: activate#(n__inf(X)) = 4X + 4 >= 4X + 0 = activate#(X) activate#(n__take(X1,X2)) = 6X1 + 4X2 + 7 >= 4X2 + 0 = activate#(X2) activate#(n__take(X1,X2)) = 6X1 + 4X2 + 7 >= 4X1 + 0 = activate#(X1) activate#(n__take(X1,X2)) = 6X1 + 4X2 + 7 >= 4X1 + 4X2 + 5 = take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) = 4L + 4X + 4Y + 5 >= 4L + 0 = activate#(L) take#(s(X),cons(Y,L)) = 4L + 4X + 4Y + 5 >= 4X + 0 = activate#(X) take#(s(X),cons(Y,L)) = 4L + 4X + 4Y + 5 >= 4Y + 0 = activate#(Y) eq(n__0(),n__0()) = 5 >= 5 = true() eq(n__s(X),n__s(Y)) = 5Y + 5 >= 5Y + 5 = eq(activate(X),activate(Y)) eq(X,Y) = 5Y + 0 >= 0 = false() inf(X) = X + 0 >= X + 0 = cons(X,n__inf(n__s(X))) take(0(),X) = X + 3 >= 2 = nil() take(s(X),cons(Y,L)) = L + 2X + Y + 3 >= L + 2X + Y + 3 = cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) = 7 >= 0 = 0() length(cons(X,L)) = 7 >= 7 = s(n__length(activate(L))) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X + 0 = n__s(X) inf(X) = X + 0 >= X + 0 = n__inf(X) take(X1,X2) = 2X1 + X2 + 3 >= 2X1 + X2 + 3 = n__take(X1,X2) length(X) = 7 >= 7 = n__length(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(X) activate(n__inf(X)) = X + 0 >= X + 0 = inf(activate(X)) activate(n__take(X1,X2)) = 2X1 + X2 + 3 >= 2X1 + X2 + 3 = take(activate(X1),activate(X2)) activate(n__length(X)) = 7 >= 7 = length(activate(X)) activate(X) = X + 0 >= X = X problem: DPs: activate#(n__inf(X)) -> activate#(X) activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [take#](x0, x1) = x0 + x1, [activate#](x0) = x0, [n__length](x0) = x0, [length](x0) = x0, [n__take](x0, x1) = 2x0 + x1, [s](x0) = x0, [nil] = 2, [take](x0, x1) = 2x0 + x1, [0] = 0, [cons](x0, x1) = x0 + x1 + 0, [n__inf](x0) = 6x0 + 0, [inf](x0) = 6x0 + 0, [false] = 0, [activate](x0) = x0, [n__s](x0) = x0, [true] = 0, [eq](x0, x1) = 4x0 + 7x1 + 0, [n__0] = 0 orientation: activate#(n__inf(X)) = 6X + 0 >= X = activate#(X) activate#(n__take(X1,X2)) = 2X1 + X2 >= X2 = activate#(X2) activate#(n__take(X1,X2)) = 2X1 + X2 >= X1 + X2 = take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) = L + X + Y + 0 >= L = activate#(L) take#(s(X),cons(Y,L)) = L + X + Y + 0 >= X = activate#(X) take#(s(X),cons(Y,L)) = L + X + Y + 0 >= Y = activate#(Y) eq(n__0(),n__0()) = 7 >= 0 = true() eq(n__s(X),n__s(Y)) = 4X + 7Y + 0 >= 4X + 7Y + 0 = eq(activate(X),activate(Y)) eq(X,Y) = 4X + 7Y + 0 >= 0 = false() inf(X) = 6X + 0 >= 6X + 0 = cons(X,n__inf(n__s(X))) take(0(),X) = X + 2 >= 2 = nil() take(s(X),cons(Y,L)) = L + 2X + Y + 0 >= L + 2X + Y + 0 = cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) = 2 >= 0 = 0() length(cons(X,L)) = L + X + 0 >= L = s(n__length(activate(L))) 0() = 0 >= 0 = n__0() s(X) = X >= X = n__s(X) inf(X) = 6X + 0 >= 6X + 0 = n__inf(X) take(X1,X2) = 2X1 + X2 >= 2X1 + X2 = n__take(X1,X2) length(X) = X >= X = n__length(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X >= X = s(X) activate(n__inf(X)) = 6X + 0 >= 6X + 0 = inf(activate(X)) activate(n__take(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = take(activate(X1),activate(X2)) activate(n__length(X)) = X >= X = length(activate(X)) activate(X) = X >= X = X problem: DPs: activate#(n__take(X1,X2)) -> activate#(X2) activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [take#](x0, x1) = x0 + x1, [activate#](x0) = x0, [n__length](x0) = x0, [length](x0) = x0, [n__take](x0, x1) = 2x0 + 2x1, [s](x0) = x0, [nil] = 2, [take](x0, x1) = 2x0 + 2x1, [0] = 0, [cons](x0, x1) = x0 + x1, [n__inf](x0) = x0 + 0, [inf](x0) = x0 + 0, [false] = 2, [activate](x0) = x0, [n__s](x0) = x0, [true] = 1, [eq](x0, x1) = x1 + 8, [n__0] = 0 orientation: activate#(n__take(X1,X2)) = 2X1 + 2X2 >= X2 = activate#(X2) activate#(n__take(X1,X2)) = 2X1 + 2X2 >= X1 + X2 = take#(activate(X1),activate(X2)) take#(s(X),cons(Y,L)) = L + X + Y >= L = activate#(L) take#(s(X),cons(Y,L)) = L + X + Y >= X = activate#(X) take#(s(X),cons(Y,L)) = L + X + Y >= Y = activate#(Y) eq(n__0(),n__0()) = 8 >= 1 = true() eq(n__s(X),n__s(Y)) = Y + 8 >= Y + 8 = eq(activate(X),activate(Y)) eq(X,Y) = Y + 8 >= 2 = false() inf(X) = X + 0 >= X + 0 = cons(X,n__inf(n__s(X))) take(0(),X) = 2X + 2 >= 2 = nil() take(s(X),cons(Y,L)) = 2L + 2X + 2Y >= 2L + 2X + Y = cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) = 2 >= 0 = 0() length(cons(X,L)) = L + X >= L = s(n__length(activate(L))) 0() = 0 >= 0 = n__0() s(X) = X >= X = n__s(X) inf(X) = X + 0 >= X + 0 = n__inf(X) take(X1,X2) = 2X1 + 2X2 >= 2X1 + 2X2 = n__take(X1,X2) length(X) = X >= X = n__length(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X >= X = s(X) activate(n__inf(X)) = X + 0 >= X + 0 = inf(activate(X)) activate(n__take(X1,X2)) = 2X1 + 2X2 >= 2X1 + 2X2 = take(activate(X1),activate(X2)) activate(n__length(X)) = X >= X = length(activate(X)) activate(X) = X >= X = X problem: DPs: take#(s(X),cons(Y,L)) -> activate#(L) take#(s(X),cons(Y,L)) -> activate#(X) take#(s(X),cons(Y,L)) -> activate#(Y) TRS: eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) eq(X,Y) -> false() inf(X) -> cons(X,n__inf(n__s(X))) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) length(nil()) -> 0() length(cons(X,L)) -> s(n__length(activate(L))) 0() -> n__0() s(X) -> n__s(X) inf(X) -> n__inf(X) take(X1,X2) -> n__take(X1,X2) length(X) -> n__length(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__inf(X)) -> inf(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__length(X)) -> length(activate(X)) activate(X) -> X SCC Processor: #sccs: 0 #rules: 0 #arcs: 27/9