* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
duplicate(Nil()) -> Nil()
goal(x) -> duplicate(x)
- Signature:
{duplicate/1,goal/1} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {duplicate,goal} and constructors {Cons,Nil}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
duplicate(Nil()) -> Nil()
goal(x) -> duplicate(x)
- Signature:
{duplicate/1,goal/1} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {duplicate,goal} and constructors {Cons,Nil}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
duplicate(y){y -> Cons(x,y)} =
duplicate(Cons(x,y)) ->^+ Cons(x,Cons(x,duplicate(y)))
= C[duplicate(y) = duplicate(y){}]
** Step 1.b:1: MI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
duplicate(Nil()) -> Nil()
goal(x) -> duplicate(x)
- Signature:
{duplicate/1,goal/1} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {duplicate,goal} and constructors {Cons,Nil}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(Cons) = {2}
Following symbols are considered usable:
{duplicate,goal}
TcT has computed the following interpretation:
p(Cons) = [1] x_2 + [0]
p(Nil) = [0]
p(duplicate) = [0]
p(goal) = [8]
Following rules are strictly oriented:
goal(x) = [8]
> [0]
= duplicate(x)
Following rules are (at-least) weakly oriented:
duplicate(Cons(x,xs)) = [0]
>= [0]
= Cons(x,Cons(x,duplicate(xs)))
duplicate(Nil()) = [0]
>= [0]
= Nil()
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
duplicate(Nil()) -> Nil()
- Weak TRS:
goal(x) -> duplicate(x)
- Signature:
{duplicate/1,goal/1} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {duplicate,goal} and constructors {Cons,Nil}
+ 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(Cons) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [0]
p(Nil) = [0]
p(duplicate) = [5]
p(goal) = [5]
Following rules are strictly oriented:
duplicate(Nil()) = [5]
> [0]
= Nil()
Following rules are (at-least) weakly oriented:
duplicate(Cons(x,xs)) = [5]
>= [5]
= Cons(x,Cons(x,duplicate(xs)))
goal(x) = [5]
>= [5]
= duplicate(x)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
- Weak TRS:
duplicate(Nil()) -> Nil()
goal(x) -> duplicate(x)
- Signature:
{duplicate/1,goal/1} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {duplicate,goal} and constructors {Cons,Nil}
+ 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(Cons) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [1]
p(Nil) = [10]
p(duplicate) = [3] x1 + [0]
p(goal) = [9] x1 + [0]
Following rules are strictly oriented:
duplicate(Cons(x,xs)) = [3] xs + [3]
> [3] xs + [2]
= Cons(x,Cons(x,duplicate(xs)))
Following rules are (at-least) weakly oriented:
duplicate(Nil()) = [30]
>= [10]
= Nil()
goal(x) = [9] x + [0]
>= [3] x + [0]
= duplicate(x)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
duplicate(Nil()) -> Nil()
goal(x) -> duplicate(x)
- Signature:
{duplicate/1,goal/1} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {duplicate,goal} and constructors {Cons,Nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))