WORST_CASE(?,O(n^2)) * Step 1: Ara 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: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "revapp") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "select") :: ["A"(0)] -(2)-> "A"(0) F (TrsFun "selects") :: ["A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: select(Cons(x,xs)) -> selects(x,Nil(),xs) select(Nil()) -> Nil() selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil()) 2. Weak: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) * Step 2: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) revapp(Nil(),rest) -> rest selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) - Weak TRS: 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: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Cons") :: ["A"(15) x "A"(15)] -(15)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(7) F (TrsFun "revapp") :: ["A"(0) x "A"(0)] -(15)-> "A"(0) F (TrsFun "select") :: ["A"(15)] -(12)-> "A"(0) F (TrsFun "selects") :: ["A"(8) x "A"(0) x "A"(15)] -(15)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"Cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: revapp(Nil(),rest) -> rest 2. Weak: 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)) * Step 3: Ara 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: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Cons") :: ["A"(0) x "A"(8)] -(8)-> "A"(8) F (TrsFun "Cons") :: ["A"(0) x "A"(1)] -(1)-> "A"(1) F (TrsFun "Cons") :: ["A"(0) x "A"(4)] -(4)-> "A"(4) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(8) F (TrsFun "Nil") :: [] -(0)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(14) F (TrsFun "Nil") :: [] -(0)-> "A"(6) F (TrsFun "revapp") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "select") :: ["A"(8)] -(6)-> "A"(1) F (TrsFun "selects") :: ["A"(0) x "A"(0) x "A"(8)] -(9)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"Cons\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs))) ,selects(x,Cons(x',revprefix),xs)) 2. Weak: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) * Step 4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest)) - 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()) 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 + 4*x1 + x2 p(select) = 3*x1^2 p(selects) = 3 + 4*x1*x3 + 4*x2*x3 + 3*x3^2 Following rules are strictly oriented: revapp(Cons(x,xs),rest) = 14 + rest + 4*x + 4*xs > 8 + rest + x + 4*xs = revapp(xs,Cons(x,rest)) Following rules are (at-least) weakly oriented: revapp(Nil(),rest) = 14 + rest >= rest = rest select(Cons(x,xs)) = 12 + 12*x + 6*x*xs + 3*x^2 + 12*xs + 3*xs^2 >= 3 + 4*x*xs + 8*xs + 3*xs^2 = selects(x,Nil(),xs) select(Nil()) = 12 >= 2 = Nil() selects(x,revprefix,Nil()) = 15 + 8*revprefix + 8*x >= 14 + 4*revprefix + x = Cons(Cons(x,revapp(revprefix,Nil())),Nil()) selects(x',revprefix,Cons(x,xs)) = 15 + 8*revprefix + 4*revprefix*x + 4*revprefix*xs + 12*x + 4*x*x' + 6*x*xs + 3*x^2 + 8*x' + 4*x'*xs + 12*xs + 3*xs^2 >= 15 + 4*revprefix + 4*revprefix*xs + x + 4*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 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))