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