WORST_CASE(?,O(n^1))
* Step 1: InnermostRuleRemoval WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
2nd(cons(X,XS)) -> head(activate(XS))
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
head(cons(X,XS)) -> X
s(X) -> n__s(X)
sel(0(),cons(X,XS)) -> X
sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
take(X1,X2) -> n__take(X1,X2)
take(0(),XS) -> nil()
take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
- Signature:
{2nd/1,activate/1,from/1,head/1,s/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__s/1,n__take/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,s,sel,take} and constructors {0
,cons,n__from,n__s,n__take,nil}
+ Applied Processor:
InnermostRuleRemoval
+ Details:
Arguments of following rules are not normal-forms.
sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
All above mentioned rules can be savely removed.
* Step 2: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
2nd(cons(X,XS)) -> head(activate(XS))
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
head(cons(X,XS)) -> X
s(X) -> n__s(X)
sel(0(),cons(X,XS)) -> X
take(X1,X2) -> n__take(X1,X2)
take(0(),XS) -> nil()
- Signature:
{2nd/1,activate/1,from/1,head/1,s/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__s/1,n__take/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,s,sel,take} and constructors {0
,cons,n__from,n__s,n__take,nil}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> A(0)
2nd :: [A(31)] -(23)-> A(0)
activate :: [A(29)] -(1)-> A(0)
cons :: [A(0) x A(31)] -(31)-> A(31)
cons :: [A(0) x A(0)] -(0)-> A(0)
from :: [A(0)] -(0)-> A(0)
head :: [A(0)] -(16)-> A(0)
n__from :: [A(29)] -(29)-> A(29)
n__from :: [A(0)] -(0)-> A(0)
n__s :: [A(29)] -(29)-> A(29)
n__s :: [A(0)] -(0)-> A(0)
n__take :: [A(29) x A(29)] -(29)-> A(29)
n__take :: [A(0) x A(0)] -(0)-> A(0)
nil :: [] -(0)-> A(14)
s :: [A(0)] -(2)-> A(0)
sel :: [A(0) x A(0)] -(23)-> A(0)
take :: [A(0) x A(0)] -(16)-> A(0)
Cost-free Signatures used:
--------------------------
0 :: [] -(0)-> A_cf(0)
activate :: [A_cf(0)] -(0)-> A_cf(0)
cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
from :: [A_cf(0)] -(0)-> A_cf(0)
n__from :: [A_cf(0)] -(0)-> A_cf(0)
n__s :: [A_cf(0)] -(0)-> A_cf(0)
n__take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
nil :: [] -(0)-> A_cf(0)
s :: [A_cf(0)] -(0)-> A_cf(0)
take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1)
cons_A :: [A(0) x A(1)] -(1)-> A(1)
n__from_A :: [A(0)] -(1)-> A(1)
n__s_A :: [A(0)] -(1)-> A(1)
n__take_A :: [A(0) x A(0)] -(1)-> A(1)
nil_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
head(cons(X,XS)) -> X
s(X) -> n__s(X)
take(0(),XS) -> nil()
2. Weak:
2nd(cons(X,XS)) -> head(activate(XS))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
sel(0(),cons(X,XS)) -> X
take(X1,X2) -> n__take(X1,X2)
* Step 3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
2nd(cons(X,XS)) -> head(activate(XS))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
sel(0(),cons(X,XS)) -> X
take(X1,X2) -> n__take(X1,X2)
- Weak TRS:
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
head(cons(X,XS)) -> X
s(X) -> n__s(X)
take(0(),XS) -> nil()
- Signature:
{2nd/1,activate/1,from/1,head/1,s/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__s/1,n__take/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,s,sel,take} and constructors {0
,cons,n__from,n__s,n__take,nil}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> A(0)
2nd :: [A(15)] -(3)-> A(0)
activate :: [A(13)] -(1)-> A(0)
cons :: [A(0) x A(15)] -(15)-> A(15)
cons :: [A(0) x A(1)] -(1)-> A(1)
cons :: [A(0) x A(0)] -(0)-> A(0)
from :: [A(0)] -(8)-> A(0)
head :: [A(0)] -(1)-> A(0)
n__from :: [A(13)] -(13)-> A(13)
n__from :: [A(0)] -(0)-> A(0)
n__s :: [A(13)] -(0)-> A(13)
n__s :: [A(0)] -(0)-> A(0)
n__take :: [A(13) x A(13)] -(13)-> A(13)
n__take :: [A(0) x A(0)] -(0)-> A(0)
nil :: [] -(0)-> A(6)
s :: [A(0)] -(0)-> A(0)
sel :: [A(0) x A(1)] -(11)-> A(0)
take :: [A(0) x A(0)] -(0)-> A(0)
Cost-free Signatures used:
--------------------------
0 :: [] -(0)-> A_cf(0)
activate :: [A_cf(0)] -(0)-> A_cf(0)
cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
from :: [A_cf(0)] -(0)-> A_cf(0)
n__from :: [A_cf(0)] -(0)-> A_cf(0)
n__s :: [A_cf(0)] -(0)-> A_cf(0)
n__take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
nil :: [] -(0)-> A_cf(0)
s :: [A_cf(0)] -(0)-> A_cf(0)
take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1)
cons_A :: [A(0) x A(1)] -(1)-> A(1)
n__from_A :: [A(0)] -(1)-> A(1)
n__s_A :: [A(0)] -(0)-> A(1)
n__take_A :: [A(0) x A(0)] -(1)-> A(1)
nil_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
2nd(cons(X,XS)) -> head(activate(XS))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
2. Weak:
sel(0(),cons(X,XS)) -> X
take(X1,X2) -> n__take(X1,X2)
* Step 4: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
sel(0(),cons(X,XS)) -> X
take(X1,X2) -> n__take(X1,X2)
- Weak TRS:
2nd(cons(X,XS)) -> head(activate(XS))
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
head(cons(X,XS)) -> X
s(X) -> n__s(X)
take(0(),XS) -> nil()
- Signature:
{2nd/1,activate/1,from/1,head/1,s/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__s/1,n__take/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,s,sel,take} and constructors {0
,cons,n__from,n__s,n__take,nil}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> A(0)
2nd :: [A(15)] -(10)-> A(0)
activate :: [A(11)] -(2)-> A(0)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons :: [A(15) x A(15)] -(15)-> A(15)
from :: [A(0)] -(9)-> A(0)
head :: [A(0)] -(0)-> A(0)
n__from :: [A(11)] -(11)-> A(11)
n__from :: [A(0)] -(0)-> A(0)
n__s :: [A(11)] -(11)-> A(11)
n__s :: [A(0)] -(0)-> A(0)
n__take :: [A(11) x A(11)] -(11)-> A(11)
n__take :: [A(0) x A(0)] -(0)-> A(0)
nil :: [] -(0)-> A(6)
s :: [A(0)] -(1)-> A(0)
sel :: [A(0) x A(0)] -(11)-> A(0)
take :: [A(0) x A(0)] -(2)-> A(0)
Cost-free Signatures used:
--------------------------
0 :: [] -(0)-> A_cf(0)
activate :: [A_cf(0)] -(0)-> A_cf(0)
cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
from :: [A_cf(0)] -(0)-> A_cf(0)
n__from :: [A_cf(0)] -(0)-> A_cf(0)
n__s :: [A_cf(0)] -(0)-> A_cf(0)
n__take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
nil :: [] -(0)-> A_cf(0)
s :: [A_cf(0)] -(0)-> A_cf(0)
take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1)
cons_A :: [A(1) x A(1)] -(1)-> A(1)
n__from_A :: [A(0)] -(1)-> A(1)
n__s_A :: [A(0)] -(1)-> A(1)
n__take_A :: [A(0) x A(0)] -(1)-> A(1)
nil_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
take(X1,X2) -> n__take(X1,X2)
2. Weak:
sel(0(),cons(X,XS)) -> X
* Step 5: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
sel(0(),cons(X,XS)) -> X
- Weak TRS:
2nd(cons(X,XS)) -> head(activate(XS))
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
head(cons(X,XS)) -> X
s(X) -> n__s(X)
take(X1,X2) -> n__take(X1,X2)
take(0(),XS) -> nil()
- Signature:
{2nd/1,activate/1,from/1,head/1,s/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__s/1,n__take/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,s,sel,take} and constructors {0
,cons,n__from,n__s,n__take,nil}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> A(0)
2nd :: [A(15)] -(13)-> A(0)
activate :: [A(15)] -(9)-> A(0)
cons :: [A(0) x A(1)] -(1)-> A(1)
cons :: [A(0) x A(15)] -(15)-> A(15)
cons :: [A(0) x A(0)] -(0)-> A(0)
from :: [A(0)] -(12)-> A(0)
head :: [A(0)] -(7)-> A(0)
n__from :: [A(15)] -(15)-> A(15)
n__from :: [A(0)] -(0)-> A(0)
n__s :: [A(15)] -(15)-> A(15)
n__s :: [A(0)] -(0)-> A(0)
n__take :: [A(15) x A(15)] -(15)-> A(15)
n__take :: [A(0) x A(0)] -(0)-> A(0)
nil :: [] -(0)-> A(6)
s :: [A(0)] -(2)-> A(0)
sel :: [A(0) x A(1)] -(11)-> A(0)
take :: [A(0) x A(0)] -(3)-> A(0)
Cost-free Signatures used:
--------------------------
0 :: [] -(0)-> A_cf(0)
activate :: [A_cf(0)] -(0)-> A_cf(0)
cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
from :: [A_cf(0)] -(0)-> A_cf(0)
n__from :: [A_cf(0)] -(0)-> A_cf(0)
n__s :: [A_cf(0)] -(0)-> A_cf(0)
n__take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
nil :: [] -(0)-> A_cf(0)
s :: [A_cf(0)] -(0)-> A_cf(0)
take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1)
cons_A :: [A(0) x A(1)] -(1)-> A(1)
n__from_A :: [A(0)] -(1)-> A(1)
n__s_A :: [A(0)] -(1)-> A(1)
n__take_A :: [A(0) x A(0)] -(1)-> A(1)
nil_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
sel(0(),cons(X,XS)) -> X
2. Weak:
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
2nd(cons(X,XS)) -> head(activate(XS))
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
head(cons(X,XS)) -> X
s(X) -> n__s(X)
sel(0(),cons(X,XS)) -> X
take(X1,X2) -> n__take(X1,X2)
take(0(),XS) -> nil()
- Signature:
{2nd/1,activate/1,from/1,head/1,s/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__s/1,n__take/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,s,sel,take} and constructors {0
,cons,n__from,n__s,n__take,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))