WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: IF(false(),z0,z1,z2) -> c15(IF2(z0,z1,z2)) IF(true(),z0,z1,z2) -> c14() IF2(false(),z0,z1) -> c17(LOG2(quot(z0,s(s(0()))),z1),QUOT(z0,s(s(0())))) IF2(true(),z0,s(z1)) -> c16() INC(0()) -> c3() INC(s(z0)) -> c4(INC(z0)) LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) LOG(z0) -> c10(LOG2(z0,0())) LOG2(z0,z1) -> c11(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),LE(z0,0())) LOG2(z0,z1) -> c12(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),LE(z0,s(0()))) LOG2(z0,z1) -> c13(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),INC(z1)) MINUS(z0,0()) -> c6() MINUS(0(),z0) -> c5() MINUS(s(z0),s(z1)) -> c7(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c8() QUOT(s(z0),s(z1)) -> c9(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) - Weak TRS: if(false(),z0,z1,z2) -> if2(z0,z1,z2) if(true(),z0,z1,z2) -> log_undefined() if2(false(),z0,z1) -> log2(quot(z0,s(s(0()))),z1) if2(true(),z0,s(z1)) -> z1 inc(0()) -> 0() inc(s(z0)) -> s(inc(z0)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) log(z0) -> log2(z0,0()) log2(z0,z1) -> if(le(z0,0()),le(z0,s(0())),z0,inc(z1)) minus(z0,0()) -> z0 minus(0(),z0) -> 0() minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) - Signature: {IF/4,IF2/3,INC/1,LE/2,LOG/1,LOG2/2,MINUS/2,QUOT/2,if/4,if2/3,inc/1,le/2,log/1,log2/2,minus/2,quot/2} / {0/0 ,c/0,c1/0,c10/1,c11/2,c12/2,c13/2,c14/0,c15/1,c16/0,c17/2,c2/1,c3/0,c4/1,c5/0,c6/0,c7/1,c8/0,c9/2,false/0 ,log_undefined/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {IF,IF2,INC,LE,LOG,LOG2,MINUS,QUOT,if,if2,inc,le,log,log2 ,minus,quot} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,false ,log_undefined,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: IF(false(),z0,z1,z2) -> c15(IF2(z0,z1,z2)) IF(true(),z0,z1,z2) -> c14() IF2(false(),z0,z1) -> c17(LOG2(quot(z0,s(s(0()))),z1),QUOT(z0,s(s(0())))) IF2(true(),z0,s(z1)) -> c16() INC(0()) -> c3() INC(s(z0)) -> c4(INC(z0)) LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) LOG(z0) -> c10(LOG2(z0,0())) LOG2(z0,z1) -> c11(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),LE(z0,0())) LOG2(z0,z1) -> c12(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),LE(z0,s(0()))) LOG2(z0,z1) -> c13(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),INC(z1)) MINUS(z0,0()) -> c6() MINUS(0(),z0) -> c5() MINUS(s(z0),s(z1)) -> c7(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c8() QUOT(s(z0),s(z1)) -> c9(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) - Weak TRS: if(false(),z0,z1,z2) -> if2(z0,z1,z2) if(true(),z0,z1,z2) -> log_undefined() if2(false(),z0,z1) -> log2(quot(z0,s(s(0()))),z1) if2(true(),z0,s(z1)) -> z1 inc(0()) -> 0() inc(s(z0)) -> s(inc(z0)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) log(z0) -> log2(z0,0()) log2(z0,z1) -> if(le(z0,0()),le(z0,s(0())),z0,inc(z1)) minus(z0,0()) -> z0 minus(0(),z0) -> 0() minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) - Signature: {IF/4,IF2/3,INC/1,LE/2,LOG/1,LOG2/2,MINUS/2,QUOT/2,if/4,if2/3,inc/1,le/2,log/1,log2/2,minus/2,quot/2} / {0/0 ,c/0,c1/0,c10/1,c11/2,c12/2,c13/2,c14/0,c15/1,c16/0,c17/2,c2/1,c3/0,c4/1,c5/0,c6/0,c7/1,c8/0,c9/2,false/0 ,log_undefined/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {IF,IF2,INC,LE,LOG,LOG2,MINUS,QUOT,if,if2,inc,le,log,log2 ,minus,quot} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,false ,log_undefined,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: IF(false(),z0,z1,z2) -> c15(IF2(z0,z1,z2)) IF(true(),z0,z1,z2) -> c14() IF2(false(),z0,z1) -> c17(LOG2(quot(z0,s(s(0()))),z1),QUOT(z0,s(s(0())))) IF2(true(),z0,s(z1)) -> c16() INC(0()) -> c3() INC(s(z0)) -> c4(INC(z0)) LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) LOG(z0) -> c10(LOG2(z0,0())) LOG2(z0,z1) -> c11(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),LE(z0,0())) LOG2(z0,z1) -> c12(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),LE(z0,s(0()))) LOG2(z0,z1) -> c13(IF(le(z0,0()),le(z0,s(0())),z0,inc(z1)),INC(z1)) MINUS(z0,0()) -> c6() MINUS(0(),z0) -> c5() MINUS(s(z0),s(z1)) -> c7(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c8() QUOT(s(z0),s(z1)) -> c9(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) - Weak TRS: if(false(),z0,z1,z2) -> if2(z0,z1,z2) if(true(),z0,z1,z2) -> log_undefined() if2(false(),z0,z1) -> log2(quot(z0,s(s(0()))),z1) if2(true(),z0,s(z1)) -> z1 inc(0()) -> 0() inc(s(z0)) -> s(inc(z0)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) log(z0) -> log2(z0,0()) log2(z0,z1) -> if(le(z0,0()),le(z0,s(0())),z0,inc(z1)) minus(z0,0()) -> z0 minus(0(),z0) -> 0() minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) - Signature: {IF/4,IF2/3,INC/1,LE/2,LOG/1,LOG2/2,MINUS/2,QUOT/2,if/4,if2/3,inc/1,le/2,log/1,log2/2,minus/2,quot/2} / {0/0 ,c/0,c1/0,c10/1,c11/2,c12/2,c13/2,c14/0,c15/1,c16/0,c17/2,c2/1,c3/0,c4/1,c5/0,c6/0,c7/1,c8/0,c9/2,false/0 ,log_undefined/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {IF,IF2,INC,LE,LOG,LOG2,MINUS,QUOT,if,if2,inc,le,log,log2 ,minus,quot} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,false ,log_undefined,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: INC(x){x -> s(x)} = INC(s(x)) ->^+ c4(INC(x)) = C[INC(x) = INC(x){}] WORST_CASE(Omega(n^1),?)