* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
+Full(x,y){x -> S(x)} =
+Full(S(x),y) ->^+ +Full(x,S(y))
= C[+Full(x,S(y)) = +Full(x,y){y -> S(y)}]
** Step 1.b:1: MI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
+ 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(+) = {2},
uargs(Cons) = {1,2}
Following symbols are considered usable:
{*,+Full,f,goal,map}
TcT has computed the following interpretation:
p(*) = [2] x_1 + [7]
p(+) = [1] x_2 + [0]
p(+Full) = [1] x_1 + [1] x_2 + [4]
p(0) = [4]
p(Cons) = [1] x_1 + [1] x_2 + [8]
p(Nil) = [0]
p(S) = [1] x_1 + [1]
p(f) = [3] x_1 + [10]
p(goal) = [3] x_1 + [2]
p(map) = [3] x_1 + [1]
Following rules are strictly oriented:
+Full(0(),y) = [1] y + [8]
> [1] y + [0]
= y
f(x) = [3] x + [10]
> [2] x + [7]
= *(x,x)
goal(xs) = [3] xs + [2]
> [3] xs + [1]
= map(xs)
map(Cons(x,xs)) = [3] x + [3] xs + [25]
> [3] x + [3] xs + [19]
= Cons(f(x),map(xs))
map(Nil()) = [1]
> [0]
= Nil()
Following rules are (at-least) weakly oriented:
*(x,0()) = [2] x + [7]
>= [4]
= 0()
*(x,S(0())) = [2] x + [7]
>= [1] x + [0]
= x
*(x,S(S(y))) = [2] x + [7]
>= [2] x + [7]
= +(x,*(x,S(y)))
*(0(),y) = [15]
>= [4]
= 0()
+Full(S(x),y) = [1] x + [1] y + [5]
>= [1] x + [1] y + [5]
= +Full(x,S(y))
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
+Full(S(x),y) -> +Full(x,S(y))
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
+Full(0(),y) -> y
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
+ 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(+) = {2},
uargs(Cons) = {1,2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = [8] x1 + [9]
p(+) = [1] x2 + [0]
p(+Full) = [6] x1 + [4] x2 + [1]
p(0) = [2]
p(Cons) = [1] x1 + [1] x2 + [2]
p(Nil) = [0]
p(S) = [1] x1 + [4]
p(f) = [8] x1 + [9]
p(goal) = [10] x1 + [8]
p(map) = [8] x1 + [6]
Following rules are strictly oriented:
+Full(S(x),y) = [6] x + [4] y + [25]
> [6] x + [4] y + [17]
= +Full(x,S(y))
Following rules are (at-least) weakly oriented:
*(x,0()) = [8] x + [9]
>= [2]
= 0()
*(x,S(0())) = [8] x + [9]
>= [1] x + [0]
= x
*(x,S(S(y))) = [8] x + [9]
>= [8] x + [9]
= +(x,*(x,S(y)))
*(0(),y) = [25]
>= [2]
= 0()
+Full(0(),y) = [4] y + [13]
>= [1] y + [0]
= y
f(x) = [8] x + [9]
>= [8] x + [9]
= *(x,x)
goal(xs) = [10] xs + [8]
>= [8] xs + [6]
= map(xs)
map(Cons(x,xs)) = [8] x + [8] xs + [22]
>= [8] x + [8] xs + [17]
= Cons(f(x),map(xs))
map(Nil()) = [6]
>= [0]
= Nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))