WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: DEL(z0,cons(z1,z2)) -> c6(IF2(eq(z0,z1),z0,z1,z2),EQ(z0,z1)) DEL(z0,nil()) -> c5() EQ(0(),0()) -> c9() EQ(0(),s(z0)) -> c10() EQ(s(z0),0()) -> c11() EQ(s(z0),s(z1)) -> c12(EQ(z0,z1)) GE(0(),0()) -> c16() GE(0(),s(z0)) -> c18() GE(s(z0),0()) -> c17() GE(s(z0),s(z1)) -> c19(GE(z0,z1)) H(cons(z0,z1)) -> c21(H(z1)) H(nil()) -> c20() IF1(false(),z0,z1,z2) -> c4(MAX(cons(z1,z2))) IF1(true(),z0,z1,z2) -> c3(MAX(cons(z0,z2))) IF2(false(),z0,z1,z2) -> c8(DEL(z0,z2)) IF2(true(),z0,z1,z2) -> c7() MAX(cons(z0,cons(z1,z2))) -> c2(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) MAX(cons(z0,nil())) -> c1() MAX(nil()) -> c() SORT(cons(z0,z1)) -> c14(MAX(cons(z0,z1))) SORT(cons(z0,z1)) -> c15(SORT(h(del(max(cons(z0,z1)),cons(z0,z1)))) ,H(del(max(cons(z0,z1)),cons(z0,z1))) ,DEL(max(cons(z0,z1)),cons(z0,z1)) ,MAX(cons(z0,z1))) SORT(nil()) -> c13() - Weak TRS: del(z0,cons(z1,z2)) -> if2(eq(z0,z1),z0,z1,z2) del(z0,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) ge(0(),0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),0()) -> true() ge(s(z0),s(z1)) -> ge(z0,z1) h(cons(z0,z1)) -> cons(z0,h(z1)) h(nil()) -> nil() if1(false(),z0,z1,z2) -> max(cons(z1,z2)) if1(true(),z0,z1,z2) -> max(cons(z0,z2)) if2(false(),z0,z1,z2) -> cons(z1,del(z0,z2)) if2(true(),z0,z1,z2) -> z2 max(cons(z0,cons(z1,z2))) -> if1(ge(z0,z1),z0,z1,z2) max(cons(z0,nil())) -> z0 max(nil()) -> 0() sort(cons(z0,z1)) -> cons(max(cons(z0,z1)),sort(h(del(max(cons(z0,z1)),cons(z0,z1))))) sort(nil()) -> nil() - Signature: {DEL/2,EQ/2,GE/2,H/1,IF1/4,IF2/4,MAX/1,SORT/1,del/2,eq/2,ge/2,h/1,if1/4,if2/4,max/1,sort/1} / {0/0,c/0,c1/0 ,c10/0,c11/0,c12/1,c13/0,c14/1,c15/4,c16/0,c17/0,c18/0,c19/1,c2/2,c20/0,c21/1,c3/1,c4/1,c5/0,c6/2,c7/0,c8/1 ,c9/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {DEL,EQ,GE,H,IF1,IF2,MAX,SORT,del,eq,ge,h,if1,if2,max ,sort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,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: DEL(z0,cons(z1,z2)) -> c6(IF2(eq(z0,z1),z0,z1,z2),EQ(z0,z1)) DEL(z0,nil()) -> c5() EQ(0(),0()) -> c9() EQ(0(),s(z0)) -> c10() EQ(s(z0),0()) -> c11() EQ(s(z0),s(z1)) -> c12(EQ(z0,z1)) GE(0(),0()) -> c16() GE(0(),s(z0)) -> c18() GE(s(z0),0()) -> c17() GE(s(z0),s(z1)) -> c19(GE(z0,z1)) H(cons(z0,z1)) -> c21(H(z1)) H(nil()) -> c20() IF1(false(),z0,z1,z2) -> c4(MAX(cons(z1,z2))) IF1(true(),z0,z1,z2) -> c3(MAX(cons(z0,z2))) IF2(false(),z0,z1,z2) -> c8(DEL(z0,z2)) IF2(true(),z0,z1,z2) -> c7() MAX(cons(z0,cons(z1,z2))) -> c2(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) MAX(cons(z0,nil())) -> c1() MAX(nil()) -> c() SORT(cons(z0,z1)) -> c14(MAX(cons(z0,z1))) SORT(cons(z0,z1)) -> c15(SORT(h(del(max(cons(z0,z1)),cons(z0,z1)))) ,H(del(max(cons(z0,z1)),cons(z0,z1))) ,DEL(max(cons(z0,z1)),cons(z0,z1)) ,MAX(cons(z0,z1))) SORT(nil()) -> c13() - Weak TRS: del(z0,cons(z1,z2)) -> if2(eq(z0,z1),z0,z1,z2) del(z0,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) ge(0(),0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),0()) -> true() ge(s(z0),s(z1)) -> ge(z0,z1) h(cons(z0,z1)) -> cons(z0,h(z1)) h(nil()) -> nil() if1(false(),z0,z1,z2) -> max(cons(z1,z2)) if1(true(),z0,z1,z2) -> max(cons(z0,z2)) if2(false(),z0,z1,z2) -> cons(z1,del(z0,z2)) if2(true(),z0,z1,z2) -> z2 max(cons(z0,cons(z1,z2))) -> if1(ge(z0,z1),z0,z1,z2) max(cons(z0,nil())) -> z0 max(nil()) -> 0() sort(cons(z0,z1)) -> cons(max(cons(z0,z1)),sort(h(del(max(cons(z0,z1)),cons(z0,z1))))) sort(nil()) -> nil() - Signature: {DEL/2,EQ/2,GE/2,H/1,IF1/4,IF2/4,MAX/1,SORT/1,del/2,eq/2,ge/2,h/1,if1/4,if2/4,max/1,sort/1} / {0/0,c/0,c1/0 ,c10/0,c11/0,c12/1,c13/0,c14/1,c15/4,c16/0,c17/0,c18/0,c19/1,c2/2,c20/0,c21/1,c3/1,c4/1,c5/0,c6/2,c7/0,c8/1 ,c9/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {DEL,EQ,GE,H,IF1,IF2,MAX,SORT,del,eq,ge,h,if1,if2,max ,sort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,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: DEL(z0,cons(z1,z2)) -> c6(IF2(eq(z0,z1),z0,z1,z2),EQ(z0,z1)) DEL(z0,nil()) -> c5() EQ(0(),0()) -> c9() EQ(0(),s(z0)) -> c10() EQ(s(z0),0()) -> c11() EQ(s(z0),s(z1)) -> c12(EQ(z0,z1)) GE(0(),0()) -> c16() GE(0(),s(z0)) -> c18() GE(s(z0),0()) -> c17() GE(s(z0),s(z1)) -> c19(GE(z0,z1)) H(cons(z0,z1)) -> c21(H(z1)) H(nil()) -> c20() IF1(false(),z0,z1,z2) -> c4(MAX(cons(z1,z2))) IF1(true(),z0,z1,z2) -> c3(MAX(cons(z0,z2))) IF2(false(),z0,z1,z2) -> c8(DEL(z0,z2)) IF2(true(),z0,z1,z2) -> c7() MAX(cons(z0,cons(z1,z2))) -> c2(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) MAX(cons(z0,nil())) -> c1() MAX(nil()) -> c() SORT(cons(z0,z1)) -> c14(MAX(cons(z0,z1))) SORT(cons(z0,z1)) -> c15(SORT(h(del(max(cons(z0,z1)),cons(z0,z1)))) ,H(del(max(cons(z0,z1)),cons(z0,z1))) ,DEL(max(cons(z0,z1)),cons(z0,z1)) ,MAX(cons(z0,z1))) SORT(nil()) -> c13() - Weak TRS: del(z0,cons(z1,z2)) -> if2(eq(z0,z1),z0,z1,z2) del(z0,nil()) -> nil() eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) ge(0(),0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),0()) -> true() ge(s(z0),s(z1)) -> ge(z0,z1) h(cons(z0,z1)) -> cons(z0,h(z1)) h(nil()) -> nil() if1(false(),z0,z1,z2) -> max(cons(z1,z2)) if1(true(),z0,z1,z2) -> max(cons(z0,z2)) if2(false(),z0,z1,z2) -> cons(z1,del(z0,z2)) if2(true(),z0,z1,z2) -> z2 max(cons(z0,cons(z1,z2))) -> if1(ge(z0,z1),z0,z1,z2) max(cons(z0,nil())) -> z0 max(nil()) -> 0() sort(cons(z0,z1)) -> cons(max(cons(z0,z1)),sort(h(del(max(cons(z0,z1)),cons(z0,z1))))) sort(nil()) -> nil() - Signature: {DEL/2,EQ/2,GE/2,H/1,IF1/4,IF2/4,MAX/1,SORT/1,del/2,eq/2,ge/2,h/1,if1/4,if2/4,max/1,sort/1} / {0/0,c/0,c1/0 ,c10/0,c11/0,c12/1,c13/0,c14/1,c15/4,c16/0,c17/0,c18/0,c19/1,c2/2,c20/0,c21/1,c3/1,c4/1,c5/0,c6/2,c7/0,c8/1 ,c9/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {DEL,EQ,GE,H,IF1,IF2,MAX,SORT,del,eq,ge,h,if1,if2,max ,sort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,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: EQ(x,y){x -> s(x),y -> s(y)} = EQ(s(x),s(y)) ->^+ c12(EQ(x,y)) = C[EQ(x,y) = EQ(x,y){}] WORST_CASE(Omega(n^1),?)