WORST_CASE(?,O(n^1))
* Step 1: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs))
anyEq(nr,NilNat()) -> False()
lookup(nr,Leaf(xs)) -> anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt)
- Weak TRS:
eq(0(),0()) -> True()
eq(0(),S(m)) -> False()
eq(S(n),0()) -> False()
eq(S(n),S(m)) -> eq(n,m)
ite(False(),t,e) -> e
ite(True(),t,e) -> t
leq(0(),0()) -> True()
leq(0(),S(m)) -> True()
leq(S(n),0()) -> False()
leq(S(n),S(m)) -> leq(n,m)
- Signature:
{anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2
,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree
,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(ite) = {1,2,3}
Following symbols are considered usable:
{anyEq,eq,ite,leq,lookup}
TcT has computed the following interpretation:
p(0) = 1
p(ConsBTree) = x1 + x2
p(ConsNat) = x2
p(False) = 0
p(Leaf) = 0
p(NilBTree) = 1
p(NilNat) = 0
p(Node) = x1 + x2
p(S) = 2
p(True) = 0
p(anyEq) = 0
p(eq) = 0
p(ite) = 4*x1 + x2 + x3
p(leq) = 0
p(lookup) = 2*x2
Following rules are strictly oriented:
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = 2 + 2*tGt
> 2*tGt
= lookup(nr,tGt)
Following rules are (at-least) weakly oriented:
anyEq(nr,ConsNat(x,xs)) = 0
>= 0
= ite(eq(nr,x),True(),anyEq(nr,xs))
anyEq(nr,NilNat()) = 0
>= 0
= False()
eq(0(),0()) = 0
>= 0
= True()
eq(0(),S(m)) = 0
>= 0
= False()
eq(S(n),0()) = 0
>= 0
= False()
eq(S(n),S(m)) = 0
>= 0
= eq(n,m)
ite(False(),t,e) = e + t
>= e
= e
ite(True(),t,e) = e + t
>= t
= t
leq(0(),0()) = 0
>= 0
= True()
leq(0(),S(m)) = 0
>= 0
= True()
leq(S(n),0()) = 0
>= 0
= False()
leq(S(n),S(m)) = 0
>= 0
= leq(n,m)
lookup(nr,Leaf(xs)) = 0
>= 0
= anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = 2*nrs + 2*t + 2*ts
>= 2*nrs + 2*t + 2*ts
= ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
* Step 2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs))
anyEq(nr,NilNat()) -> False()
lookup(nr,Leaf(xs)) -> anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
- Weak TRS:
eq(0(),0()) -> True()
eq(0(),S(m)) -> False()
eq(S(n),0()) -> False()
eq(S(n),S(m)) -> eq(n,m)
ite(False(),t,e) -> e
ite(True(),t,e) -> t
leq(0(),0()) -> True()
leq(0(),S(m)) -> True()
leq(S(n),0()) -> False()
leq(S(n),S(m)) -> leq(n,m)
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt)
- Signature:
{anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2
,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree
,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(ite) = {1,2,3}
Following symbols are considered usable:
{anyEq,eq,ite,leq,lookup}
TcT has computed the following interpretation:
p(0) = 0
p(ConsBTree) = 7 + x1 + x2
p(ConsNat) = 1 + x2
p(False) = 0
p(Leaf) = 0
p(NilBTree) = 2
p(NilNat) = 0
p(Node) = x1 + x2
p(S) = 0
p(True) = 0
p(anyEq) = 0
p(eq) = 0
p(ite) = 4*x1 + x2 + x3
p(leq) = 0
p(lookup) = 4 + x2
Following rules are strictly oriented:
lookup(nr,Leaf(xs)) = 4
> 0
= anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = 12 + nrs + t + ts
> 8 + nrs + t + ts
= ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
Following rules are (at-least) weakly oriented:
anyEq(nr,ConsNat(x,xs)) = 0
>= 0
= ite(eq(nr,x),True(),anyEq(nr,xs))
anyEq(nr,NilNat()) = 0
>= 0
= False()
eq(0(),0()) = 0
>= 0
= True()
eq(0(),S(m)) = 0
>= 0
= False()
eq(S(n),0()) = 0
>= 0
= False()
eq(S(n),S(m)) = 0
>= 0
= eq(n,m)
ite(False(),t,e) = e + t
>= e
= e
ite(True(),t,e) = e + t
>= t
= t
leq(0(),0()) = 0
>= 0
= True()
leq(0(),S(m)) = 0
>= 0
= True()
leq(S(n),0()) = 0
>= 0
= False()
leq(S(n),S(m)) = 0
>= 0
= leq(n,m)
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = 13 + tGt
>= 4 + tGt
= lookup(nr,tGt)
* Step 3: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs))
anyEq(nr,NilNat()) -> False()
- Weak TRS:
eq(0(),0()) -> True()
eq(0(),S(m)) -> False()
eq(S(n),0()) -> False()
eq(S(n),S(m)) -> eq(n,m)
ite(False(),t,e) -> e
ite(True(),t,e) -> t
leq(0(),0()) -> True()
leq(0(),S(m)) -> True()
leq(S(n),0()) -> False()
leq(S(n),S(m)) -> leq(n,m)
lookup(nr,Leaf(xs)) -> anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt)
- Signature:
{anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2
,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree
,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(ite) = {1,2,3}
Following symbols are considered usable:
{anyEq,eq,ite,leq,lookup}
TcT has computed the following interpretation:
p(0) = [6]
p(ConsBTree) = [1] x1 + [1] x2 + [2]
p(ConsNat) = [1] x1 + [1] x2 + [0]
p(False) = [0]
p(Leaf) = [0]
p(NilBTree) = [0]
p(NilNat) = [0]
p(Node) = [1] x1 + [1] x2 + [0]
p(S) = [1] x1 + [5]
p(True) = [0]
p(anyEq) = [1]
p(eq) = [0]
p(ite) = [2] x1 + [1] x2 + [1] x3 + [0]
p(leq) = [1] x2 + [3]
p(lookup) = [8] x2 + [1]
Following rules are strictly oriented:
anyEq(nr,NilNat()) = [1]
> [0]
= False()
Following rules are (at-least) weakly oriented:
anyEq(nr,ConsNat(x,xs)) = [1]
>= [1]
= ite(eq(nr,x),True(),anyEq(nr,xs))
eq(0(),0()) = [0]
>= [0]
= True()
eq(0(),S(m)) = [0]
>= [0]
= False()
eq(S(n),0()) = [0]
>= [0]
= False()
eq(S(n),S(m)) = [0]
>= [0]
= eq(n,m)
ite(False(),t,e) = [1] e + [1] t + [0]
>= [1] e + [0]
= e
ite(True(),t,e) = [1] e + [1] t + [0]
>= [1] t + [0]
= t
leq(0(),0()) = [9]
>= [0]
= True()
leq(0(),S(m)) = [1] m + [8]
>= [0]
= True()
leq(S(n),0()) = [9]
>= [0]
= False()
leq(S(n),S(m)) = [1] m + [8]
>= [1] m + [3]
= leq(n,m)
lookup(nr,Leaf(xs)) = [1]
>= [1]
= anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = [8] nrs + [8] t + [8] ts + [8] up + [17]
>= [8] nrs + [8] t + [8] ts + [2] up + [8]
= ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = [8] tGt + [17]
>= [8] tGt + [1]
= lookup(nr,tGt)
* Step 4: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs))
- Weak TRS:
anyEq(nr,NilNat()) -> False()
eq(0(),0()) -> True()
eq(0(),S(m)) -> False()
eq(S(n),0()) -> False()
eq(S(n),S(m)) -> eq(n,m)
ite(False(),t,e) -> e
ite(True(),t,e) -> t
leq(0(),0()) -> True()
leq(0(),S(m)) -> True()
leq(S(n),0()) -> False()
leq(S(n),S(m)) -> leq(n,m)
lookup(nr,Leaf(xs)) -> anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt)
- Signature:
{anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2
,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree
,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(ite) = {1,2,3}
Following symbols are considered usable:
{anyEq,eq,ite,leq,lookup}
TcT has computed the following interpretation:
p(0) = 4
p(ConsBTree) = 4 + x1 + x2
p(ConsNat) = 4 + x1 + x2
p(False) = 0
p(Leaf) = 4 + x1
p(NilBTree) = 0
p(NilNat) = 2
p(Node) = x2
p(S) = x1
p(True) = 1
p(anyEq) = 4 + 2*x2
p(eq) = x2
p(ite) = 4 + x1 + x2 + x3
p(leq) = 2
p(lookup) = 2*x2
Following rules are strictly oriented:
anyEq(nr,ConsNat(x,xs)) = 12 + 2*x + 2*xs
> 9 + x + 2*xs
= ite(eq(nr,x),True(),anyEq(nr,xs))
Following rules are (at-least) weakly oriented:
anyEq(nr,NilNat()) = 8
>= 0
= False()
eq(0(),0()) = 4
>= 1
= True()
eq(0(),S(m)) = m
>= 0
= False()
eq(S(n),0()) = 4
>= 0
= False()
eq(S(n),S(m)) = m
>= m
= eq(n,m)
ite(False(),t,e) = 4 + e + t
>= e
= e
ite(True(),t,e) = 5 + e + t
>= t
= t
leq(0(),0()) = 2
>= 1
= True()
leq(0(),S(m)) = 2
>= 1
= True()
leq(S(n),0()) = 2
>= 0
= False()
leq(S(n),S(m)) = 2
>= 2
= leq(n,m)
lookup(nr,Leaf(xs)) = 8 + 2*xs
>= 4 + 2*xs
= anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) = 8 + 2*t + 2*ts
>= 6 + 2*t + 2*ts
= ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) = 8 + 2*tGt
>= 2*tGt
= lookup(nr,tGt)
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
anyEq(nr,ConsNat(x,xs)) -> ite(eq(nr,x),True(),anyEq(nr,xs))
anyEq(nr,NilNat()) -> False()
eq(0(),0()) -> True()
eq(0(),S(m)) -> False()
eq(S(n),0()) -> False()
eq(S(n),S(m)) -> eq(n,m)
ite(False(),t,e) -> e
ite(True(),t,e) -> t
leq(0(),0()) -> True()
leq(0(),S(m)) -> True()
leq(S(n),0()) -> False()
leq(S(n),S(m)) -> leq(n,m)
lookup(nr,Leaf(xs)) -> anyEq(nr,xs)
lookup(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) -> ite(leq(nr,up),lookup(nr,t),lookup(nr,Node(nrs,ts)))
lookup(nr,Node(NilNat(),ConsBTree(tGt,NilBTree()))) -> lookup(nr,tGt)
- Signature:
{anyEq/2,eq/2,ite/3,leq/2,lookup/2} / {0/0,ConsBTree/2,ConsNat/2,False/0,Leaf/1,NilBTree/0,NilNat/0,Node/2
,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {anyEq,eq,ite,leq,lookup} and constructors {0,ConsBTree
,ConsNat,False,Leaf,NilBTree,NilNat,Node,S,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))