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: ADDLIST(z0,z1) -> c12(IF(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) ,LE(0(),min(len(z0),len(z1))) ,MIN(len(z0),len(z1)) ,LEN(z0)) ADDLIST(z0,z1) -> c13(IF(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) ,LE(0(),min(len(z0),len(z1))) ,MIN(len(z0),len(z1)) ,LEN(z1)) IF(false(),z0,z1,z2,z3) -> c14() IF(true(),z0,z1,z2,z3) -> c15(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,LE(s(z0),min(len(z1),len(z2))) ,MIN(len(z1),len(z2)) ,LEN(z1)) IF(true(),z0,z1,z2,z3) -> c16(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,LE(s(z0),min(len(z1),len(z2))) ,MIN(len(z1),len(z2)) ,LEN(z2)) IF(true(),z0,z1,z2,z3) -> c17(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,SUM(take(z0,z1),take(z0,z2)) ,TAKE(z0,z1)) IF(true(),z0,z1,z2,z3) -> c18(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,SUM(take(z0,z1),take(z0,z2)) ,TAKE(z0,z2)) LE(0(),z0) -> c7() LE(s(z0),0()) -> c8() LE(s(z0),s(z1)) -> c9(LE(z0,z1)) LEN(cons(z0,z1)) -> c4(LEN(z1)) LEN(nil()) -> c3() MIN(0(),z0) -> c() MIN(s(z0),0()) -> c1() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) SUM(z0,0()) -> c5() SUM(z0,s(z1)) -> c6(SUM(z0,z1)) TAKE(0(),cons(z0,z1)) -> c10() TAKE(s(z0),cons(z1,z2)) -> c11(TAKE(z0,z2)) - Weak TRS: addList(z0,z1) -> if(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) if(false(),z0,z1,z2,z3) -> z3 if(true(),z0,z1,z2,z3) -> if(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) len(cons(z0,z1)) -> s(len(z1)) len(nil()) -> 0() min(0(),z0) -> 0() min(s(z0),0()) -> 0() min(s(z0),s(z1)) -> min(z0,z1) sum(z0,0()) -> z0 sum(z0,s(z1)) -> s(sum(z0,z1)) take(0(),cons(z0,z1)) -> z0 take(s(z0),cons(z1,z2)) -> take(z0,z2) - Signature: {ADDLIST/2,IF/5,LE/2,LEN/1,MIN/2,SUM/2,TAKE/2,addList/2,if/5,le/2,len/1,min/2,sum/2,take/2} / {0/0,c/0,c1/0 ,c10/0,c11/1,c12/4,c13/4,c14/0,c15/4,c16/4,c17/3,c18/3,c2/1,c3/0,c4/1,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2 ,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ADDLIST,IF,LE,LEN,MIN,SUM,TAKE,addList,if,le,len,min,sum ,take} 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: ADDLIST(z0,z1) -> c12(IF(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) ,LE(0(),min(len(z0),len(z1))) ,MIN(len(z0),len(z1)) ,LEN(z0)) ADDLIST(z0,z1) -> c13(IF(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) ,LE(0(),min(len(z0),len(z1))) ,MIN(len(z0),len(z1)) ,LEN(z1)) IF(false(),z0,z1,z2,z3) -> c14() IF(true(),z0,z1,z2,z3) -> c15(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,LE(s(z0),min(len(z1),len(z2))) ,MIN(len(z1),len(z2)) ,LEN(z1)) IF(true(),z0,z1,z2,z3) -> c16(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,LE(s(z0),min(len(z1),len(z2))) ,MIN(len(z1),len(z2)) ,LEN(z2)) IF(true(),z0,z1,z2,z3) -> c17(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,SUM(take(z0,z1),take(z0,z2)) ,TAKE(z0,z1)) IF(true(),z0,z1,z2,z3) -> c18(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,SUM(take(z0,z1),take(z0,z2)) ,TAKE(z0,z2)) LE(0(),z0) -> c7() LE(s(z0),0()) -> c8() LE(s(z0),s(z1)) -> c9(LE(z0,z1)) LEN(cons(z0,z1)) -> c4(LEN(z1)) LEN(nil()) -> c3() MIN(0(),z0) -> c() MIN(s(z0),0()) -> c1() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) SUM(z0,0()) -> c5() SUM(z0,s(z1)) -> c6(SUM(z0,z1)) TAKE(0(),cons(z0,z1)) -> c10() TAKE(s(z0),cons(z1,z2)) -> c11(TAKE(z0,z2)) - Weak TRS: addList(z0,z1) -> if(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) if(false(),z0,z1,z2,z3) -> z3 if(true(),z0,z1,z2,z3) -> if(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) len(cons(z0,z1)) -> s(len(z1)) len(nil()) -> 0() min(0(),z0) -> 0() min(s(z0),0()) -> 0() min(s(z0),s(z1)) -> min(z0,z1) sum(z0,0()) -> z0 sum(z0,s(z1)) -> s(sum(z0,z1)) take(0(),cons(z0,z1)) -> z0 take(s(z0),cons(z1,z2)) -> take(z0,z2) - Signature: {ADDLIST/2,IF/5,LE/2,LEN/1,MIN/2,SUM/2,TAKE/2,addList/2,if/5,le/2,len/1,min/2,sum/2,take/2} / {0/0,c/0,c1/0 ,c10/0,c11/1,c12/4,c13/4,c14/0,c15/4,c16/4,c17/3,c18/3,c2/1,c3/0,c4/1,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2 ,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ADDLIST,IF,LE,LEN,MIN,SUM,TAKE,addList,if,le,len,min,sum ,take} 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: ADDLIST(z0,z1) -> c12(IF(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) ,LE(0(),min(len(z0),len(z1))) ,MIN(len(z0),len(z1)) ,LEN(z0)) ADDLIST(z0,z1) -> c13(IF(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) ,LE(0(),min(len(z0),len(z1))) ,MIN(len(z0),len(z1)) ,LEN(z1)) IF(false(),z0,z1,z2,z3) -> c14() IF(true(),z0,z1,z2,z3) -> c15(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,LE(s(z0),min(len(z1),len(z2))) ,MIN(len(z1),len(z2)) ,LEN(z1)) IF(true(),z0,z1,z2,z3) -> c16(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,LE(s(z0),min(len(z1),len(z2))) ,MIN(len(z1),len(z2)) ,LEN(z2)) IF(true(),z0,z1,z2,z3) -> c17(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,SUM(take(z0,z1),take(z0,z2)) ,TAKE(z0,z1)) IF(true(),z0,z1,z2,z3) -> c18(IF(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) ,SUM(take(z0,z1),take(z0,z2)) ,TAKE(z0,z2)) LE(0(),z0) -> c7() LE(s(z0),0()) -> c8() LE(s(z0),s(z1)) -> c9(LE(z0,z1)) LEN(cons(z0,z1)) -> c4(LEN(z1)) LEN(nil()) -> c3() MIN(0(),z0) -> c() MIN(s(z0),0()) -> c1() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) SUM(z0,0()) -> c5() SUM(z0,s(z1)) -> c6(SUM(z0,z1)) TAKE(0(),cons(z0,z1)) -> c10() TAKE(s(z0),cons(z1,z2)) -> c11(TAKE(z0,z2)) - Weak TRS: addList(z0,z1) -> if(le(0(),min(len(z0),len(z1))),0(),z0,z1,nil()) if(false(),z0,z1,z2,z3) -> z3 if(true(),z0,z1,z2,z3) -> if(le(s(z0),min(len(z1),len(z2))) ,s(z0) ,z1 ,z2 ,cons(sum(take(z0,z1),take(z0,z2)),z3)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) len(cons(z0,z1)) -> s(len(z1)) len(nil()) -> 0() min(0(),z0) -> 0() min(s(z0),0()) -> 0() min(s(z0),s(z1)) -> min(z0,z1) sum(z0,0()) -> z0 sum(z0,s(z1)) -> s(sum(z0,z1)) take(0(),cons(z0,z1)) -> z0 take(s(z0),cons(z1,z2)) -> take(z0,z2) - Signature: {ADDLIST/2,IF/5,LE/2,LEN/1,MIN/2,SUM/2,TAKE/2,addList/2,if/5,le/2,len/1,min/2,sum/2,take/2} / {0/0,c/0,c1/0 ,c10/0,c11/1,c12/4,c13/4,c14/0,c15/4,c16/4,c17/3,c18/3,c2/1,c3/0,c4/1,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2 ,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ADDLIST,IF,LE,LEN,MIN,SUM,TAKE,addList,if,le,len,min,sum ,take} 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: LE(x,y){x -> s(x),y -> s(y)} = LE(s(x),s(y)) ->^+ c9(LE(x,y)) = C[LE(x,y) = LE(x,y){}] WORST_CASE(Omega(n^1),?)