WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c16() ACTIVATE(n__from(z0)) -> c14(FROM(z0)) ACTIVATE(n__zWquot(z0,z1)) -> c15(ZWQUOT(z0,z1)) FROM(z0) -> c() FROM(z0) -> c1() MINUS(z0,0()) -> c4() MINUS(s(z0),s(z1)) -> c5(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c6() QUOT(s(z0),s(z1)) -> c7(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) SEL(0(),cons(z0,z1)) -> c2() SEL(s(z0),cons(z1,z2)) -> c3(SEL(z0,activate(z2)),ACTIVATE(z2)) ZWQUOT(z0,z1) -> c13() ZWQUOT(z0,nil()) -> c8() ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c10(QUOT(z0,z2)) ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c11(ACTIVATE(z1)) ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c12(ACTIVATE(z3)) ZWQUOT(nil(),z0) -> c9() - Weak TRS: activate(z0) -> z0 activate(n__from(z0)) -> from(z0) activate(n__zWquot(z0,z1)) -> zWquot(z0,z1) from(z0) -> cons(z0,n__from(s(z0))) from(z0) -> n__from(z0) minus(z0,0()) -> 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))) sel(0(),cons(z0,z1)) -> z0 sel(s(z0),cons(z1,z2)) -> sel(z0,activate(z2)) zWquot(z0,z1) -> n__zWquot(z0,z1) zWquot(z0,nil()) -> nil() zWquot(cons(z0,z1),cons(z2,z3)) -> cons(quot(z0,z2),n__zWquot(activate(z1),activate(z3))) zWquot(nil(),z0) -> nil() - Signature: {ACTIVATE/1,FROM/1,MINUS/2,QUOT/2,SEL/2,ZWQUOT/2,activate/1,from/1,minus/2,quot/2,sel/2,zWquot/2} / {0/0,c/0 ,c1/0,c10/1,c11/1,c12/1,c13/0,c14/1,c15/1,c16/0,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/0,cons/2,n__from/1 ,n__zWquot/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,FROM,MINUS,QUOT,SEL,ZWQUOT,activate,from,minus ,quot,sel,zWquot} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__from ,n__zWquot,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c16() ACTIVATE(n__from(z0)) -> c14(FROM(z0)) ACTIVATE(n__zWquot(z0,z1)) -> c15(ZWQUOT(z0,z1)) FROM(z0) -> c() FROM(z0) -> c1() MINUS(z0,0()) -> c4() MINUS(s(z0),s(z1)) -> c5(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c6() QUOT(s(z0),s(z1)) -> c7(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) SEL(0(),cons(z0,z1)) -> c2() SEL(s(z0),cons(z1,z2)) -> c3(SEL(z0,activate(z2)),ACTIVATE(z2)) ZWQUOT(z0,z1) -> c13() ZWQUOT(z0,nil()) -> c8() ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c10(QUOT(z0,z2)) ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c11(ACTIVATE(z1)) ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c12(ACTIVATE(z3)) ZWQUOT(nil(),z0) -> c9() - Weak TRS: activate(z0) -> z0 activate(n__from(z0)) -> from(z0) activate(n__zWquot(z0,z1)) -> zWquot(z0,z1) from(z0) -> cons(z0,n__from(s(z0))) from(z0) -> n__from(z0) minus(z0,0()) -> 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))) sel(0(),cons(z0,z1)) -> z0 sel(s(z0),cons(z1,z2)) -> sel(z0,activate(z2)) zWquot(z0,z1) -> n__zWquot(z0,z1) zWquot(z0,nil()) -> nil() zWquot(cons(z0,z1),cons(z2,z3)) -> cons(quot(z0,z2),n__zWquot(activate(z1),activate(z3))) zWquot(nil(),z0) -> nil() - Signature: {ACTIVATE/1,FROM/1,MINUS/2,QUOT/2,SEL/2,ZWQUOT/2,activate/1,from/1,minus/2,quot/2,sel/2,zWquot/2} / {0/0,c/0 ,c1/0,c10/1,c11/1,c12/1,c13/0,c14/1,c15/1,c16/0,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/0,cons/2,n__from/1 ,n__zWquot/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,FROM,MINUS,QUOT,SEL,ZWQUOT,activate,from,minus ,quot,sel,zWquot} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__from ,n__zWquot,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c16() ACTIVATE(n__from(z0)) -> c14(FROM(z0)) ACTIVATE(n__zWquot(z0,z1)) -> c15(ZWQUOT(z0,z1)) FROM(z0) -> c() FROM(z0) -> c1() MINUS(z0,0()) -> c4() MINUS(s(z0),s(z1)) -> c5(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c6() QUOT(s(z0),s(z1)) -> c7(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) SEL(0(),cons(z0,z1)) -> c2() SEL(s(z0),cons(z1,z2)) -> c3(SEL(z0,activate(z2)),ACTIVATE(z2)) ZWQUOT(z0,z1) -> c13() ZWQUOT(z0,nil()) -> c8() ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c10(QUOT(z0,z2)) ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c11(ACTIVATE(z1)) ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c12(ACTIVATE(z3)) ZWQUOT(nil(),z0) -> c9() - Weak TRS: activate(z0) -> z0 activate(n__from(z0)) -> from(z0) activate(n__zWquot(z0,z1)) -> zWquot(z0,z1) from(z0) -> cons(z0,n__from(s(z0))) from(z0) -> n__from(z0) minus(z0,0()) -> 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))) sel(0(),cons(z0,z1)) -> z0 sel(s(z0),cons(z1,z2)) -> sel(z0,activate(z2)) zWquot(z0,z1) -> n__zWquot(z0,z1) zWquot(z0,nil()) -> nil() zWquot(cons(z0,z1),cons(z2,z3)) -> cons(quot(z0,z2),n__zWquot(activate(z1),activate(z3))) zWquot(nil(),z0) -> nil() - Signature: {ACTIVATE/1,FROM/1,MINUS/2,QUOT/2,SEL/2,ZWQUOT/2,activate/1,from/1,minus/2,quot/2,sel/2,zWquot/2} / {0/0,c/0 ,c1/0,c10/1,c11/1,c12/1,c13/0,c14/1,c15/1,c16/0,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/0,cons/2,n__from/1 ,n__zWquot/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,FROM,MINUS,QUOT,SEL,ZWQUOT,activate,from,minus ,quot,sel,zWquot} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__from ,n__zWquot,nil,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MINUS(x,y){x -> s(x),y -> s(y)} = MINUS(s(x),s(y)) ->^+ c5(MINUS(x,y)) = C[MINUS(x,y) = MINUS(x,y){}] WORST_CASE(Omega(n^1),?)