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:
            GOAL(z0) -> c16(MERGESORT(z0))
            MERGE(Cons(z0,z1),Cons(z2,z3)) -> c8(MERGE[ITE](<=(z0,z2),Cons(z0,z1),Cons(z2,z3)),<='(z0,z2))
            MERGE(Cons(z0,z1),Nil()) -> c9()
            MERGE(Nil(),z0) -> c10()
            MERGESORT(Cons(z0,Cons(z1,z2))) -> c5(SPLITMERGE(Cons(z0,Cons(z1,z2)),Nil(),Nil()))
            MERGESORT(Cons(z0,Nil())) -> c6()
            MERGESORT(Nil()) -> c7()
            NOTEMPTY(Cons(z0,z1)) -> c14()
            NOTEMPTY(Nil()) -> c15()
            SPLITMERGE(Cons(z0,z1),z2,z3) -> c11(SPLITMERGE(z1,Cons(z0,z3),z2))
            SPLITMERGE(Nil(),z0,z1) -> c12(MERGE(mergesort(z0),mergesort(z1)),MERGESORT(z0))
            SPLITMERGE(Nil(),z0,z1) -> c13(MERGE(mergesort(z0),mergesort(z1)),MERGESORT(z1))
        - Weak TRS:
            <=(0(),z0) -> True()
            <=(S(z0),0()) -> False()
            <=(S(z0),S(z1)) -> <=(z0,z1)
            <='(0(),z0) -> c1()
            <='(S(z0),0()) -> c2()
            <='(S(z0),S(z1)) -> c(<='(z0,z1))
            MERGE[ITE](False(),z0,Cons(z1,z2)) -> c3(MERGE(z0,z2))
            MERGE[ITE](True(),Cons(z0,z1),z2) -> c4(MERGE(z1,z2))
            goal(z0) -> mergesort(z0)
            merge(Cons(z0,z1),Cons(z2,z3)) -> merge[Ite](<=(z0,z2),Cons(z0,z1),Cons(z2,z3))
            merge(Cons(z0,z1),Nil()) -> Cons(z0,z1)
            merge(Nil(),z0) -> z0
            merge[Ite](False(),z0,Cons(z1,z2)) -> Cons(z1,merge(z0,z2))
            merge[Ite](True(),Cons(z0,z1),z2) -> Cons(z0,merge(z1,z2))
            mergesort(Cons(z0,Cons(z1,z2))) -> splitmerge(Cons(z0,Cons(z1,z2)),Nil(),Nil())
            mergesort(Cons(z0,Nil())) -> Cons(z0,Nil())
            mergesort(Nil()) -> Nil()
            notEmpty(Cons(z0,z1)) -> True()
            notEmpty(Nil()) -> False()
            splitmerge(Cons(z0,z1),z2,z3) -> splitmerge(z1,Cons(z0,z3),z2)
            splitmerge(Nil(),z0,z1) -> merge(mergesort(z0),mergesort(z1))
        - Signature:
            {<=/2,<='/2,GOAL/1,MERGE/2,MERGESORT/1,MERGE[ITE]/3,NOTEMPTY/1,SPLITMERGE/3,goal/1,merge/2,merge[Ite]/3
            ,mergesort/1,notEmpty/1,splitmerge/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/0,c11/1,c12/2
            ,c13/2,c14/0,c15/0,c16/1,c2/0,c3/1,c4/1,c5/1,c6/0,c7/0,c8/2,c9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=,<=',GOAL,MERGE,MERGESORT,MERGE[ITE],NOTEMPTY
            ,SPLITMERGE,goal,merge,merge[Ite],mergesort,notEmpty,splitmerge} and constructors {0,Cons,False,Nil,S,True,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            GOAL(z0) -> c16(MERGESORT(z0))
            MERGE(Cons(z0,z1),Cons(z2,z3)) -> c8(MERGE[ITE](<=(z0,z2),Cons(z0,z1),Cons(z2,z3)),<='(z0,z2))
            MERGE(Cons(z0,z1),Nil()) -> c9()
            MERGE(Nil(),z0) -> c10()
            MERGESORT(Cons(z0,Cons(z1,z2))) -> c5(SPLITMERGE(Cons(z0,Cons(z1,z2)),Nil(),Nil()))
            MERGESORT(Cons(z0,Nil())) -> c6()
            MERGESORT(Nil()) -> c7()
            NOTEMPTY(Cons(z0,z1)) -> c14()
            NOTEMPTY(Nil()) -> c15()
            SPLITMERGE(Cons(z0,z1),z2,z3) -> c11(SPLITMERGE(z1,Cons(z0,z3),z2))
            SPLITMERGE(Nil(),z0,z1) -> c12(MERGE(mergesort(z0),mergesort(z1)),MERGESORT(z0))
            SPLITMERGE(Nil(),z0,z1) -> c13(MERGE(mergesort(z0),mergesort(z1)),MERGESORT(z1))
        - Weak TRS:
            <=(0(),z0) -> True()
            <=(S(z0),0()) -> False()
            <=(S(z0),S(z1)) -> <=(z0,z1)
            <='(0(),z0) -> c1()
            <='(S(z0),0()) -> c2()
            <='(S(z0),S(z1)) -> c(<='(z0,z1))
            MERGE[ITE](False(),z0,Cons(z1,z2)) -> c3(MERGE(z0,z2))
            MERGE[ITE](True(),Cons(z0,z1),z2) -> c4(MERGE(z1,z2))
            goal(z0) -> mergesort(z0)
            merge(Cons(z0,z1),Cons(z2,z3)) -> merge[Ite](<=(z0,z2),Cons(z0,z1),Cons(z2,z3))
            merge(Cons(z0,z1),Nil()) -> Cons(z0,z1)
            merge(Nil(),z0) -> z0
            merge[Ite](False(),z0,Cons(z1,z2)) -> Cons(z1,merge(z0,z2))
            merge[Ite](True(),Cons(z0,z1),z2) -> Cons(z0,merge(z1,z2))
            mergesort(Cons(z0,Cons(z1,z2))) -> splitmerge(Cons(z0,Cons(z1,z2)),Nil(),Nil())
            mergesort(Cons(z0,Nil())) -> Cons(z0,Nil())
            mergesort(Nil()) -> Nil()
            notEmpty(Cons(z0,z1)) -> True()
            notEmpty(Nil()) -> False()
            splitmerge(Cons(z0,z1),z2,z3) -> splitmerge(z1,Cons(z0,z3),z2)
            splitmerge(Nil(),z0,z1) -> merge(mergesort(z0),mergesort(z1))
        - Signature:
            {<=/2,<='/2,GOAL/1,MERGE/2,MERGESORT/1,MERGE[ITE]/3,NOTEMPTY/1,SPLITMERGE/3,goal/1,merge/2,merge[Ite]/3
            ,mergesort/1,notEmpty/1,splitmerge/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/0,c11/1,c12/2
            ,c13/2,c14/0,c15/0,c16/1,c2/0,c3/1,c4/1,c5/1,c6/0,c7/0,c8/2,c9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=,<=',GOAL,MERGE,MERGESORT,MERGE[ITE],NOTEMPTY
            ,SPLITMERGE,goal,merge,merge[Ite],mergesort,notEmpty,splitmerge} and constructors {0,Cons,False,Nil,S,True,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            GOAL(z0) -> c16(MERGESORT(z0))
            MERGE(Cons(z0,z1),Cons(z2,z3)) -> c8(MERGE[ITE](<=(z0,z2),Cons(z0,z1),Cons(z2,z3)),<='(z0,z2))
            MERGE(Cons(z0,z1),Nil()) -> c9()
            MERGE(Nil(),z0) -> c10()
            MERGESORT(Cons(z0,Cons(z1,z2))) -> c5(SPLITMERGE(Cons(z0,Cons(z1,z2)),Nil(),Nil()))
            MERGESORT(Cons(z0,Nil())) -> c6()
            MERGESORT(Nil()) -> c7()
            NOTEMPTY(Cons(z0,z1)) -> c14()
            NOTEMPTY(Nil()) -> c15()
            SPLITMERGE(Cons(z0,z1),z2,z3) -> c11(SPLITMERGE(z1,Cons(z0,z3),z2))
            SPLITMERGE(Nil(),z0,z1) -> c12(MERGE(mergesort(z0),mergesort(z1)),MERGESORT(z0))
            SPLITMERGE(Nil(),z0,z1) -> c13(MERGE(mergesort(z0),mergesort(z1)),MERGESORT(z1))
        - Weak TRS:
            <=(0(),z0) -> True()
            <=(S(z0),0()) -> False()
            <=(S(z0),S(z1)) -> <=(z0,z1)
            <='(0(),z0) -> c1()
            <='(S(z0),0()) -> c2()
            <='(S(z0),S(z1)) -> c(<='(z0,z1))
            MERGE[ITE](False(),z0,Cons(z1,z2)) -> c3(MERGE(z0,z2))
            MERGE[ITE](True(),Cons(z0,z1),z2) -> c4(MERGE(z1,z2))
            goal(z0) -> mergesort(z0)
            merge(Cons(z0,z1),Cons(z2,z3)) -> merge[Ite](<=(z0,z2),Cons(z0,z1),Cons(z2,z3))
            merge(Cons(z0,z1),Nil()) -> Cons(z0,z1)
            merge(Nil(),z0) -> z0
            merge[Ite](False(),z0,Cons(z1,z2)) -> Cons(z1,merge(z0,z2))
            merge[Ite](True(),Cons(z0,z1),z2) -> Cons(z0,merge(z1,z2))
            mergesort(Cons(z0,Cons(z1,z2))) -> splitmerge(Cons(z0,Cons(z1,z2)),Nil(),Nil())
            mergesort(Cons(z0,Nil())) -> Cons(z0,Nil())
            mergesort(Nil()) -> Nil()
            notEmpty(Cons(z0,z1)) -> True()
            notEmpty(Nil()) -> False()
            splitmerge(Cons(z0,z1),z2,z3) -> splitmerge(z1,Cons(z0,z3),z2)
            splitmerge(Nil(),z0,z1) -> merge(mergesort(z0),mergesort(z1))
        - Signature:
            {<=/2,<='/2,GOAL/1,MERGE/2,MERGESORT/1,MERGE[ITE]/3,NOTEMPTY/1,SPLITMERGE/3,goal/1,merge/2,merge[Ite]/3
            ,mergesort/1,notEmpty/1,splitmerge/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/0,c11/1,c12/2
            ,c13/2,c14/0,c15/0,c16/1,c2/0,c3/1,c4/1,c5/1,c6/0,c7/0,c8/2,c9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=,<=',GOAL,MERGE,MERGESORT,MERGE[ITE],NOTEMPTY
            ,SPLITMERGE,goal,merge,merge[Ite],mergesort,notEmpty,splitmerge} and constructors {0,Cons,False,Nil,S,True,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          SPLITMERGE(y,z,u){y -> Cons(x,y)} =
            SPLITMERGE(Cons(x,y),z,u) ->^+ c11(SPLITMERGE(y,Cons(x,u),z))
              = C[SPLITMERGE(y,Cons(x,u),z) = SPLITMERGE(y,z,u){z -> Cons(x,u),u -> z}]

WORST_CASE(Omega(n^1),?)