WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: DEL(z0,cons(z1,z2)) -> c17(IF(eq(z0,z1),z2,cons(z1,del(z0,z2))),EQ(z0,z1)) DEL(z0,cons(z1,z2)) -> c18(IF(eq(z0,z1),z2,cons(z1,del(z0,z2))),DEL(z0,z2)) DEL(z0,nil()) -> c16() EQ(0(),0()) -> c3() EQ(0(),s(z0)) -> c4() EQ(s(z0),0()) -> c5() EQ(s(z0),s(z1)) -> c6(EQ(z0,z1)) IF(false(),z0,z1) -> c8() IF(true(),z0,z1) -> c7() LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) MIN(z0,cons(z1,z2)) -> c13(IF(le(z0,z1),min(z0,z2),min(z1,z2)),LE(z0,z1)) MIN(z0,cons(z1,z2)) -> c14(IF(le(z0,z1),min(z0,z2),min(z1,z2)),MIN(z0,z2)) MIN(z0,cons(z1,z2)) -> c15(IF(le(z0,z1),min(z0,z2),min(z1,z2)),MIN(z1,z2)) MIN(z0,nil()) -> c12() MINSORT(cons(z0,z1)) -> c10(MIN(z0,z1)) MINSORT(cons(z0,z1)) -> c11(MINSORT(del(min(z0,z1),cons(z0,z1))),DEL(min(z0,z1),cons(z0,z1)),MIN(z0,z1)) MINSORT(nil()) -> c9() - Weak TRS: del(z0,cons(z1,z2)) -> if(eq(z0,z1),z2,cons(z1,del(z0,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) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) min(z0,cons(z1,z2)) -> if(le(z0,z1),min(z0,z2),min(z1,z2)) min(z0,nil()) -> z0 minsort(cons(z0,z1)) -> cons(min(z0,z1),minsort(del(min(z0,z1),cons(z0,z1)))) minsort(nil()) -> nil() - Signature: {DEL/2,EQ/2,IF/3,LE/2,MIN/2,MINSORT/1,del/2,eq/2,if/3,le/2,min/2,minsort/1} / {0/0,c/0,c1/0,c10/1,c11/3 ,c12/0,c13/2,c14/2,c15/2,c16/0,c17/2,c18/2,c2/1,c3/0,c4/0,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,nil/0,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {DEL,EQ,IF,LE,MIN,MINSORT,del,eq,if,le,min ,minsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,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)) -> c17(IF(eq(z0,z1),z2,cons(z1,del(z0,z2))),EQ(z0,z1)) DEL(z0,cons(z1,z2)) -> c18(IF(eq(z0,z1),z2,cons(z1,del(z0,z2))),DEL(z0,z2)) DEL(z0,nil()) -> c16() EQ(0(),0()) -> c3() EQ(0(),s(z0)) -> c4() EQ(s(z0),0()) -> c5() EQ(s(z0),s(z1)) -> c6(EQ(z0,z1)) IF(false(),z0,z1) -> c8() IF(true(),z0,z1) -> c7() LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) MIN(z0,cons(z1,z2)) -> c13(IF(le(z0,z1),min(z0,z2),min(z1,z2)),LE(z0,z1)) MIN(z0,cons(z1,z2)) -> c14(IF(le(z0,z1),min(z0,z2),min(z1,z2)),MIN(z0,z2)) MIN(z0,cons(z1,z2)) -> c15(IF(le(z0,z1),min(z0,z2),min(z1,z2)),MIN(z1,z2)) MIN(z0,nil()) -> c12() MINSORT(cons(z0,z1)) -> c10(MIN(z0,z1)) MINSORT(cons(z0,z1)) -> c11(MINSORT(del(min(z0,z1),cons(z0,z1))),DEL(min(z0,z1),cons(z0,z1)),MIN(z0,z1)) MINSORT(nil()) -> c9() - Weak TRS: del(z0,cons(z1,z2)) -> if(eq(z0,z1),z2,cons(z1,del(z0,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) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) min(z0,cons(z1,z2)) -> if(le(z0,z1),min(z0,z2),min(z1,z2)) min(z0,nil()) -> z0 minsort(cons(z0,z1)) -> cons(min(z0,z1),minsort(del(min(z0,z1),cons(z0,z1)))) minsort(nil()) -> nil() - Signature: {DEL/2,EQ/2,IF/3,LE/2,MIN/2,MINSORT/1,del/2,eq/2,if/3,le/2,min/2,minsort/1} / {0/0,c/0,c1/0,c10/1,c11/3 ,c12/0,c13/2,c14/2,c15/2,c16/0,c17/2,c18/2,c2/1,c3/0,c4/0,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,nil/0,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {DEL,EQ,IF,LE,MIN,MINSORT,del,eq,if,le,min ,minsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,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)) -> c17(IF(eq(z0,z1),z2,cons(z1,del(z0,z2))),EQ(z0,z1)) DEL(z0,cons(z1,z2)) -> c18(IF(eq(z0,z1),z2,cons(z1,del(z0,z2))),DEL(z0,z2)) DEL(z0,nil()) -> c16() EQ(0(),0()) -> c3() EQ(0(),s(z0)) -> c4() EQ(s(z0),0()) -> c5() EQ(s(z0),s(z1)) -> c6(EQ(z0,z1)) IF(false(),z0,z1) -> c8() IF(true(),z0,z1) -> c7() LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) MIN(z0,cons(z1,z2)) -> c13(IF(le(z0,z1),min(z0,z2),min(z1,z2)),LE(z0,z1)) MIN(z0,cons(z1,z2)) -> c14(IF(le(z0,z1),min(z0,z2),min(z1,z2)),MIN(z0,z2)) MIN(z0,cons(z1,z2)) -> c15(IF(le(z0,z1),min(z0,z2),min(z1,z2)),MIN(z1,z2)) MIN(z0,nil()) -> c12() MINSORT(cons(z0,z1)) -> c10(MIN(z0,z1)) MINSORT(cons(z0,z1)) -> c11(MINSORT(del(min(z0,z1),cons(z0,z1))),DEL(min(z0,z1),cons(z0,z1)),MIN(z0,z1)) MINSORT(nil()) -> c9() - Weak TRS: del(z0,cons(z1,z2)) -> if(eq(z0,z1),z2,cons(z1,del(z0,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) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) min(z0,cons(z1,z2)) -> if(le(z0,z1),min(z0,z2),min(z1,z2)) min(z0,nil()) -> z0 minsort(cons(z0,z1)) -> cons(min(z0,z1),minsort(del(min(z0,z1),cons(z0,z1)))) minsort(nil()) -> nil() - Signature: {DEL/2,EQ/2,IF/3,LE/2,MIN/2,MINSORT/1,del/2,eq/2,if/3,le/2,min/2,minsort/1} / {0/0,c/0,c1/0,c10/1,c11/3 ,c12/0,c13/2,c14/2,c15/2,c16/0,c17/2,c18/2,c2/1,c3/0,c4/0,c5/0,c6/1,c7/0,c8/0,c9/0,cons/2,false/0,nil/0,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {DEL,EQ,IF,LE,MIN,MINSORT,del,eq,if,le,min ,minsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,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: DEL(x,z){z -> cons(y,z)} = DEL(x,cons(y,z)) ->^+ c18(IF(eq(x,y),z,cons(y,del(x,z))),DEL(x,z)) = C[DEL(x,z) = DEL(x,z){}] WORST_CASE(Omega(n^1),?)