WORST_CASE(?,O(n^1))
* Step 1: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
s(X) -> n__s(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
2nd :: [A(14)] -(14)-> A(0)
activate :: [A(8)] -(5)-> A(0)
cons :: [A(14) x A(14)] -(14)-> A(14)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons1 :: [A(14) x A(0)] -(0)-> A(14)
from :: [A(0)] -(3)-> A(0)
n__from :: [A(8)] -(8)-> A(8)
n__from :: [A(0)] -(0)-> A(0)
n__s :: [A(8)] -(8)-> A(8)
n__s :: [A(0)] -(0)-> A(0)
s :: [A(0)] -(0)-> A(0)
Cost-free Signatures used:
--------------------------
2nd :: [A_cf(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)
cons1 :: [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)
s :: [A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
cons1_A :: [A(1) x A(0)] -(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)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
activate(n__s(X)) -> s(activate(X))
from(X) -> n__from(X)
2. Weak:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
s(X) -> n__s(X)
* Step 2: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
s(X) -> n__s(X)
- Weak TRS:
activate(n__s(X)) -> s(activate(X))
from(X) -> n__from(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
2nd :: [A(13)] -(7)-> A(0)
activate :: [A(0)] -(1)-> A(0)
cons :: [A(13) x A(0)] -(13)-> A(13)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons1 :: [A(0) x A(0)] -(0)-> A(13)
cons1 :: [A(0) x A(0)] -(0)-> A(15)
from :: [A(0)] -(0)-> A(0)
n__from :: [A(0)] -(0)-> A(0)
n__from :: [A(0)] -(0)-> A(9)
n__from :: [A(0)] -(0)-> A(1)
n__s :: [A(0)] -(0)-> A(0)
n__s :: [A(0)] -(0)-> A(5)
n__s :: [A(0)] -(0)-> A(14)
s :: [A(0)] -(0)-> A(13)
Cost-free Signatures used:
--------------------------
2nd :: [A_cf(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)
cons1 :: [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)
s :: [A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
cons1_A :: [A(0) x A(0)] -(0)-> A(1)
cons_A :: [A(1) x A(0)] -(1)-> A(1)
n__from_A :: [A(0)] -(0)-> A(1)
n__s_A :: [A(0)] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
2. Weak:
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
s(X) -> n__s(X)
* Step 3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
s(X) -> n__s(X)
- Weak TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(n__s(X)) -> s(activate(X))
from(X) -> n__from(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
2nd :: [A(15)] -(7)-> A(0)
activate :: [A(15)] -(8)-> A(0)
cons :: [A(0) x A(15)] -(15)-> A(15)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons1 :: [A(0) x A(0)] -(0)-> A(15)
from :: [A(0)] -(15)-> 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)
s :: [A(0)] -(0)-> A(0)
Cost-free Signatures used:
--------------------------
2nd :: [A_cf(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)
cons1 :: [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)
s :: [A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
cons1_A :: [A(0) x A(0)] -(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)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
activate(X) -> X
2. Weak:
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
s(X) -> n__s(X)
* Step 4: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
s(X) -> n__s(X)
- Weak TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__s(X)) -> s(activate(X))
from(X) -> n__from(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
2nd :: [A(15)] -(9)-> A(0)
activate :: [A(11)] -(15)-> A(0)
cons :: [A(0) x A(15)] -(15)-> A(15)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons1 :: [A(0) x A(0)] -(0)-> A(15)
from :: [A(0)] -(11)-> 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)
s :: [A(0)] -(4)-> A(0)
Cost-free Signatures used:
--------------------------
2nd :: [A_cf(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)
cons1 :: [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)
s :: [A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
cons1_A :: [A(0) x A(0)] -(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)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
s(X) -> n__s(X)
2. Weak:
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
* Step 5: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(n__from(X)) -> from(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
- Weak TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__s(X)) -> s(activate(X))
from(X) -> n__from(X)
s(X) -> n__s(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
2nd :: [A(11)] -(13)-> A(0)
activate :: [A(11)] -(2)-> A(0)
cons :: [A(0) x A(11)] -(11)-> A(11)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons1 :: [A(0) x A(0)] -(0)-> A(11)
cons1 :: [A(0) x A(0)] -(0)-> A(13)
from :: [A(0)] -(7)-> 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)
s :: [A(0)] -(1)-> A(0)
Cost-free Signatures used:
--------------------------
2nd :: [A_cf(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)
cons1 :: [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)
s :: [A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
cons1_A :: [A(0) x A(0)] -(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)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
from(X) -> cons(X,n__from(n__s(X)))
2. Weak:
activate(n__from(X)) -> from(activate(X))
* Step 6: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(n__from(X)) -> from(activate(X))
- Weak TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__s(X)) -> s(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
s(X) -> n__s(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
2nd :: [A(15)] -(4)-> A(0)
activate :: [A(15)] -(0)-> A(8)
cons :: [A(0) x A(15)] -(0)-> A(15)
cons :: [A(0) x A(0)] -(0)-> A(0)
cons :: [A(0) x A(8)] -(0)-> A(8)
cons1 :: [A(0) x A(0)] -(0)-> A(15)
from :: [A(8)] -(10)-> A(8)
n__from :: [A(15)] -(15)-> A(15)
n__from :: [A(8)] -(8)-> A(8)
n__s :: [A(15)] -(0)-> A(15)
n__s :: [A(8)] -(0)-> A(8)
s :: [A(8)] -(0)-> A(8)
Cost-free Signatures used:
--------------------------
2nd :: [A_cf(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)
cons1 :: [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)
s :: [A_cf(0)] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
cons1_A :: [A(0) x A(0)] -(0)-> A(1)
cons_A :: [A(0) x A(1)] -(0)-> A(1)
n__from_A :: [A(0)] -(1)-> A(1)
n__s_A :: [A(0)] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
activate(n__from(X)) -> from(activate(X))
2. Weak:
* Step 7: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
2nd(cons1(X,cons(Y,Z))) -> Y
activate(X) -> X
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
s(X) -> n__s(X)
- Signature:
{2nd/1,activate/1,from/1,s/1} / {cons/2,cons1/2,n__from/1,n__s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2nd,activate,from,s} and constructors {cons,cons1,n__from
,n__s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))