WORST_CASE(?,O(n^2))
* Step 1: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
a__add(X1,X2) -> add(X1,X2)
a__add(0(),X) -> mark(X)
a__add(s(X),Y) -> s(add(X,Y))
a__from(X) -> cons(mark(X),from(s(X)))
a__from(X) -> from(X)
a__fst(X1,X2) -> fst(X1,X2)
a__fst(0(),Z) -> nil()
a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
a__len(X) -> len(X)
a__len(cons(X,Z)) -> s(len(Z))
a__len(nil()) -> 0()
mark(0()) -> 0()
mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(from(X)) -> a__from(mark(X))
mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
mark(len(X)) -> a__len(mark(X))
mark(nil()) -> nil()
mark(s(X)) -> s(X)
- Signature:
{a__add/2,a__from/1,a__fst/2,a__len/1,mark/1} / {0/0,add/2,cons/2,from/1,fst/2,len/1,nil/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__add,a__from,a__fst,a__len,mark} and constructors {0
,add,cons,from,fst,len,nil,s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> A(6, 3)
0 :: [] -(0)-> A(9, 3)
0 :: [] -(0)-> A(13, 5)
a__add :: [A(6, 3) x A(9, 3)] -(7)-> A(6, 3)
a__from :: [A(9, 3)] -(8)-> A(6, 3)
a__fst :: [A(6, 3) x A(9, 3)] -(7)-> A(6, 3)
a__len :: [A(6, 3)] -(7)-> A(6, 3)
add :: [A(9, 3) x A(12, 3)] -(9)-> A(9, 3)
add :: [A(6, 3) x A(9, 3)] -(6)-> A(6, 3)
add :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0)
cons :: [A(9, 3) x A(0, 0)] -(9)-> A(9, 3)
cons :: [A(6, 3) x A(0, 0)] -(6)-> A(6, 3)
from :: [A(12, 3)] -(9)-> A(9, 3)
from :: [A(0, 0)] -(0)-> A(0, 0)
from :: [A(9, 3)] -(6)-> A(6, 3)
fst :: [A(9, 3) x A(12, 3)] -(9)-> A(9, 3)
fst :: [A(6, 3) x A(9, 3)] -(6)-> A(6, 3)
fst :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0)
len :: [A(9, 3)] -(9)-> A(9, 3)
len :: [A(6, 3)] -(6)-> A(6, 3)
len :: [A(0, 0)] -(0)-> A(0, 0)
mark :: [A(9, 3)] -(1)-> A(6, 3)
nil :: [] -(0)-> A(6, 3)
nil :: [] -(0)-> A(9, 3)
nil :: [] -(0)-> A(13, 5)
s :: [A(0, 0)] -(3)-> A(6, 3)
s :: [A(0, 0)] -(3)-> A(9, 3)
s :: [A(0, 0)] -(4)-> A(12, 4)
s :: [A(0, 0)] -(0)-> A(0, 0)
s :: [A(0, 0)] -(9)-> A(10, 9)
s :: [A(0, 0)] -(3)-> A(10, 3)
Cost-free Signatures used:
--------------------------
0 :: [] -(0)-> A_cf(0, 0)
0 :: [] -(0)-> A_cf(3, 0)
0 :: [] -(0)-> A_cf(3, 2)
a__add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
a__add :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0)
a__from :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
a__from :: [A_cf(3, 0)] -(3)-> A_cf(3, 0)
a__fst :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
a__fst :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0)
a__len :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
a__len :: [A_cf(3, 0)] -(3)-> A_cf(3, 0)
add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
add :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0)
cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
cons :: [A_cf(3, 0) x A_cf(0, 0)] -(3)-> A_cf(3, 0)
from :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
from :: [A_cf(3, 0)] -(3)-> A_cf(3, 0)
fst :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
fst :: [A_cf(3, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0)
len :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
len :: [A_cf(3, 0)] -(3)-> A_cf(3, 0)
mark :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
mark :: [A_cf(3, 0)] -(0)-> A_cf(3, 0)
nil :: [] -(0)-> A_cf(0, 0)
nil :: [] -(0)-> A_cf(3, 0)
nil :: [] -(0)-> A_cf(3, 2)
s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
s :: [A_cf(0, 0)] -(0)-> A_cf(3, 0)
s :: [A_cf(0, 0)] -(2)-> A_cf(11, 2)
s :: [A_cf(0, 0)] -(6)-> A_cf(4, 6)
s :: [A_cf(0, 0)] -(0)-> A_cf(14, 0)
s :: [A_cf(0, 0)] -(2)-> A_cf(10, 2)
s :: [A_cf(0, 0)] -(1)-> A_cf(8, 1)
s :: [A_cf(0, 0)] -(3)-> A_cf(12, 3)
s :: [A_cf(0, 0)] -(0)-> A_cf(8, 0)
s :: [A_cf(0, 0)] -(5)-> A_cf(4, 5)
s :: [A_cf(0, 0)] -(0)-> A_cf(5, 0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1, 0)
0_A :: [] -(0)-> A(0, 1)
add_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0)
add_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1)
cons_A :: [A(1, 0) x A(0, 0)] -(1)-> A(1, 0)
cons_A :: [A(0, 1) x A(0, 0)] -(0)-> A(0, 1)
from_A :: [A(1, 0)] -(1)-> A(1, 0)
from_A :: [A(1, 1)] -(0)-> A(0, 1)
fst_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0)
fst_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1)
len_A :: [A(1, 0)] -(1)-> A(1, 0)
len_A :: [A(0, 1)] -(0)-> A(0, 1)
nil_A :: [] -(0)-> A(1, 0)
nil_A :: [] -(0)-> A(0, 1)
s_A :: [A(0, 0)] -(0)-> A(1, 0)
s_A :: [A(0, 0)] -(1)-> A(0, 1)
* Step 2: Open MAYBE
- Strict TRS:
a__add(X1,X2) -> add(X1,X2)
a__add(0(),X) -> mark(X)
a__add(s(X),Y) -> s(add(X,Y))
a__from(X) -> cons(mark(X),from(s(X)))
a__from(X) -> from(X)
a__fst(X1,X2) -> fst(X1,X2)
a__fst(0(),Z) -> nil()
a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
a__len(X) -> len(X)
a__len(cons(X,Z)) -> s(len(Z))
a__len(nil()) -> 0()
mark(0()) -> 0()
mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(from(X)) -> a__from(mark(X))
mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
mark(len(X)) -> a__len(mark(X))
mark(nil()) -> nil()
mark(s(X)) -> s(X)
- Signature:
{a__add/2,a__from/1,a__fst/2,a__len/1,mark/1} / {0/0,add/2,cons/2,from/1,fst/2,len/1,nil/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__add,a__from,a__fst,a__len,mark} and constructors {0
,add,cons,from,fst,len,nil,s}
Following problems could not be solved:
- Strict TRS:
a__add(X1,X2) -> add(X1,X2)
a__add(0(),X) -> mark(X)
a__add(s(X),Y) -> s(add(X,Y))
a__from(X) -> cons(mark(X),from(s(X)))
a__from(X) -> from(X)
a__fst(X1,X2) -> fst(X1,X2)
a__fst(0(),Z) -> nil()
a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
a__len(X) -> len(X)
a__len(cons(X,Z)) -> s(len(Z))
a__len(nil()) -> 0()
mark(0()) -> 0()
mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(from(X)) -> a__from(mark(X))
mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
mark(len(X)) -> a__len(mark(X))
mark(nil()) -> nil()
mark(s(X)) -> s(X)
- Signature:
{a__add/2,a__from/1,a__fst/2,a__len/1,mark/1} / {0/0,add/2,cons/2,from/1,fst/2,len/1,nil/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__add,a__from,a__fst,a__len,mark} and constructors {0
,add,cons,from,fst,len,nil,s}
WORST_CASE(?,O(n^2))