WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: COND1(false(),z0,z1) -> c3(COND2(gt(z0,max(z1)),z0,z1),GT(z0,max(z1)),MAX(z1)) COND1(true(),z0,z1) -> c2(ST(s(z0),z1)) COND2(false(),z0,z1) -> c5(ST(s(z0),z1)) COND2(true(),z0,z1) -> c4() EQUAL(0(),0()) -> c11() EQUAL(0(),s(z0)) -> c13() EQUAL(s(z0),0()) -> c12() EQUAL(s(z0),s(z1)) -> c14(EQUAL(z0,z1)) GT(0(),z0) -> c15() GT(s(z0),0()) -> c16() GT(s(z0),s(z1)) -> c17(GT(z0,z1)) IF(false(),z0,z1) -> c22() IF(true(),z0,z1) -> c21() MAX(cons(z0,z1)) -> c19(IF(gt(z0,max(z1)),z0,max(z1)),GT(z0,max(z1)),MAX(z1)) MAX(cons(z0,z1)) -> c20(IF(gt(z0,max(z1)),z0,max(z1)),MAX(z1)) MAX(nil()) -> c18() MEMBER(z0,cons(z1,z2)) -> c7(OR(equal(z0,z1),member(z0,z2)),EQUAL(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c8(OR(equal(z0,z1),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c6() OR(z0,false()) -> c10() OR(z0,true()) -> c9() SORT(z0) -> c(ST(0(),z0)) ST(z0,z1) -> c1(COND1(member(z0,z1),z0,z1),MEMBER(z0,z1)) - Weak TRS: cond1(false(),z0,z1) -> cond2(gt(z0,max(z1)),z0,z1) cond1(true(),z0,z1) -> cons(z0,st(s(z0),z1)) cond2(false(),z0,z1) -> st(s(z0),z1) cond2(true(),z0,z1) -> nil() equal(0(),0()) -> true() equal(0(),s(z0)) -> false() equal(s(z0),0()) -> false() equal(s(z0),s(z1)) -> equal(z0,z1) gt(0(),z0) -> false() gt(s(z0),0()) -> true() gt(s(z0),s(z1)) -> gt(z0,z1) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 max(cons(z0,z1)) -> if(gt(z0,max(z1)),z0,max(z1)) max(nil()) -> 0() member(z0,cons(z1,z2)) -> or(equal(z0,z1),member(z0,z2)) member(z0,nil()) -> false() or(z0,false()) -> z0 or(z0,true()) -> true() sort(z0) -> st(0(),z0) st(z0,z1) -> cond1(member(z0,z1),z0,z1) - Signature: {COND1/3,COND2/3,EQUAL/2,GT/2,IF/3,MAX/1,MEMBER/2,OR/2,SORT/1,ST/2,cond1/3,cond2/3,equal/2,gt/2,if/3,max/1 ,member/2,or/2,sort/1,st/2} / {0/0,c/1,c1/2,c10/0,c11/0,c12/0,c13/0,c14/1,c15/0,c16/0,c17/1,c18/0,c19/3,c2/1 ,c20/2,c21/0,c22/0,c3/3,c4/0,c5/1,c6/0,c7/2,c8/2,c9/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {COND1,COND2,EQUAL,GT,IF,MAX,MEMBER,OR,SORT,ST,cond1,cond2 ,equal,gt,if,max,member,or,sort,st} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: COND1(false(),z0,z1) -> c3(COND2(gt(z0,max(z1)),z0,z1),GT(z0,max(z1)),MAX(z1)) COND1(true(),z0,z1) -> c2(ST(s(z0),z1)) COND2(false(),z0,z1) -> c5(ST(s(z0),z1)) COND2(true(),z0,z1) -> c4() EQUAL(0(),0()) -> c11() EQUAL(0(),s(z0)) -> c13() EQUAL(s(z0),0()) -> c12() EQUAL(s(z0),s(z1)) -> c14(EQUAL(z0,z1)) GT(0(),z0) -> c15() GT(s(z0),0()) -> c16() GT(s(z0),s(z1)) -> c17(GT(z0,z1)) IF(false(),z0,z1) -> c22() IF(true(),z0,z1) -> c21() MAX(cons(z0,z1)) -> c19(IF(gt(z0,max(z1)),z0,max(z1)),GT(z0,max(z1)),MAX(z1)) MAX(cons(z0,z1)) -> c20(IF(gt(z0,max(z1)),z0,max(z1)),MAX(z1)) MAX(nil()) -> c18() MEMBER(z0,cons(z1,z2)) -> c7(OR(equal(z0,z1),member(z0,z2)),EQUAL(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c8(OR(equal(z0,z1),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c6() OR(z0,false()) -> c10() OR(z0,true()) -> c9() SORT(z0) -> c(ST(0(),z0)) ST(z0,z1) -> c1(COND1(member(z0,z1),z0,z1),MEMBER(z0,z1)) - Weak TRS: cond1(false(),z0,z1) -> cond2(gt(z0,max(z1)),z0,z1) cond1(true(),z0,z1) -> cons(z0,st(s(z0),z1)) cond2(false(),z0,z1) -> st(s(z0),z1) cond2(true(),z0,z1) -> nil() equal(0(),0()) -> true() equal(0(),s(z0)) -> false() equal(s(z0),0()) -> false() equal(s(z0),s(z1)) -> equal(z0,z1) gt(0(),z0) -> false() gt(s(z0),0()) -> true() gt(s(z0),s(z1)) -> gt(z0,z1) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 max(cons(z0,z1)) -> if(gt(z0,max(z1)),z0,max(z1)) max(nil()) -> 0() member(z0,cons(z1,z2)) -> or(equal(z0,z1),member(z0,z2)) member(z0,nil()) -> false() or(z0,false()) -> z0 or(z0,true()) -> true() sort(z0) -> st(0(),z0) st(z0,z1) -> cond1(member(z0,z1),z0,z1) - Signature: {COND1/3,COND2/3,EQUAL/2,GT/2,IF/3,MAX/1,MEMBER/2,OR/2,SORT/1,ST/2,cond1/3,cond2/3,equal/2,gt/2,if/3,max/1 ,member/2,or/2,sort/1,st/2} / {0/0,c/1,c1/2,c10/0,c11/0,c12/0,c13/0,c14/1,c15/0,c16/0,c17/1,c18/0,c19/3,c2/1 ,c20/2,c21/0,c22/0,c3/3,c4/0,c5/1,c6/0,c7/2,c8/2,c9/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {COND1,COND2,EQUAL,GT,IF,MAX,MEMBER,OR,SORT,ST,cond1,cond2 ,equal,gt,if,max,member,or,sort,st} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: COND1(false(),z0,z1) -> c3(COND2(gt(z0,max(z1)),z0,z1),GT(z0,max(z1)),MAX(z1)) COND1(true(),z0,z1) -> c2(ST(s(z0),z1)) COND2(false(),z0,z1) -> c5(ST(s(z0),z1)) COND2(true(),z0,z1) -> c4() EQUAL(0(),0()) -> c11() EQUAL(0(),s(z0)) -> c13() EQUAL(s(z0),0()) -> c12() EQUAL(s(z0),s(z1)) -> c14(EQUAL(z0,z1)) GT(0(),z0) -> c15() GT(s(z0),0()) -> c16() GT(s(z0),s(z1)) -> c17(GT(z0,z1)) IF(false(),z0,z1) -> c22() IF(true(),z0,z1) -> c21() MAX(cons(z0,z1)) -> c19(IF(gt(z0,max(z1)),z0,max(z1)),GT(z0,max(z1)),MAX(z1)) MAX(cons(z0,z1)) -> c20(IF(gt(z0,max(z1)),z0,max(z1)),MAX(z1)) MAX(nil()) -> c18() MEMBER(z0,cons(z1,z2)) -> c7(OR(equal(z0,z1),member(z0,z2)),EQUAL(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c8(OR(equal(z0,z1),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c6() OR(z0,false()) -> c10() OR(z0,true()) -> c9() SORT(z0) -> c(ST(0(),z0)) ST(z0,z1) -> c1(COND1(member(z0,z1),z0,z1),MEMBER(z0,z1)) - Weak TRS: cond1(false(),z0,z1) -> cond2(gt(z0,max(z1)),z0,z1) cond1(true(),z0,z1) -> cons(z0,st(s(z0),z1)) cond2(false(),z0,z1) -> st(s(z0),z1) cond2(true(),z0,z1) -> nil() equal(0(),0()) -> true() equal(0(),s(z0)) -> false() equal(s(z0),0()) -> false() equal(s(z0),s(z1)) -> equal(z0,z1) gt(0(),z0) -> false() gt(s(z0),0()) -> true() gt(s(z0),s(z1)) -> gt(z0,z1) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 max(cons(z0,z1)) -> if(gt(z0,max(z1)),z0,max(z1)) max(nil()) -> 0() member(z0,cons(z1,z2)) -> or(equal(z0,z1),member(z0,z2)) member(z0,nil()) -> false() or(z0,false()) -> z0 or(z0,true()) -> true() sort(z0) -> st(0(),z0) st(z0,z1) -> cond1(member(z0,z1),z0,z1) - Signature: {COND1/3,COND2/3,EQUAL/2,GT/2,IF/3,MAX/1,MEMBER/2,OR/2,SORT/1,ST/2,cond1/3,cond2/3,equal/2,gt/2,if/3,max/1 ,member/2,or/2,sort/1,st/2} / {0/0,c/1,c1/2,c10/0,c11/0,c12/0,c13/0,c14/1,c15/0,c16/0,c17/1,c18/0,c19/3,c2/1 ,c20/2,c21/0,c22/0,c3/3,c4/0,c5/1,c6/0,c7/2,c8/2,c9/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {COND1,COND2,EQUAL,GT,IF,MAX,MEMBER,OR,SORT,ST,cond1,cond2 ,equal,gt,if,max,member,or,sort,st} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EQUAL(x,y){x -> s(x),y -> s(y)} = EQUAL(s(x),s(y)) ->^+ c14(EQUAL(x,y)) = C[EQUAL(x,y) = EQUAL(x,y){}] WORST_CASE(Omega(n^1),?)