WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__DIFF(z0,z1) -> c11(A__IF(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) ,A__LEQ(mark(z0),mark(z1)) ,MARK(z0)) A__DIFF(z0,z1) -> c12(A__IF(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) ,A__LEQ(mark(z0),mark(z1)) ,MARK(z1)) A__DIFF(z0,z1) -> c13() A__IF(z0,z1,z2) -> c10() A__IF(false(),z0,z1) -> c9(MARK(z1)) A__IF(true(),z0,z1) -> c8(MARK(z0)) A__LEQ(z0,z1) -> c7() A__LEQ(0(),z0) -> c3() A__LEQ(s(z0),0()) -> c4() A__LEQ(s(z0),s(z1)) -> c5(A__LEQ(mark(z0),mark(z1)),MARK(z0)) A__LEQ(s(z0),s(z1)) -> c6(A__LEQ(mark(z0),mark(z1)),MARK(z1)) A__P(z0) -> c2() A__P(0()) -> c() A__P(s(z0)) -> c1(MARK(z0)) MARK(0()) -> c20() MARK(diff(z0,z1)) -> c18(A__DIFF(mark(z0),mark(z1)),MARK(z0)) MARK(diff(z0,z1)) -> c19(A__DIFF(mark(z0),mark(z1)),MARK(z1)) MARK(false()) -> c23() MARK(if(z0,z1,z2)) -> c17(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(leq(z0,z1)) -> c15(A__LEQ(mark(z0),mark(z1)),MARK(z0)) MARK(leq(z0,z1)) -> c16(A__LEQ(mark(z0),mark(z1)),MARK(z1)) MARK(p(z0)) -> c14(A__P(mark(z0)),MARK(z0)) MARK(s(z0)) -> c21(MARK(z0)) MARK(true()) -> c22() - Weak TRS: a__diff(z0,z1) -> a__if(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) a__diff(z0,z1) -> diff(z0,z1) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__leq(z0,z1) -> leq(z0,z1) a__leq(0(),z0) -> true() a__leq(s(z0),0()) -> false() a__leq(s(z0),s(z1)) -> a__leq(mark(z0),mark(z1)) a__p(z0) -> p(z0) a__p(0()) -> 0() a__p(s(z0)) -> mark(z0) mark(0()) -> 0() mark(diff(z0,z1)) -> a__diff(mark(z0),mark(z1)) mark(false()) -> false() mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(leq(z0,z1)) -> a__leq(mark(z0),mark(z1)) mark(p(z0)) -> a__p(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(true()) -> true() - Signature: {A__DIFF/2,A__IF/3,A__LEQ/2,A__P/1,MARK/1,a__diff/2,a__if/3,a__leq/2,a__p/1,mark/1} / {0/0,c/0,c1/1,c10/0 ,c11/3,c12/3,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/0,c20/0,c21/1,c22/0,c23/0,c3/0,c4/0,c5/2,c6/2,c7/0 ,c8/1,c9/1,diff/2,false/0,if/3,leq/2,p/1,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__DIFF,A__IF,A__LEQ,A__P,MARK,a__diff,a__if,a__leq,a__p ,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8 ,c9,diff,false,if,leq,p,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__DIFF(z0,z1) -> c11(A__IF(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) ,A__LEQ(mark(z0),mark(z1)) ,MARK(z0)) A__DIFF(z0,z1) -> c12(A__IF(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) ,A__LEQ(mark(z0),mark(z1)) ,MARK(z1)) A__DIFF(z0,z1) -> c13() A__IF(z0,z1,z2) -> c10() A__IF(false(),z0,z1) -> c9(MARK(z1)) A__IF(true(),z0,z1) -> c8(MARK(z0)) A__LEQ(z0,z1) -> c7() A__LEQ(0(),z0) -> c3() A__LEQ(s(z0),0()) -> c4() A__LEQ(s(z0),s(z1)) -> c5(A__LEQ(mark(z0),mark(z1)),MARK(z0)) A__LEQ(s(z0),s(z1)) -> c6(A__LEQ(mark(z0),mark(z1)),MARK(z1)) A__P(z0) -> c2() A__P(0()) -> c() A__P(s(z0)) -> c1(MARK(z0)) MARK(0()) -> c20() MARK(diff(z0,z1)) -> c18(A__DIFF(mark(z0),mark(z1)),MARK(z0)) MARK(diff(z0,z1)) -> c19(A__DIFF(mark(z0),mark(z1)),MARK(z1)) MARK(false()) -> c23() MARK(if(z0,z1,z2)) -> c17(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(leq(z0,z1)) -> c15(A__LEQ(mark(z0),mark(z1)),MARK(z0)) MARK(leq(z0,z1)) -> c16(A__LEQ(mark(z0),mark(z1)),MARK(z1)) MARK(p(z0)) -> c14(A__P(mark(z0)),MARK(z0)) MARK(s(z0)) -> c21(MARK(z0)) MARK(true()) -> c22() - Weak TRS: a__diff(z0,z1) -> a__if(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) a__diff(z0,z1) -> diff(z0,z1) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__leq(z0,z1) -> leq(z0,z1) a__leq(0(),z0) -> true() a__leq(s(z0),0()) -> false() a__leq(s(z0),s(z1)) -> a__leq(mark(z0),mark(z1)) a__p(z0) -> p(z0) a__p(0()) -> 0() a__p(s(z0)) -> mark(z0) mark(0()) -> 0() mark(diff(z0,z1)) -> a__diff(mark(z0),mark(z1)) mark(false()) -> false() mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(leq(z0,z1)) -> a__leq(mark(z0),mark(z1)) mark(p(z0)) -> a__p(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(true()) -> true() - Signature: {A__DIFF/2,A__IF/3,A__LEQ/2,A__P/1,MARK/1,a__diff/2,a__if/3,a__leq/2,a__p/1,mark/1} / {0/0,c/0,c1/1,c10/0 ,c11/3,c12/3,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/0,c20/0,c21/1,c22/0,c23/0,c3/0,c4/0,c5/2,c6/2,c7/0 ,c8/1,c9/1,diff/2,false/0,if/3,leq/2,p/1,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__DIFF,A__IF,A__LEQ,A__P,MARK,a__diff,a__if,a__leq,a__p ,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8 ,c9,diff,false,if,leq,p,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__DIFF(z0,z1) -> c11(A__IF(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) ,A__LEQ(mark(z0),mark(z1)) ,MARK(z0)) A__DIFF(z0,z1) -> c12(A__IF(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) ,A__LEQ(mark(z0),mark(z1)) ,MARK(z1)) A__DIFF(z0,z1) -> c13() A__IF(z0,z1,z2) -> c10() A__IF(false(),z0,z1) -> c9(MARK(z1)) A__IF(true(),z0,z1) -> c8(MARK(z0)) A__LEQ(z0,z1) -> c7() A__LEQ(0(),z0) -> c3() A__LEQ(s(z0),0()) -> c4() A__LEQ(s(z0),s(z1)) -> c5(A__LEQ(mark(z0),mark(z1)),MARK(z0)) A__LEQ(s(z0),s(z1)) -> c6(A__LEQ(mark(z0),mark(z1)),MARK(z1)) A__P(z0) -> c2() A__P(0()) -> c() A__P(s(z0)) -> c1(MARK(z0)) MARK(0()) -> c20() MARK(diff(z0,z1)) -> c18(A__DIFF(mark(z0),mark(z1)),MARK(z0)) MARK(diff(z0,z1)) -> c19(A__DIFF(mark(z0),mark(z1)),MARK(z1)) MARK(false()) -> c23() MARK(if(z0,z1,z2)) -> c17(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(leq(z0,z1)) -> c15(A__LEQ(mark(z0),mark(z1)),MARK(z0)) MARK(leq(z0,z1)) -> c16(A__LEQ(mark(z0),mark(z1)),MARK(z1)) MARK(p(z0)) -> c14(A__P(mark(z0)),MARK(z0)) MARK(s(z0)) -> c21(MARK(z0)) MARK(true()) -> c22() - Weak TRS: a__diff(z0,z1) -> a__if(a__leq(mark(z0),mark(z1)),0(),s(diff(p(z0),z1))) a__diff(z0,z1) -> diff(z0,z1) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__leq(z0,z1) -> leq(z0,z1) a__leq(0(),z0) -> true() a__leq(s(z0),0()) -> false() a__leq(s(z0),s(z1)) -> a__leq(mark(z0),mark(z1)) a__p(z0) -> p(z0) a__p(0()) -> 0() a__p(s(z0)) -> mark(z0) mark(0()) -> 0() mark(diff(z0,z1)) -> a__diff(mark(z0),mark(z1)) mark(false()) -> false() mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(leq(z0,z1)) -> a__leq(mark(z0),mark(z1)) mark(p(z0)) -> a__p(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(true()) -> true() - Signature: {A__DIFF/2,A__IF/3,A__LEQ/2,A__P/1,MARK/1,a__diff/2,a__if/3,a__leq/2,a__p/1,mark/1} / {0/0,c/0,c1/1,c10/0 ,c11/3,c12/3,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/0,c20/0,c21/1,c22/0,c23/0,c3/0,c4/0,c5/2,c6/2,c7/0 ,c8/1,c9/1,diff/2,false/0,if/3,leq/2,p/1,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__DIFF,A__IF,A__LEQ,A__P,MARK,a__diff,a__if,a__leq,a__p ,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8 ,c9,diff,false,if,leq,p,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> diff(x,y)} = MARK(diff(x,y)) ->^+ c18(A__DIFF(mark(x),mark(y)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)