* 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),?)