WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
a__b() -> a()
a__b() -> b()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__f(a(),X,X) -> a__f(X,a__b(),b())
mark(a()) -> a()
mark(b()) -> a__b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
a__b() -> a()
a__b() -> b()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__f(a(),X,X) -> a__f(X,a__b(),b())
mark(a()) -> a()
mark(b()) -> a__b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
mark(y){y -> f(x,y,z)} =
mark(f(x,y,z)) ->^+ a__f(x,mark(y),z)
= C[mark(y) = mark(y){}]
** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__b() -> a()
a__b() -> b()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__f(a(),X,X) -> a__f(X,a__b(),b())
mark(a()) -> a()
mark(b()) -> a__b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {2}
Following symbols are considered usable:
{a__b,a__f,mark}
TcT has computed the following interpretation:
p(a) = 0
p(a__b) = 0
p(a__f) = 2 + x2
p(b) = 0
p(f) = 2 + x2
p(mark) = 1 + x1
Following rules are strictly oriented:
mark(a()) = 1
> 0
= a()
mark(b()) = 1
> 0
= a__b()
Following rules are (at-least) weakly oriented:
a__b() = 0
>= 0
= a()
a__b() = 0
>= 0
= b()
a__f(X1,X2,X3) = 2 + X2
>= 2 + X2
= f(X1,X2,X3)
a__f(a(),X,X) = 2 + X
>= 2
= a__f(X,a__b(),b())
mark(f(X1,X2,X3)) = 3 + X2
>= 3 + X2
= a__f(X1,mark(X2),X3)
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__b() -> a()
a__b() -> b()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__f(a(),X,X) -> a__f(X,a__b(),b())
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Weak TRS:
mark(a()) -> a()
mark(b()) -> a__b()
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {2}
Following symbols are considered usable:
{a__b,a__f,mark}
TcT has computed the following interpretation:
p(a) = 0
p(a__b) = 0
p(a__f) = 4 + x2
p(b) = 0
p(f) = 2 + x2
p(mark) = 8 + 8*x1
Following rules are strictly oriented:
a__f(X1,X2,X3) = 4 + X2
> 2 + X2
= f(X1,X2,X3)
mark(f(X1,X2,X3)) = 24 + 8*X2
> 12 + 8*X2
= a__f(X1,mark(X2),X3)
Following rules are (at-least) weakly oriented:
a__b() = 0
>= 0
= a()
a__b() = 0
>= 0
= b()
a__f(a(),X,X) = 4 + X
>= 4
= a__f(X,a__b(),b())
mark(a()) = 8
>= 0
= a()
mark(b()) = 8
>= 0
= a__b()
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__b() -> a()
a__b() -> b()
a__f(a(),X,X) -> a__f(X,a__b(),b())
- Weak TRS:
a__f(X1,X2,X3) -> f(X1,X2,X3)
mark(a()) -> a()
mark(b()) -> a__b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {2}
Following symbols are considered usable:
{a__b,a__f,mark}
TcT has computed the following interpretation:
p(a) = 2
p(a__b) = 4
p(a__f) = 10 + 4*x1 + x2 + 4*x3
p(b) = 1
p(f) = 2 + x1 + x2 + x3
p(mark) = 9 + 8*x1
Following rules are strictly oriented:
a__b() = 4
> 2
= a()
a__b() = 4
> 1
= b()
Following rules are (at-least) weakly oriented:
a__f(X1,X2,X3) = 10 + 4*X1 + X2 + 4*X3
>= 2 + X1 + X2 + X3
= f(X1,X2,X3)
a__f(a(),X,X) = 18 + 5*X
>= 18 + 4*X
= a__f(X,a__b(),b())
mark(a()) = 25
>= 2
= a()
mark(b()) = 17
>= 4
= a__b()
mark(f(X1,X2,X3)) = 25 + 8*X1 + 8*X2 + 8*X3
>= 19 + 4*X1 + 8*X2 + 4*X3
= a__f(X1,mark(X2),X3)
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__f(a(),X,X) -> a__f(X,a__b(),b())
- Weak TRS:
a__b() -> a()
a__b() -> b()
a__f(X1,X2,X3) -> f(X1,X2,X3)
mark(a()) -> a()
mark(b()) -> a__b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {2}
Following symbols are considered usable:
{a__b,a__f,mark}
TcT has computed the following interpretation:
p(a) = 2
p(a__b) = 9
p(a__f) = 8*x1 + x2 + 8*x3
p(b) = 0
p(f) = x1 + x2 + x3
p(mark) = 10 + 9*x1
Following rules are strictly oriented:
a__f(a(),X,X) = 16 + 9*X
> 9 + 8*X
= a__f(X,a__b(),b())
Following rules are (at-least) weakly oriented:
a__b() = 9
>= 2
= a()
a__b() = 9
>= 0
= b()
a__f(X1,X2,X3) = 8*X1 + X2 + 8*X3
>= X1 + X2 + X3
= f(X1,X2,X3)
mark(a()) = 28
>= 2
= a()
mark(b()) = 10
>= 9
= a__b()
mark(f(X1,X2,X3)) = 10 + 9*X1 + 9*X2 + 9*X3
>= 10 + 8*X1 + 9*X2 + 8*X3
= a__f(X1,mark(X2),X3)
** Step 1.b:5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
a__b() -> a()
a__b() -> b()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__f(a(),X,X) -> a__f(X,a__b(),b())
mark(a()) -> a()
mark(b()) -> a__b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
- Signature:
{a__b/0,a__f/3,mark/1} / {a/0,b/0,f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__b,a__f,mark} and constructors {a,b,f}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))