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))