tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EMPTY(cons(z0,z1)) -> c16() EMPTY(nil()) -> c15() EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) HEAD(cons(z0,z1)) -> c17() IF(false(),z0,z1,z2) -> c24(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,MIN(z0)) IF(false(),z0,z1,z2) -> c25(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,HEAD(z0)) IF(false(),z0,z1,z2) -> c26(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,TAIL(z0)) IF(true(),z0,z1,z2) -> c23() IF_MIN(false(),cons(z0,cons(z1,z2))) -> c10(MIN(cons(z1,z2))) IF_MIN(true(),cons(z0,cons(z1,z2))) -> c9(MIN(cons(z0,z2))) IF_REPLACE(false(),z0,z1,cons(z2,z3)) -> c14(REPLACE(z0,z1,z3)) IF_REPLACE(true(),z0,z1,cons(z2,z3)) -> c13() LE(0(),z0) -> c4() LE(s(z0),0()) -> c5() LE(s(z0),s(z1)) -> c6(LE(z0,z1)) MIN(cons(z0,cons(z1,z2))) -> c8(IF_MIN(le(z0,z1),cons(z0,cons(z1,z2))),LE(z0,z1)) MIN(cons(z0,nil())) -> c7() REPLACE(z0,z1,cons(z2,z3)) -> c12(IF_REPLACE(eq(z0,z2),z0,z1,cons(z2,z3)),EQ(z0,z2)) REPLACE(z0,z1,nil()) -> c11() SORT(z0) -> c20(SORTITER(z0,nil())) SORTITER(z0,z1) -> c21(IF(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))),EMPTY(z0)) SORTITER(z0,z1) -> c22(IF(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))),MIN(z0)) TAIL(cons(z0,z1)) -> c19() TAIL(nil()) -> c18() - Weak TRS: empty(cons(z0,z1)) -> false() empty(nil()) -> true() eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) head(cons(z0,z1)) -> z0 if(false(),z0,z1,z2) -> sortIter(replace(min(z0),head(z0),tail(z0)),z2) if(true(),z0,z1,z2) -> z1 if_min(false(),cons(z0,cons(z1,z2))) -> min(cons(z1,z2)) if_min(true(),cons(z0,cons(z1,z2))) -> min(cons(z0,z2)) if_replace(false(),z0,z1,cons(z2,z3)) -> cons(z2,replace(z0,z1,z3)) if_replace(true(),z0,z1,cons(z2,z3)) -> cons(z1,z3) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) min(cons(z0,cons(z1,z2))) -> if_min(le(z0,z1),cons(z0,cons(z1,z2))) min(cons(z0,nil())) -> z0 replace(z0,z1,cons(z2,z3)) -> if_replace(eq(z0,z2),z0,z1,cons(z2,z3)) replace(z0,z1,nil()) -> nil() sort(z0) -> sortIter(z0,nil()) sortIter(z0,z1) -> if(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() - Signature: {EMPTY/1,EQ/2,HEAD/1,IF/4,IF_MIN/2,IF_REPLACE/4,LE/2,MIN/1,REPLACE/3,SORT/1,SORTITER/2,TAIL/1,empty/1,eq/2 ,head/1,if/4,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,sortIter/2,tail/1} / {0/0,append/2,c/0,c1/0 ,c10/1,c11/0,c12/2,c13/0,c14/1,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/1,c21/2,c22/2,c23/0,c24/3,c25/3,c26/3 ,c3/1,c4/0,c5/0,c6/1,c7/0,c8/2,c9/1,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EMPTY,EQ,HEAD,IF,IF_MIN,IF_REPLACE,LE,MIN,REPLACE,SORT ,SORTITER,TAIL,empty,eq,head,if,if_min,if_replace,le,min,replace,sort,sortIter,tail} and constructors {0 ,append,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,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: EMPTY(cons(z0,z1)) -> c16() EMPTY(nil()) -> c15() EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) HEAD(cons(z0,z1)) -> c17() IF(false(),z0,z1,z2) -> c24(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,MIN(z0)) IF(false(),z0,z1,z2) -> c25(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,HEAD(z0)) IF(false(),z0,z1,z2) -> c26(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,TAIL(z0)) IF(true(),z0,z1,z2) -> c23() IF_MIN(false(),cons(z0,cons(z1,z2))) -> c10(MIN(cons(z1,z2))) IF_MIN(true(),cons(z0,cons(z1,z2))) -> c9(MIN(cons(z0,z2))) IF_REPLACE(false(),z0,z1,cons(z2,z3)) -> c14(REPLACE(z0,z1,z3)) IF_REPLACE(true(),z0,z1,cons(z2,z3)) -> c13() LE(0(),z0) -> c4() LE(s(z0),0()) -> c5() LE(s(z0),s(z1)) -> c6(LE(z0,z1)) MIN(cons(z0,cons(z1,z2))) -> c8(IF_MIN(le(z0,z1),cons(z0,cons(z1,z2))),LE(z0,z1)) MIN(cons(z0,nil())) -> c7() REPLACE(z0,z1,cons(z2,z3)) -> c12(IF_REPLACE(eq(z0,z2),z0,z1,cons(z2,z3)),EQ(z0,z2)) REPLACE(z0,z1,nil()) -> c11() SORT(z0) -> c20(SORTITER(z0,nil())) SORTITER(z0,z1) -> c21(IF(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))),EMPTY(z0)) SORTITER(z0,z1) -> c22(IF(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))),MIN(z0)) TAIL(cons(z0,z1)) -> c19() TAIL(nil()) -> c18() - Weak TRS: empty(cons(z0,z1)) -> false() empty(nil()) -> true() eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) head(cons(z0,z1)) -> z0 if(false(),z0,z1,z2) -> sortIter(replace(min(z0),head(z0),tail(z0)),z2) if(true(),z0,z1,z2) -> z1 if_min(false(),cons(z0,cons(z1,z2))) -> min(cons(z1,z2)) if_min(true(),cons(z0,cons(z1,z2))) -> min(cons(z0,z2)) if_replace(false(),z0,z1,cons(z2,z3)) -> cons(z2,replace(z0,z1,z3)) if_replace(true(),z0,z1,cons(z2,z3)) -> cons(z1,z3) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) min(cons(z0,cons(z1,z2))) -> if_min(le(z0,z1),cons(z0,cons(z1,z2))) min(cons(z0,nil())) -> z0 replace(z0,z1,cons(z2,z3)) -> if_replace(eq(z0,z2),z0,z1,cons(z2,z3)) replace(z0,z1,nil()) -> nil() sort(z0) -> sortIter(z0,nil()) sortIter(z0,z1) -> if(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() - Signature: {EMPTY/1,EQ/2,HEAD/1,IF/4,IF_MIN/2,IF_REPLACE/4,LE/2,MIN/1,REPLACE/3,SORT/1,SORTITER/2,TAIL/1,empty/1,eq/2 ,head/1,if/4,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,sortIter/2,tail/1} / {0/0,append/2,c/0,c1/0 ,c10/1,c11/0,c12/2,c13/0,c14/1,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/1,c21/2,c22/2,c23/0,c24/3,c25/3,c26/3 ,c3/1,c4/0,c5/0,c6/1,c7/0,c8/2,c9/1,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EMPTY,EQ,HEAD,IF,IF_MIN,IF_REPLACE,LE,MIN,REPLACE,SORT ,SORTITER,TAIL,empty,eq,head,if,if_min,if_replace,le,min,replace,sort,sortIter,tail} and constructors {0 ,append,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,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: EMPTY(cons(z0,z1)) -> c16() EMPTY(nil()) -> c15() EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) HEAD(cons(z0,z1)) -> c17() IF(false(),z0,z1,z2) -> c24(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,MIN(z0)) IF(false(),z0,z1,z2) -> c25(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,HEAD(z0)) IF(false(),z0,z1,z2) -> c26(SORTITER(replace(min(z0),head(z0),tail(z0)),z2) ,REPLACE(min(z0),head(z0),tail(z0)) ,TAIL(z0)) IF(true(),z0,z1,z2) -> c23() IF_MIN(false(),cons(z0,cons(z1,z2))) -> c10(MIN(cons(z1,z2))) IF_MIN(true(),cons(z0,cons(z1,z2))) -> c9(MIN(cons(z0,z2))) IF_REPLACE(false(),z0,z1,cons(z2,z3)) -> c14(REPLACE(z0,z1,z3)) IF_REPLACE(true(),z0,z1,cons(z2,z3)) -> c13() LE(0(),z0) -> c4() LE(s(z0),0()) -> c5() LE(s(z0),s(z1)) -> c6(LE(z0,z1)) MIN(cons(z0,cons(z1,z2))) -> c8(IF_MIN(le(z0,z1),cons(z0,cons(z1,z2))),LE(z0,z1)) MIN(cons(z0,nil())) -> c7() REPLACE(z0,z1,cons(z2,z3)) -> c12(IF_REPLACE(eq(z0,z2),z0,z1,cons(z2,z3)),EQ(z0,z2)) REPLACE(z0,z1,nil()) -> c11() SORT(z0) -> c20(SORTITER(z0,nil())) SORTITER(z0,z1) -> c21(IF(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))),EMPTY(z0)) SORTITER(z0,z1) -> c22(IF(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))),MIN(z0)) TAIL(cons(z0,z1)) -> c19() TAIL(nil()) -> c18() - Weak TRS: empty(cons(z0,z1)) -> false() empty(nil()) -> true() eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) head(cons(z0,z1)) -> z0 if(false(),z0,z1,z2) -> sortIter(replace(min(z0),head(z0),tail(z0)),z2) if(true(),z0,z1,z2) -> z1 if_min(false(),cons(z0,cons(z1,z2))) -> min(cons(z1,z2)) if_min(true(),cons(z0,cons(z1,z2))) -> min(cons(z0,z2)) if_replace(false(),z0,z1,cons(z2,z3)) -> cons(z2,replace(z0,z1,z3)) if_replace(true(),z0,z1,cons(z2,z3)) -> cons(z1,z3) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) min(cons(z0,cons(z1,z2))) -> if_min(le(z0,z1),cons(z0,cons(z1,z2))) min(cons(z0,nil())) -> z0 replace(z0,z1,cons(z2,z3)) -> if_replace(eq(z0,z2),z0,z1,cons(z2,z3)) replace(z0,z1,nil()) -> nil() sort(z0) -> sortIter(z0,nil()) sortIter(z0,z1) -> if(empty(z0),z0,z1,append(z1,cons(min(z0),nil()))) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() - Signature: {EMPTY/1,EQ/2,HEAD/1,IF/4,IF_MIN/2,IF_REPLACE/4,LE/2,MIN/1,REPLACE/3,SORT/1,SORTITER/2,TAIL/1,empty/1,eq/2 ,head/1,if/4,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,sortIter/2,tail/1} / {0/0,append/2,c/0,c1/0 ,c10/1,c11/0,c12/2,c13/0,c14/1,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/1,c21/2,c22/2,c23/0,c24/3,c25/3,c26/3 ,c3/1,c4/0,c5/0,c6/1,c7/0,c8/2,c9/1,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EMPTY,EQ,HEAD,IF,IF_MIN,IF_REPLACE,LE,MIN,REPLACE,SORT ,SORTITER,TAIL,empty,eq,head,if,if_min,if_replace,le,min,replace,sort,sortIter,tail} and constructors {0 ,append,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,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)) ->^+ c3(EQ(x,y)) = C[EQ(x,y) = EQ(x,y){}] WORST_CASE(Omega(n^1),?)