* Step 1: Sum WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
loop(Cons(x,xs),Nil(),pp,ss) -> False()
loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
loop(Nil(),s,pp,ss) -> True()
match1(p,s) -> loop(p,s,p,s)
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
- Signature:
{!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,loop,loop[Ite],match1} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
loop(Cons(x,xs),Nil(),pp,ss) -> False()
loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
loop(Nil(),s,pp,ss) -> True()
match1(p,s) -> loop(p,s,p,s)
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
- Signature:
{!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,loop,loop[Ite],match1} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(loop[Ite]) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(!EQ) = [1]
p(0) = [0]
p(Cons) = [1]
p(False) = [1]
p(Nil) = [0]
p(S) = [0]
p(True) = [0]
p(loop) = [1]
p(loop[Ite]) = [1] x1 + [2] x2 + [2] x3 + [4]
p(match1) = [1]
Following rules are strictly oriented:
loop(Nil(),s,pp,ss) = [1]
> [0]
= True()
Following rules are (at-least) weakly oriented:
!EQ(0(),0()) = [1]
>= [0]
= True()
!EQ(0(),S(y)) = [1]
>= [1]
= False()
!EQ(S(x),0()) = [1]
>= [1]
= False()
!EQ(S(x),S(y)) = [1]
>= [1]
= !EQ(x,y)
loop(Cons(x,xs),Nil(),pp,ss) = [1]
>= [1]
= False()
loop(Cons(x',xs'),Cons(x,xs),pp,ss) = [1]
>= [9]
= loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
loop[Ite](False(),p,s,pp,Cons(x,xs)) = [2] p + [2] s + [5]
>= [1]
= loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = [8]
>= [1]
= loop(xs',xs,pp,ss)
match1(p,s) = [1]
>= [1]
= loop(p,s,p,s)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
loop(Cons(x,xs),Nil(),pp,ss) -> False()
loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
match1(p,s) -> loop(p,s,p,s)
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
loop(Nil(),s,pp,ss) -> True()
loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
- Signature:
{!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,loop,loop[Ite],match1} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(loop[Ite]) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(!EQ) = [2]
p(0) = [0]
p(Cons) = [2]
p(False) = [1]
p(Nil) = [0]
p(S) = [1] x1 + [0]
p(True) = [2]
p(loop) = [2]
p(loop[Ite]) = [1] x1 + [1] x2 + [5] x3 + [1]
p(match1) = [5]
Following rules are strictly oriented:
loop(Cons(x,xs),Nil(),pp,ss) = [2]
> [1]
= False()
match1(p,s) = [5]
> [2]
= loop(p,s,p,s)
Following rules are (at-least) weakly oriented:
!EQ(0(),0()) = [2]
>= [2]
= True()
!EQ(0(),S(y)) = [2]
>= [1]
= False()
!EQ(S(x),0()) = [2]
>= [1]
= False()
!EQ(S(x),S(y)) = [2]
>= [2]
= !EQ(x,y)
loop(Cons(x',xs'),Cons(x,xs),pp,ss) = [2]
>= [15]
= loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
loop(Nil(),s,pp,ss) = [2]
>= [2]
= True()
loop[Ite](False(),p,s,pp,Cons(x,xs)) = [1] p + [5] s + [2]
>= [2]
= loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = [15]
>= [2]
= loop(xs',xs,pp,ss)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
loop(Cons(x,xs),Nil(),pp,ss) -> False()
loop(Nil(),s,pp,ss) -> True()
loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
match1(p,s) -> loop(p,s,p,s)
- Signature:
{!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,loop,loop[Ite],match1} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(loop[Ite]) = {1}
Following symbols are considered usable:
{!EQ,loop,loop[Ite],match1}
TcT has computed the following interpretation:
p(!EQ) = 0
p(0) = 0
p(Cons) = 1 + x2
p(False) = 0
p(Nil) = 0
p(S) = 1
p(True) = 0
p(loop) = 1 + x1 + 3*x2 + x3 + x3*x4 + 2*x4^2
p(loop[Ite]) = 2*x1 + x2 + 3*x3 + x4 + x4*x5 + 2*x5^2
p(match1) = 2 + 3*x1 + 2*x1*x2 + x1^2 + 3*x2 + 2*x2^2
Following rules are strictly oriented:
loop(Cons(x',xs'),Cons(x,xs),pp,ss) = 5 + pp + pp*ss + 2*ss^2 + 3*xs + xs'
> 4 + pp + pp*ss + 2*ss^2 + 3*xs + xs'
= loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
Following rules are (at-least) weakly oriented:
!EQ(0(),0()) = 0
>= 0
= True()
!EQ(0(),S(y)) = 0
>= 0
= False()
!EQ(S(x),0()) = 0
>= 0
= False()
!EQ(S(x),S(y)) = 0
>= 0
= !EQ(x,y)
loop(Cons(x,xs),Nil(),pp,ss) = 2 + pp + pp*ss + 2*ss^2 + xs
>= 0
= False()
loop(Nil(),s,pp,ss) = 1 + pp + pp*ss + 3*s + 2*ss^2
>= 0
= True()
loop[Ite](False(),p,s,pp,Cons(x,xs)) = 2 + p + 2*pp + pp*xs + 3*s + 4*xs + 2*xs^2
>= 1 + 2*pp + pp*xs + 3*xs + 2*xs^2
= loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = 4 + pp + pp*ss + 2*ss^2 + 3*xs + xs'
>= 1 + pp + pp*ss + 2*ss^2 + 3*xs + xs'
= loop(xs',xs,pp,ss)
match1(p,s) = 2 + 3*p + 2*p*s + p^2 + 3*s + 2*s^2
>= 1 + 2*p + p*s + 3*s + 2*s^2
= loop(p,s,p,s)
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
loop(Cons(x,xs),Nil(),pp,ss) -> False()
loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
loop(Nil(),s,pp,ss) -> True()
loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
match1(p,s) -> loop(p,s,p,s)
- Signature:
{!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ,loop,loop[Ite],match1} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))