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