* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
goal(xs,ys) -> revapp(xs,ys)
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
- Signature:
{goal/2,revapp/2} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,revapp} 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:
goal(xs,ys) -> revapp(xs,ys)
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
- Signature:
{goal/2,revapp/2} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,revapp} and constructors {Cons,Nil}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
revapp(y,z){y -> Cons(x,y)} =
revapp(Cons(x,y),z) ->^+ revapp(y,Cons(x,z))
= C[revapp(y,Cons(x,z)) = revapp(y,z){z -> Cons(x,z)}]
** Step 1.b:1: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
goal(xs,ys) -> revapp(xs,ys)
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
- Signature:
{goal/2,revapp/2} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,revapp} 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:
none
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [0]
p(Nil) = [0]
p(goal) = [3] x2 + [0]
p(revapp) = [3] x2 + [11]
Following rules are strictly oriented:
revapp(Nil(),rest) = [3] rest + [11]
> [1] rest + [0]
= rest
Following rules are (at-least) weakly oriented:
goal(xs,ys) = [3] ys + [0]
>= [3] ys + [11]
= revapp(xs,ys)
revapp(Cons(x,xs),rest) = [3] rest + [11]
>= [3] rest + [11]
= revapp(xs,Cons(x,rest))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
goal(xs,ys) -> revapp(xs,ys)
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
- Weak TRS:
revapp(Nil(),rest) -> rest
- Signature:
{goal/2,revapp/2} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,revapp} 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:
none
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [5]
p(Nil) = [0]
p(goal) = [4] x1 + [2] x2 + [0]
p(revapp) = [4] x1 + [2] x2 + [0]
Following rules are strictly oriented:
revapp(Cons(x,xs),rest) = [2] rest + [4] xs + [20]
> [2] rest + [4] xs + [10]
= revapp(xs,Cons(x,rest))
Following rules are (at-least) weakly oriented:
goal(xs,ys) = [4] xs + [2] ys + [0]
>= [4] xs + [2] ys + [0]
= revapp(xs,ys)
revapp(Nil(),rest) = [2] rest + [0]
>= [1] rest + [0]
= rest
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:
goal(xs,ys) -> revapp(xs,ys)
- Weak TRS:
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
- Signature:
{goal/2,revapp/2} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,revapp} 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:
none
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [0]
p(Nil) = [0]
p(goal) = [3] x2 + [1]
p(revapp) = [3] x2 + [0]
Following rules are strictly oriented:
goal(xs,ys) = [3] ys + [1]
> [3] ys + [0]
= revapp(xs,ys)
Following rules are (at-least) weakly oriented:
revapp(Cons(x,xs),rest) = [3] rest + [0]
>= [3] rest + [0]
= revapp(xs,Cons(x,rest))
revapp(Nil(),rest) = [3] rest + [0]
>= [1] rest + [0]
= rest
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:
goal(xs,ys) -> revapp(xs,ys)
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
- Signature:
{goal/2,revapp/2} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,revapp} 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))