WORST_CASE(?,O(n^2)) * Step 1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest select(Cons(x,xs)) -> selects(x,Nil(),xs) select(Nil()) -> Nil() selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) - Signature: {revapp/2,select/1,selects/3} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(Cons) = {1,2} Following symbols are considered usable: {revapp,select,selects} TcT has computed the following interpretation: p(Cons) = 2 + x1 + x2 p(Nil) = 2 p(revapp) = 2 + 4*x1 + 2*x2 p(select) = 3*x1^2 p(selects) = 5*x1 + 4*x1*x3 + 2*x1^2 + x2 + 4*x2*x3 + 3*x3^2 Following rules are strictly oriented: revapp(Cons(x,xs),rest) = 10 + 2*rest + 4*x + 4*xs > 6 + 2*rest + 2*x + 4*xs = revapp(xs,Cons(x,rest)) revapp(Nil(),rest) = 10 + 2*rest > rest = rest select(Cons(x,xs)) = 12 + 12*x + 6*x*xs + 3*x^2 + 12*xs + 3*xs^2 > 2 + 5*x + 4*x*xs + 2*x^2 + 8*xs + 3*xs^2 = selects(x,Nil(),xs) select(Nil()) = 12 > 2 = Nil() Following rules are (at-least) weakly oriented: selects(x,revprefix,Nil()) = 12 + 9*revprefix + 13*x + 2*x^2 >= 12 + 4*revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) = 12 + 9*revprefix + 4*revprefix*x + 4*revprefix*xs + 12*x + 4*x*x' + 6*x*xs + 3*x^2 + 13*x' + 4*x'*xs + 2*x'^2 + 12*xs + 3*xs^2 >= 12 + 5*revprefix + 4*revprefix*xs + 7*x + 4*x*xs + 2*x^2 + 2*x' + 4*x'*xs + 10*xs + 3*xs^2 = Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs)) * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) - Weak TRS: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest select(Cons(x,xs)) -> selects(x,Nil(),xs) select(Nil()) -> Nil() - Signature: {revapp/2,select/1,selects/3} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(Cons) = {1,2} Following symbols are considered usable: {revapp,select,selects} TcT has computed the following interpretation: p(Cons) = 1 + x1 + x2 p(Nil) = 1 p(revapp) = 4*x1 + 4*x2 p(select) = x1 + 6*x1^2 p(selects) = 3 + 2*x1 + 6*x1*x3 + 5*x1^2 + 4*x2*x3 + 6*x3^2 Following rules are strictly oriented: selects(x,revprefix,Nil()) = 9 + 4*revprefix + 8*x + 5*x^2 > 7 + 4*revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) Following rules are (at-least) weakly oriented: revapp(Cons(x,xs),rest) = 4 + 4*rest + 4*x + 4*xs >= 4 + 4*rest + 4*x + 4*xs = revapp(xs,Cons(x,rest)) revapp(Nil(),rest) = 4 + 4*rest >= rest = rest select(Cons(x,xs)) = 7 + 13*x + 12*x*xs + 6*x^2 + 13*xs + 6*xs^2 >= 3 + 2*x + 6*x*xs + 5*x^2 + 4*xs + 6*xs^2 = selects(x,Nil(),xs) select(Nil()) = 7 >= 1 = Nil() selects(x',revprefix,Cons(x,xs)) = 9 + 4*revprefix + 4*revprefix*x + 4*revprefix*xs + 12*x + 6*x*x' + 12*x*xs + 6*x^2 + 8*x' + 6*x'*xs + 5*x'^2 + 12*xs + 6*xs^2 >= 9 + 4*revprefix + 4*revprefix*xs + 6*x + 6*x*xs + 5*x^2 + x' + 4*x'*xs + 8*xs + 6*xs^2 = Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs)) * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) - Weak TRS: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest select(Cons(x,xs)) -> selects(x,Nil(),xs) select(Nil()) -> Nil() selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil()) - Signature: {revapp/2,select/1,selects/3} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(Cons) = {1,2} Following symbols are considered usable: {revapp,select,selects} TcT has computed the following interpretation: p(Cons) = 1 + x1 + x2 p(Nil) = 1 p(revapp) = 1 + 5*x1 + 2*x2 p(select) = 4 + 6*x1^2 p(selects) = 3 + 6*x1 + 4*x1*x2 + 7*x1*x3 + x1^2 + 7*x2*x3 + x2^2 + 4*x3 + 5*x3^2 Following rules are strictly oriented: selects(x',revprefix,Cons(x,xs)) = 12 + 7*revprefix + 7*revprefix*x + 4*revprefix*x' + 7*revprefix*xs + revprefix^2 + 14*x + 7*x*x' + 10*x*xs + 5*x^2 + 13*x' + 7*x'*xs + x'^2 + 14*xs + 5*xs^2 > 9 + 7*revprefix + 4*revprefix*x + 2*revprefix*x' + 7*revprefix*xs + revprefix^2 + 12*x + 4*x*x' + 7*x*xs + x^2 + 3*x' + 7*x'*xs + x'^2 + 13*xs + 5*xs^2 = Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs)) Following rules are (at-least) weakly oriented: revapp(Cons(x,xs),rest) = 6 + 2*rest + 5*x + 5*xs >= 3 + 2*rest + 2*x + 5*xs = revapp(xs,Cons(x,rest)) revapp(Nil(),rest) = 6 + 2*rest >= rest = rest select(Cons(x,xs)) = 10 + 12*x + 12*x*xs + 6*x^2 + 12*xs + 6*xs^2 >= 4 + 10*x + 7*x*xs + x^2 + 11*xs + 5*xs^2 = selects(x,Nil(),xs) select(Nil()) = 10 >= 1 = Nil() selects(x,revprefix,Nil()) = 12 + 7*revprefix + 4*revprefix*x + revprefix^2 + 13*x + x^2 >= 6 + 5*revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest select(Cons(x,xs)) -> selects(x,Nil(),xs) select(Nil()) -> Nil() selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) - Signature: {revapp/2,select/1,selects/3} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))