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