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)) -> c1()
            EMPTY(nil()) -> c()
            HEAD(cons(z0,z1)) -> c4()
            IF1(false(),z0,z1) -> c19(INT(s(0()),z1))
            IF1(true(),z0,z1) -> c18()
            IF2(false(),z0,z1) -> c21(INTLIST(int(p(z0),p(z1))),INT(p(z0),p(z1)),P(z0))
            IF2(false(),z0,z1) -> c22(INTLIST(int(p(z0),p(z1))),INT(p(z0),p(z1)),P(z1))
            IF2(true(),z0,z1) -> c20()
            IF_INT(false(),z0,z1,z2) -> c17(IF2(z0,z1,z2))
            IF_INT(true(),z0,z1,z2) -> c16(IF1(z0,z1,z2))
            IF_INTLIST(false(),z0) -> c12(HEAD(z0))
            IF_INTLIST(false(),z0) -> c13(INTLIST(tail(z0)),TAIL(z0))
            IF_INTLIST(true(),z0) -> c11()
            INT(z0,z1) -> c14(IF_INT(zero(z0),zero(z1),z0,z1),ZERO(z0))
            INT(z0,z1) -> c15(IF_INT(zero(z0),zero(z1),z0,z1),ZERO(z1))
            INTLIST(z0) -> c10(IF_INTLIST(empty(z0),z0),EMPTY(z0))
            P(0()) -> c7()
            P(s(0())) -> c8()
            P(s(s(z0))) -> c9(P(s(z0)))
            TAIL(cons(z0,z1)) -> c3()
            TAIL(nil()) -> c2()
            ZERO(0()) -> c5()
            ZERO(s(z0)) -> c6()
        - Weak TRS:
            empty(cons(z0,z1)) -> false()
            empty(nil()) -> true()
            head(cons(z0,z1)) -> z0
            if1(false(),z0,z1) -> cons(0(),int(s(0()),z1))
            if1(true(),z0,z1) -> cons(0(),nil())
            if2(false(),z0,z1) -> intlist(int(p(z0),p(z1)))
            if2(true(),z0,z1) -> nil()
            if_int(false(),z0,z1,z2) -> if2(z0,z1,z2)
            if_int(true(),z0,z1,z2) -> if1(z0,z1,z2)
            if_intlist(false(),z0) -> cons(s(head(z0)),intlist(tail(z0)))
            if_intlist(true(),z0) -> nil()
            int(z0,z1) -> if_int(zero(z0),zero(z1),z0,z1)
            intlist(z0) -> if_intlist(empty(z0),z0)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(z0))) -> s(p(s(z0)))
            tail(cons(z0,z1)) -> z1
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(z0)) -> false()
        - Signature:
            {EMPTY/1,HEAD/1,IF1/3,IF2/3,IF_INT/4,IF_INTLIST/2,INT/2,INTLIST/1,P/1,TAIL/1,ZERO/1,empty/1,head/1,if1/3
            ,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1} / {0/0,c/0,c1/0,c10/2,c11/0,c12/1,c13/2
            ,c14/2,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c3/0,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,cons/2
            ,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {EMPTY,HEAD,IF1,IF2,IF_INT,IF_INTLIST,INT,INTLIST,P,TAIL
            ,ZERO,empty,head,if1,if2,if_int,if_intlist,int,intlist,p,tail,zero} and constructors {0,c,c1,c10,c11,c12,c13
            ,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,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)) -> c1()
            EMPTY(nil()) -> c()
            HEAD(cons(z0,z1)) -> c4()
            IF1(false(),z0,z1) -> c19(INT(s(0()),z1))
            IF1(true(),z0,z1) -> c18()
            IF2(false(),z0,z1) -> c21(INTLIST(int(p(z0),p(z1))),INT(p(z0),p(z1)),P(z0))
            IF2(false(),z0,z1) -> c22(INTLIST(int(p(z0),p(z1))),INT(p(z0),p(z1)),P(z1))
            IF2(true(),z0,z1) -> c20()
            IF_INT(false(),z0,z1,z2) -> c17(IF2(z0,z1,z2))
            IF_INT(true(),z0,z1,z2) -> c16(IF1(z0,z1,z2))
            IF_INTLIST(false(),z0) -> c12(HEAD(z0))
            IF_INTLIST(false(),z0) -> c13(INTLIST(tail(z0)),TAIL(z0))
            IF_INTLIST(true(),z0) -> c11()
            INT(z0,z1) -> c14(IF_INT(zero(z0),zero(z1),z0,z1),ZERO(z0))
            INT(z0,z1) -> c15(IF_INT(zero(z0),zero(z1),z0,z1),ZERO(z1))
            INTLIST(z0) -> c10(IF_INTLIST(empty(z0),z0),EMPTY(z0))
            P(0()) -> c7()
            P(s(0())) -> c8()
            P(s(s(z0))) -> c9(P(s(z0)))
            TAIL(cons(z0,z1)) -> c3()
            TAIL(nil()) -> c2()
            ZERO(0()) -> c5()
            ZERO(s(z0)) -> c6()
        - Weak TRS:
            empty(cons(z0,z1)) -> false()
            empty(nil()) -> true()
            head(cons(z0,z1)) -> z0
            if1(false(),z0,z1) -> cons(0(),int(s(0()),z1))
            if1(true(),z0,z1) -> cons(0(),nil())
            if2(false(),z0,z1) -> intlist(int(p(z0),p(z1)))
            if2(true(),z0,z1) -> nil()
            if_int(false(),z0,z1,z2) -> if2(z0,z1,z2)
            if_int(true(),z0,z1,z2) -> if1(z0,z1,z2)
            if_intlist(false(),z0) -> cons(s(head(z0)),intlist(tail(z0)))
            if_intlist(true(),z0) -> nil()
            int(z0,z1) -> if_int(zero(z0),zero(z1),z0,z1)
            intlist(z0) -> if_intlist(empty(z0),z0)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(z0))) -> s(p(s(z0)))
            tail(cons(z0,z1)) -> z1
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(z0)) -> false()
        - Signature:
            {EMPTY/1,HEAD/1,IF1/3,IF2/3,IF_INT/4,IF_INTLIST/2,INT/2,INTLIST/1,P/1,TAIL/1,ZERO/1,empty/1,head/1,if1/3
            ,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1} / {0/0,c/0,c1/0,c10/2,c11/0,c12/1,c13/2
            ,c14/2,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c3/0,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,cons/2
            ,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {EMPTY,HEAD,IF1,IF2,IF_INT,IF_INTLIST,INT,INTLIST,P,TAIL
            ,ZERO,empty,head,if1,if2,if_int,if_intlist,int,intlist,p,tail,zero} and constructors {0,c,c1,c10,c11,c12,c13
            ,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,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)) -> c1()
            EMPTY(nil()) -> c()
            HEAD(cons(z0,z1)) -> c4()
            IF1(false(),z0,z1) -> c19(INT(s(0()),z1))
            IF1(true(),z0,z1) -> c18()
            IF2(false(),z0,z1) -> c21(INTLIST(int(p(z0),p(z1))),INT(p(z0),p(z1)),P(z0))
            IF2(false(),z0,z1) -> c22(INTLIST(int(p(z0),p(z1))),INT(p(z0),p(z1)),P(z1))
            IF2(true(),z0,z1) -> c20()
            IF_INT(false(),z0,z1,z2) -> c17(IF2(z0,z1,z2))
            IF_INT(true(),z0,z1,z2) -> c16(IF1(z0,z1,z2))
            IF_INTLIST(false(),z0) -> c12(HEAD(z0))
            IF_INTLIST(false(),z0) -> c13(INTLIST(tail(z0)),TAIL(z0))
            IF_INTLIST(true(),z0) -> c11()
            INT(z0,z1) -> c14(IF_INT(zero(z0),zero(z1),z0,z1),ZERO(z0))
            INT(z0,z1) -> c15(IF_INT(zero(z0),zero(z1),z0,z1),ZERO(z1))
            INTLIST(z0) -> c10(IF_INTLIST(empty(z0),z0),EMPTY(z0))
            P(0()) -> c7()
            P(s(0())) -> c8()
            P(s(s(z0))) -> c9(P(s(z0)))
            TAIL(cons(z0,z1)) -> c3()
            TAIL(nil()) -> c2()
            ZERO(0()) -> c5()
            ZERO(s(z0)) -> c6()
        - Weak TRS:
            empty(cons(z0,z1)) -> false()
            empty(nil()) -> true()
            head(cons(z0,z1)) -> z0
            if1(false(),z0,z1) -> cons(0(),int(s(0()),z1))
            if1(true(),z0,z1) -> cons(0(),nil())
            if2(false(),z0,z1) -> intlist(int(p(z0),p(z1)))
            if2(true(),z0,z1) -> nil()
            if_int(false(),z0,z1,z2) -> if2(z0,z1,z2)
            if_int(true(),z0,z1,z2) -> if1(z0,z1,z2)
            if_intlist(false(),z0) -> cons(s(head(z0)),intlist(tail(z0)))
            if_intlist(true(),z0) -> nil()
            int(z0,z1) -> if_int(zero(z0),zero(z1),z0,z1)
            intlist(z0) -> if_intlist(empty(z0),z0)
            p(0()) -> 0()
            p(s(0())) -> 0()
            p(s(s(z0))) -> s(p(s(z0)))
            tail(cons(z0,z1)) -> z1
            tail(nil()) -> nil()
            zero(0()) -> true()
            zero(s(z0)) -> false()
        - Signature:
            {EMPTY/1,HEAD/1,IF1/3,IF2/3,IF_INT/4,IF_INTLIST/2,INT/2,INTLIST/1,P/1,TAIL/1,ZERO/1,empty/1,head/1,if1/3
            ,if2/3,if_int/4,if_intlist/2,int/2,intlist/1,p/1,tail/1,zero/1} / {0/0,c/0,c1/0,c10/2,c11/0,c12/1,c13/2
            ,c14/2,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c3/0,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,cons/2
            ,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {EMPTY,HEAD,IF1,IF2,IF_INT,IF_INTLIST,INT,INTLIST,P,TAIL
            ,ZERO,empty,head,if1,if2,if_int,if_intlist,int,intlist,p,tail,zero} and constructors {0,c,c1,c10,c11,c12,c13
            ,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,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:
          P(s(x)){x -> s(x)} =
            P(s(s(x))) ->^+ c9(P(s(x)))
              = C[P(s(x)) = P(s(x)){}]

WORST_CASE(Omega(n^1),?)