WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
half(0()) -> 0()
half(double(x)) -> x
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
if(0(),y,z) -> y
if(s(x),y,z) -> z
- Signature:
{-/2,double/1,half/1,if/3} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
half(0()) -> 0()
half(double(x)) -> x
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
if(0(),y,z) -> y
if(s(x),y,z) -> z
- Signature:
{-/2,double/1,half/1,if/3} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
-(x,y){x -> s(x),y -> s(y)} =
-(s(x),s(y)) ->^+ -(x,y)
= C[-(x,y) = -(x,y){}]
** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
half(0()) -> 0()
half(double(x)) -> x
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
if(0(),y,z) -> y
if(s(x),y,z) -> z
- Signature:
{-/2,double/1,half/1,if/3} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
+ 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(s) = {1}
Following symbols are considered usable:
{-,double,half,if}
TcT has computed the following interpretation:
p(-) = 1 + 8*x1 + 4*x2
p(0) = 4
p(double) = 2*x1
p(half) = x1
p(if) = 5*x1 + 8*x2 + 4*x3
p(s) = 2 + x1
Following rules are strictly oriented:
-(x,0()) = 17 + 8*x
> x
= x
-(s(x),s(y)) = 25 + 8*x + 4*y
> 1 + 8*x + 4*y
= -(x,y)
double(0()) = 8
> 4
= 0()
half(s(0())) = 6
> 4
= 0()
half(s(s(x))) = 4 + x
> 2 + x
= s(half(x))
if(0(),y,z) = 20 + 8*y + 4*z
> y
= y
if(s(x),y,z) = 10 + 5*x + 8*y + 4*z
> z
= z
Following rules are (at-least) weakly oriented:
double(s(x)) = 4 + 2*x
>= 4 + 2*x
= s(s(double(x)))
half(0()) = 4
>= 4
= 0()
half(double(x)) = 2*x
>= x
= x
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
double(s(x)) -> s(s(double(x)))
half(0()) -> 0()
half(double(x)) -> x
- Weak TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
double(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
if(0(),y,z) -> y
if(s(x),y,z) -> z
- Signature:
{-/2,double/1,half/1,if/3} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
+ 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(s) = {1}
Following symbols are considered usable:
{-,double,half,if}
TcT has computed the following interpretation:
p(-) = 1 + 8*x1
p(0) = 0
p(double) = 3*x1
p(half) = 3 + 10*x1
p(if) = 1 + 12*x2 + 8*x3
p(s) = 1 + x1
Following rules are strictly oriented:
double(s(x)) = 3 + 3*x
> 2 + 3*x
= s(s(double(x)))
half(0()) = 3
> 0
= 0()
half(double(x)) = 3 + 30*x
> x
= x
Following rules are (at-least) weakly oriented:
-(x,0()) = 1 + 8*x
>= x
= x
-(s(x),s(y)) = 9 + 8*x
>= 1 + 8*x
= -(x,y)
double(0()) = 0
>= 0
= 0()
half(s(0())) = 13
>= 0
= 0()
half(s(s(x))) = 23 + 10*x
>= 4 + 10*x
= s(half(x))
if(0(),y,z) = 1 + 12*y + 8*z
>= y
= y
if(s(x),y,z) = 1 + 12*y + 8*z
>= z
= z
** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
half(0()) -> 0()
half(double(x)) -> x
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
if(0(),y,z) -> y
if(s(x),y,z) -> z
- Signature:
{-/2,double/1,half/1,if/3} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))