tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
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(?,O(n^2))
* Step 1: Sum.  WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            APPEND(z0,z1) -> c(APPEND#1(z0,z1))
            APPEND#1(::(z0,z1),z2) -> c1(APPEND(z1,z2))
            APPEND#1(nil(),z0) -> c2()
            APPENDALL(z0) -> c3(APPENDALL#1(z0))
            APPENDALL#1(::(z0,z1)) -> c4(APPEND(z0,appendAll(z1)),APPENDALL(z1))
            APPENDALL#1(nil()) -> c5()
            APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
            APPENDALL2#1(::(z0,z1)) -> c7(APPEND(appendAll(z0),appendAll2(z1)),APPENDALL(z0))
            APPENDALL2#1(::(z0,z1)) -> c8(APPEND(appendAll(z0),appendAll2(z1)),APPENDALL2(z1))
            APPENDALL2#1(nil()) -> c9()
            APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
            APPENDALL3#1(::(z0,z1)) -> c11(APPEND(appendAll2(z0),appendAll3(z1)),APPENDALL2(z0))
            APPENDALL3#1(::(z0,z1)) -> c12(APPEND(appendAll2(z0),appendAll3(z1)),APPENDALL3(z1))
            APPENDALL3#1(nil()) -> c13()
        - Weak TRS:
            append(z0,z1) -> append#1(z0,z1)
            append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2))
            append#1(nil(),z0) -> z0
            appendAll(z0) -> appendAll#1(z0)
            appendAll#1(::(z0,z1)) -> append(z0,appendAll(z1))
            appendAll#1(nil()) -> nil()
            appendAll2(z0) -> appendAll2#1(z0)
            appendAll2#1(::(z0,z1)) -> append(appendAll(z0),appendAll2(z1))
            appendAll2#1(nil()) -> nil()
            appendAll3(z0) -> appendAll3#1(z0)
            appendAll3#1(::(z0,z1)) -> append(appendAll2(z0),appendAll3(z1))
            appendAll3#1(nil()) -> nil()
        - Signature:
            {APPEND/2,APPEND#1/2,APPENDALL/1,APPENDALL#1/1,APPENDALL2/1,APPENDALL2#1/1,APPENDALL3/1,APPENDALL3#1/1
            ,append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
            ,appendAll3#1/1} / {::/2,c/1,c1/1,c10/1,c11/2,c12/2,c13/0,c2/0,c3/1,c4/2,c5/0,c6/1,c7/2,c8/2,c9/0,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APPEND,APPEND#1,APPENDALL,APPENDALL#1,APPENDALL2
            ,APPENDALL2#1,APPENDALL3,APPENDALL3#1,append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1
            ,appendAll3,appendAll3#1} and constructors {::,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,nil}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Ara.  WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            APPEND(z0,z1) -> c(APPEND#1(z0,z1))
            APPEND#1(::(z0,z1),z2) -> c1(APPEND(z1,z2))
            APPEND#1(nil(),z0) -> c2()
            APPENDALL(z0) -> c3(APPENDALL#1(z0))
            APPENDALL#1(::(z0,z1)) -> c4(APPEND(z0,appendAll(z1)),APPENDALL(z1))
            APPENDALL#1(nil()) -> c5()
            APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
            APPENDALL2#1(::(z0,z1)) -> c7(APPEND(appendAll(z0),appendAll2(z1)),APPENDALL(z0))
            APPENDALL2#1(::(z0,z1)) -> c8(APPEND(appendAll(z0),appendAll2(z1)),APPENDALL2(z1))
            APPENDALL2#1(nil()) -> c9()
            APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
            APPENDALL3#1(::(z0,z1)) -> c11(APPEND(appendAll2(z0),appendAll3(z1)),APPENDALL2(z0))
            APPENDALL3#1(::(z0,z1)) -> c12(APPEND(appendAll2(z0),appendAll3(z1)),APPENDALL3(z1))
            APPENDALL3#1(nil()) -> c13()
        - Weak TRS:
            append(z0,z1) -> append#1(z0,z1)
            append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2))
            append#1(nil(),z0) -> z0
            appendAll(z0) -> appendAll#1(z0)
            appendAll#1(::(z0,z1)) -> append(z0,appendAll(z1))
            appendAll#1(nil()) -> nil()
            appendAll2(z0) -> appendAll2#1(z0)
            appendAll2#1(::(z0,z1)) -> append(appendAll(z0),appendAll2(z1))
            appendAll2#1(nil()) -> nil()
            appendAll3(z0) -> appendAll3#1(z0)
            appendAll3#1(::(z0,z1)) -> append(appendAll2(z0),appendAll3(z1))
            appendAll3#1(nil()) -> nil()
        - Signature:
            {APPEND/2,APPEND#1/2,APPENDALL/1,APPENDALL#1/1,APPENDALL2/1,APPENDALL2#1/1,APPENDALL3/1,APPENDALL3#1/1
            ,append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
            ,appendAll3#1/1} / {::/2,c/1,c1/1,c10/1,c11/2,c12/2,c13/0,c2/0,c3/1,c4/2,c5/0,c6/1,c7/2,c8/2,c9/0,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APPEND,APPEND#1,APPENDALL,APPENDALL#1,APPENDALL2
            ,APPENDALL2#1,APPENDALL3,APPENDALL3#1,append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1
            ,appendAll3,appendAll3#1} and constructors {::,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,nil}
    + Applied Processor:
        Ara {minDegree = 1, maxDegree = 2, araTimeout = 5, araRuleShifting = Nothing, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False}
    + Details:
        Signatures used:
        ----------------
          F (TrsFun "::") :: ["A"(2, 0) x "A"(2, 0)] -(2)-> "A"(2, 0)
          F (TrsFun "::") :: ["A"(15, 15) x "A"(15, 15)] -(15)-> "A"(0, 15)
          F (TrsFun "::") :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0)
          F (TrsFun "::") :: ["A"(14, 0) x "A"(14, 0)] -(14)-> "A"(14, 0)
          F (TrsFun "::") :: ["A"(15, 0) x "A"(15, 0)] -(15)-> "A"(15, 0)
          F (TrsFun "APPEND") :: ["A"(2, 0) x "A"(1, 0)] -(2)-> "A"(8, 1)
          F (TrsFun "APPEND#1") :: ["A"(2, 0) x "A"(1, 0)] -(1)-> "A"(10, 2)
          F (TrsFun "APPENDALL") :: ["A"(1, 15)] -(8)-> "A"(8, 5)
          F (TrsFun "APPENDALL#1") :: ["A"(0, 15)] -(3)-> "A"(10, 8)
          F (TrsFun "APPENDALL2") :: ["A"(0, 15)] -(12)-> "A"(10, 7)
          F (TrsFun "APPENDALL2#1") :: ["A"(0, 15)] -(9)-> "A"(0, 0)
          F (TrsFun "APPENDALL3") :: ["A"(0, 15)] -(12)-> "A"(7, 6)
          F (TrsFun "APPENDALL3#1") :: ["A"(0, 15)] -(11)-> "A"(7, 6)
          F (TrsFun "append") :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0)
          F (TrsFun "append#1") :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0)
          F (TrsFun "appendAll") :: ["A"(14, 0)] -(4)-> "A"(3, 0)
          F (TrsFun "appendAll#1") :: ["A"(14, 0)] -(4)-> "A"(3, 0)
          F (TrsFun "appendAll2") :: ["A"(15, 0)] -(1)-> "A"(3, 0)
          F (TrsFun "appendAll2#1") :: ["A"(15, 0)] -(1)-> "A"(3, 0)
          F (TrsFun "appendAll3") :: ["A"(15, 0)] -(0)-> "A"(3, 0)
          F (TrsFun "appendAll3#1") :: ["A"(15, 0)] -(0)-> "A"(3, 0)
          F (TrsFun "c") :: ["A"(10, 0)] -(0)-> "A"(10, 14)
          F (TrsFun "c1") :: ["A"(0, 0)] -(0)-> "A"(10, 7)
          F (TrsFun "c10") :: ["A"(7, 6)] -(0)-> "A"(7, 6)
          F (TrsFun "c11") :: ["A"(8, 0) x "A"(0, 6)] -(0)-> "A"(8, 6)
          F (TrsFun "c12") :: ["A"(0, 0) x "A"(7, 6)] -(0)-> "A"(7, 6)
          F (TrsFun "c13") :: [] -(0)-> "A"(9, 8)
          F (TrsFun "c2") :: [] -(0)-> "A"(10, 8)
          F (TrsFun "c3") :: ["A"(9, 8)] -(0)-> "A"(9, 8)
          F (TrsFun "c4") :: ["A"(0, 0) x "A"(8, 0)] -(0)-> "A"(12, 8)
          F (TrsFun "c5") :: [] -(0)-> "A"(10, 8)
          F (TrsFun "c6") :: ["A"(0, 0)] -(0)-> "A"(12, 7)
          F (TrsFun "c7") :: ["A"(2, 0) x "A"(1, 0)] -(0)-> "A"(1, 2)
          F (TrsFun "c8") :: ["A"(0, 0) x "A"(7, 1)] -(0)-> "A"(6, 1)
          F (TrsFun "c9") :: [] -(0)-> "A"(8, 8)
          F (TrsFun "nil") :: [] -(0)-> "A"(2, 0)
          F (TrsFun "nil") :: [] -(0)-> "A"(0, 15)
          F (TrsFun "nil") :: [] -(0)-> "A"(3, 0)
          F (TrsFun "nil") :: [] -(0)-> "A"(14, 0)
          F (TrsFun "nil") :: [] -(0)-> "A"(15, 0)
          F (TrsFun "nil") :: [] -(0)-> "A"(11, 8)
          F (TrsFun "nil") :: [] -(0)-> "A"(13, 8)
          F (TrsFun "nil") :: [] -(0)-> "A"(3, 8)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "F (TrsFun \"::\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0)
          "F (TrsFun \"::\")_A" :: ["A"(1, 1) x "A"(1, 1)] -(1)-> "A"(0, 1)
          "F (TrsFun \"c\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c1\")_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c1\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c10\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c10\")_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c11\")_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c11\")_A" :: ["A"(0, 0) x "A"(0, 1)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c12\")_A" :: ["A"(0, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c12\")_A" :: ["A"(0, 0) x "A"(0, 1)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c13\")_A" :: [] -(0)-> "A"(1, 0)
          "F (TrsFun \"c13\")_A" :: [] -(0)-> "A"(0, 1)
          "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(1, 0)
          "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(0, 1)
          "F (TrsFun \"c3\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c3\")_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c4\")_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c4\")_A" :: ["A"(0, 0) x "A"(1, 0)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(1, 0)
          "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(0, 1)
          "F (TrsFun \"c6\")_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c6\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c7\")_A" :: ["A"(0, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c7\")_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c8\")_A" :: ["A"(0, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
          "F (TrsFun \"c8\")_A" :: ["A"(0, 0) x "A"(1, 1)] -(0)-> "A"(0, 1)
          "F (TrsFun \"c9\")_A" :: [] -(0)-> "A"(1, 0)
          "F (TrsFun \"c9\")_A" :: [] -(0)-> "A"(0, 1)
          "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1, 0)
          "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(0, 1)
        
        

WORST_CASE(?,O(n^2))