* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
gcd(0(),N) -> 0()
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
lt(N,M) -> gt(M,N)
p(s(N)) -> N
quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
quot(NzM,NzM) -> u_01(is_NzNat(NzM))
u_01(True()) -> s(0())
u_02(True(),NzM) -> NzM
u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
u_2(True()) -> 0()
u_21(True(),NzM,N) -> u_2(gt(NzM,N))
u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1} / {0/0,False/0,True/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+,d,gcd,gt,is_NzNat,lt,p,quot,u_01,u_02,u_1,u_11,u_2
,u_21,u_3,u_31,u_4} and constructors {0,False,True,s}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
gcd(0(),N) -> 0()
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
lt(N,M) -> gt(M,N)
p(s(N)) -> N
quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
quot(NzM,NzM) -> u_01(is_NzNat(NzM))
u_01(True()) -> s(0())
u_02(True(),NzM) -> NzM
u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
u_2(True()) -> 0()
u_21(True(),NzM,N) -> u_2(gt(NzM,N))
u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1} / {0/0,False/0,True/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+,d,gcd,gt,is_NzNat,lt,p,quot,u_01,u_02,u_1,u_11,u_2
,u_21,u_3,u_31,u_4} and constructors {0,False,True,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)) ->^+ s(+(x,+(y,*(x,y))))
= C[*(x,y) = *(x,y){}]
WORST_CASE(Omega(n^1),?)