WORST_CASE(?,O(n^1))
* Step 1: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
goal(x,xs) -> member(x,xs)
member(x,Nil()) -> False()
member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
member[Ite][True][Ite](True(),x,xs) -> True()
- Signature:
{!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
,notEmpty} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3}
+ Details:
Signatures used:
----------------
!EQ :: [A(0) x A(0)] -(0)-> A(8)
0 :: [] -(0)-> A(0)
Cons :: [A(0) x A(10)] -(10)-> A(10)
Cons :: [A(0) x A(1)] -(1)-> A(1)
False :: [] -(0)-> A(0)
False :: [] -(0)-> A(11)
False :: [] -(0)-> A(14)
Nil :: [] -(0)-> A(10)
Nil :: [] -(0)-> A(1)
S :: [A(0)] -(0)-> A(0)
True :: [] -(0)-> A(0)
True :: [] -(0)-> A(15)
True :: [] -(0)-> A(11)
goal :: [A(15) x A(12)] -(15)-> A(2)
member :: [A(9) x A(10)] -(12)-> A(5)
member[Ite][True][Ite] :: [A(0) x A(9) x A(10)] -(2)-> A(5)
notEmpty :: [A(1)] -(8)-> A(0)
Cost-free Signatures used:
--------------------------
!EQ :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
0 :: [] -(0)-> A_cf(0)
Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
False :: [] -(0)-> A_cf(0)
Nil :: [] -(0)-> A_cf(0)
S :: [A_cf(0)] -(0)-> A_cf(0)
True :: [] -(0)-> A_cf(0)
member :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
member[Ite][True][Ite] :: [A_cf(0) x 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)
False_A :: [] -(0)-> A(1)
Nil_A :: [] -(0)-> A(1)
S_A :: [A(0)] -(0)-> A(1)
True_A :: [] -(0)-> A(1)
* Step 2: Open MAYBE
- Strict TRS:
goal(x,xs) -> member(x,xs)
member(x,Nil()) -> False()
member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
member[Ite][True][Ite](True(),x,xs) -> True()
- Signature:
{!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
,notEmpty} and constructors {0,Cons,False,Nil,S,True}
Following problems could not be solved:
- Strict TRS:
goal(x,xs) -> member(x,xs)
member(x,Nil()) -> False()
member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
member[Ite][True][Ite](True(),x,xs) -> True()
- Signature:
{!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite]
,notEmpty} and constructors {0,Cons,False,Nil,S,True}
WORST_CASE(?,O(n^1))