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