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) = 6 + x1 + x2 p(select) = 3*x1^2 p(selects) = 2 + 2*x1*x2 + 5*x1*x3 + 4*x2*x3 + 3*x3^2 Following rules are strictly oriented: revapp(Nil(),rest) = 8 + rest > rest = rest select(Cons(x,xs)) = 12 + 12*x + 6*x*xs + 3*x^2 + 12*xs + 3*xs^2 > 2 + 4*x + 5*x*xs + 8*xs + 3*xs^2 = selects(x,Nil(),xs) select(Nil()) = 12 > 2 = Nil() Following rules are (at-least) weakly oriented: revapp(Cons(x,xs),rest) = 8 + rest + x + xs >= 8 + rest + x + xs = revapp(xs,Cons(x,rest)) selects(x,revprefix,Nil()) = 14 + 8*revprefix + 2*revprefix*x + 10*x >= 14 + revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) = 14 + 8*revprefix + 4*revprefix*x + 2*revprefix*x' + 4*revprefix*xs + 12*x + 5*x*x' + 6*x*xs + 3*x^2 + 10*x' + 5*x'*xs + 12*xs + 3*xs^2 >= 14 + revprefix + 2*revprefix*x + 4*revprefix*xs + 5*x + 2*x*x' + 5*x*xs + x' + 4*x'*xs + 9*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: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) 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(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) = 0 p(revapp) = 4*x1 + 4*x2 p(select) = 2*x1 + 6*x1^2 p(selects) = 4 + x1 + 5*x1*x3 + 4*x2 + 4*x2*x3 + 6*x3 + 4*x3^2 Following rules are strictly oriented: selects(x,revprefix,Nil()) = 4 + 4*revprefix + x > 2 + 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*rest >= rest = rest select(Cons(x,xs)) = 8 + 14*x + 12*x*xs + 6*x^2 + 14*xs + 6*xs^2 >= 4 + x + 5*x*xs + 6*xs + 4*xs^2 = selects(x,Nil(),xs) select(Nil()) = 0 >= 0 = Nil() selects(x',revprefix,Cons(x,xs)) = 14 + 8*revprefix + 4*revprefix*x + 4*revprefix*xs + 14*x + 5*x*x' + 8*x*xs + 4*x^2 + 6*x' + 5*x'*xs + 14*xs + 4*xs^2 >= 14 + 8*revprefix + 4*revprefix*xs + 5*x + 5*x*xs + 5*x' + 4*x'*xs + 14*xs + 4*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: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) - Weak TRS: 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) = 2 + x1 + x2 p(Nil) = 2 p(revapp) = 4 + 4*x1 + 2*x2 p(select) = 3*x1^2 p(selects) = 2 + 2*x1 + 3*x1*x2 + 4*x1*x3 + 4*x2*x3 + 3*x3^2 Following rules are strictly oriented: revapp(Cons(x,xs),rest) = 12 + 2*rest + 4*x + 4*xs > 8 + 2*rest + 2*x + 4*xs = revapp(xs,Cons(x,rest)) Following rules are (at-least) weakly oriented: revapp(Nil(),rest) = 12 + 2*rest >= rest = rest select(Cons(x,xs)) = 12 + 12*x + 6*x*xs + 3*x^2 + 12*xs + 3*xs^2 >= 2 + 8*x + 4*x*xs + 8*xs + 3*xs^2 = selects(x,Nil(),xs) select(Nil()) = 12 >= 2 = Nil() selects(x,revprefix,Nil()) = 14 + 8*revprefix + 3*revprefix*x + 10*x >= 14 + 4*revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) = 14 + 8*revprefix + 4*revprefix*x + 3*revprefix*x' + 4*revprefix*xs + 12*x + 4*x*x' + 6*x*xs + 3*x^2 + 10*x' + 4*x'*xs + 12*xs + 3*xs^2 >= 14 + 4*revprefix + 3*revprefix*x + 4*revprefix*xs + 10*x + 3*x*x' + 4*x*xs + x' + 4*x'*xs + 10*xs + 3*xs^2 = Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs)) * Step 4: 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 + 4*x1 + 4*x2 p(select) = x1 + 7*x1^2 p(selects) = 2 + 2*x1 + 6*x1*x3 + x1^2 + 2*x2 + 4*x2*x3 + 6*x3 + 4*x3^2 Following rules are strictly oriented: selects(x',revprefix,Cons(x,xs)) = 12 + 6*revprefix + 4*revprefix*x + 4*revprefix*xs + 14*x + 6*x*x' + 8*x*xs + 4*x^2 + 8*x' + 6*x'*xs + x'^2 + 14*xs + 4*xs^2 > 11 + 6*revprefix + 4*revprefix*xs + 6*x + 6*x*xs + x^2 + 3*x' + 4*x'*xs + 14*xs + 4*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) = 5 + 4*rest + 4*x + 4*xs >= 5 + 4*rest + 4*x + 4*xs = revapp(xs,Cons(x,rest)) revapp(Nil(),rest) = 5 + 4*rest >= rest = rest select(Cons(x,xs)) = 8 + 15*x + 14*x*xs + 7*x^2 + 15*xs + 7*xs^2 >= 4 + 2*x + 6*x*xs + x^2 + 10*xs + 4*xs^2 = selects(x,Nil(),xs) select(Nil()) = 8 >= 1 = Nil() selects(x,revprefix,Nil()) = 12 + 6*revprefix + 8*x + x^2 >= 8 + 4*revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) * Step 5: 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))