* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
*(x,0()) -> 0()
*(0(),x) -> 0()
*(I(x),y) -> +(O(*(x,y)),y)
*(O(x),y) -> O(*(x,y))
+(x,0()) -> x
+(0(),x) -> x
+(I(x),I(y)) -> O(+(+(x,y),I(0())))
+(I(x),O(y)) -> I(+(x,y))
+(O(x),I(y)) -> I(+(x,y))
+(O(x),O(y)) -> O(+(x,y))
O(0()) -> 0()
- Signature:
{*/2,+/2,O/1} / {0/0,I/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+,O} and constructors {0,I}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
*(x,0()) -> 0()
*(0(),x) -> 0()
*(I(x),y) -> +(O(*(x,y)),y)
*(O(x),y) -> O(*(x,y))
+(x,0()) -> x
+(0(),x) -> x
+(I(x),I(y)) -> O(+(+(x,y),I(0())))
+(I(x),O(y)) -> I(+(x,y))
+(O(x),I(y)) -> I(+(x,y))
+(O(x),O(y)) -> O(+(x,y))
O(0()) -> 0()
- Signature:
{*/2,+/2,O/1} / {0/0,I/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+,O} and constructors {0,I}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
*(x,y){x -> I(x)} =
*(I(x),y) ->^+ +(O(*(x,y)),y)
= C[*(x,y) = *(x,y){}]
WORST_CASE(Omega(n^1),?)