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:
            @'(Cons(z0,z1),z2) -> c10(@'(z1,z2))
            @'(Nil(),z0) -> c11()
            EQLIST(Cons(z0,z1),Cons(z2,z3)) -> c21(AND(eqList(z0,z2),eqList(z1,z3)),EQLIST(z0,z2))
            EQLIST(Cons(z0,z1),Cons(z2,z3)) -> c22(AND(eqList(z0,z2),eqList(z1,z3)),EQLIST(z1,z3))
            EQLIST(Cons(z0,z1),Nil()) -> c23()
            EQLIST(Nil(),Cons(z0,z1)) -> c24()
            EQLIST(Nil(),Nil()) -> c25()
            GCD(Cons(z0,z1),Cons(z2,z3)) -> c18(GCD[ITE](eqList(Cons(z0,z1),Cons(z2,z3)),Cons(z0,z1),Cons(z2,z3))
                                               ,EQLIST(Cons(z0,z1),Cons(z2,z3)))
            GCD(Cons(z0,z1),Nil()) -> c17()
            GCD(Nil(),Cons(z0,z1)) -> c16()
            GCD(Nil(),Nil()) -> c15()
            GOAL(z0,z1) -> c27(GCD(z0,z1))
            GT0(Cons(z0,z1),Cons(z2,z3)) -> c13(GT0(z1,z3))
            GT0(Cons(z0,z1),Nil()) -> c12()
            GT0(Nil(),z0) -> c14()
            LGTH(Cons(z0,z1)) -> c19(@'(Cons(Nil(),Nil()),lgth(z1)),LGTH(z1))
            LGTH(Nil()) -> c20()
            MONUS(z0,z1) -> c26(MONUS[ITE](eqList(lgth(z1),Cons(Nil(),Nil())),z0,z1)
                               ,EQLIST(lgth(z1),Cons(Nil(),Nil()))
                               ,LGTH(z1))
        - Weak TRS:
            @(Cons(z0,z1),z2) -> Cons(z0,@(z1,z2))
            @(Nil(),z0) -> z0
            AND(False(),False()) -> c()
            AND(False(),True()) -> c2()
            AND(True(),False()) -> c1()
            AND(True(),True()) -> c3()
            GCD[FALSE][ITE](False(),z0,z1) -> c8(GCD(z0,monus(z1,z0)),MONUS(z1,z0))
            GCD[FALSE][ITE](True(),z0,z1) -> c9(GCD(monus(z0,z1),z1),MONUS(z0,z1))
            GCD[ITE](False(),z0,z1) -> c6(GCD[FALSE][ITE](gt0(z0,z1),z0,z1),GT0(z0,z1))
            GCD[ITE](True(),z0,z1) -> c7()
            MONUS[ITE](False(),Cons(z0,z1),Cons(z2,z3)) -> c4(MONUS(z1,z3))
            MONUS[ITE](True(),Cons(z0,z1),z2) -> c5()
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(z0,z1),Cons(z2,z3)) -> and(eqList(z0,z2),eqList(z1,z3))
            eqList(Cons(z0,z1),Nil()) -> False()
            eqList(Nil(),Cons(z0,z1)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(z0,z1),Cons(z2,z3)) -> gcd[Ite](eqList(Cons(z0,z1),Cons(z2,z3)),Cons(z0,z1),Cons(z2,z3))
            gcd(Cons(z0,z1),Nil()) -> Nil()
            gcd(Nil(),Cons(z0,z1)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            gcd[False][Ite](False(),z0,z1) -> gcd(z0,monus(z1,z0))
            gcd[False][Ite](True(),z0,z1) -> gcd(monus(z0,z1),z1)
            gcd[Ite](False(),z0,z1) -> gcd[False][Ite](gt0(z0,z1),z0,z1)
            gcd[Ite](True(),z0,z1) -> z0
            goal(z0,z1) -> gcd(z0,z1)
            gt0(Cons(z0,z1),Cons(z2,z3)) -> gt0(z1,z3)
            gt0(Cons(z0,z1),Nil()) -> True()
            gt0(Nil(),z0) -> False()
            lgth(Cons(z0,z1)) -> @(Cons(Nil(),Nil()),lgth(z1))
            lgth(Nil()) -> Nil()
            monus(z0,z1) -> monus[Ite](eqList(lgth(z1),Cons(Nil(),Nil())),z0,z1)
            monus[Ite](False(),Cons(z0,z1),Cons(z2,z3)) -> monus(z1,z3)
            monus[Ite](True(),Cons(z0,z1),z2) -> z1
        - Signature:
            {@/2,@'/2,AND/2,EQLIST/2,GCD/2,GCD[FALSE][ITE]/3,GCD[ITE]/3,GOAL/2,GT0/2,LGTH/1,MONUS/2,MONUS[ITE]/3,and/2
            ,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3} / {Cons/2,False/0
            ,Nil/0,True/0,c/0,c1/0,c10/1,c11/0,c12/0,c13/1,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0,c21/2,c22/2
            ,c23/0,c24/0,c25/0,c26/3,c27/1,c3/0,c4/1,c5/0,c6/2,c7/0,c8/2,c9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,@',AND,EQLIST,GCD,GCD[FALSE][ITE],GCD[ITE],GOAL,GT0
            ,LGTH,MONUS,MONUS[ITE],and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth,monus
            ,monus[Ite]} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21
            ,c22,c23,c24,c25,c26,c27,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:
            @'(Cons(z0,z1),z2) -> c10(@'(z1,z2))
            @'(Nil(),z0) -> c11()
            EQLIST(Cons(z0,z1),Cons(z2,z3)) -> c21(AND(eqList(z0,z2),eqList(z1,z3)),EQLIST(z0,z2))
            EQLIST(Cons(z0,z1),Cons(z2,z3)) -> c22(AND(eqList(z0,z2),eqList(z1,z3)),EQLIST(z1,z3))
            EQLIST(Cons(z0,z1),Nil()) -> c23()
            EQLIST(Nil(),Cons(z0,z1)) -> c24()
            EQLIST(Nil(),Nil()) -> c25()
            GCD(Cons(z0,z1),Cons(z2,z3)) -> c18(GCD[ITE](eqList(Cons(z0,z1),Cons(z2,z3)),Cons(z0,z1),Cons(z2,z3))
                                               ,EQLIST(Cons(z0,z1),Cons(z2,z3)))
            GCD(Cons(z0,z1),Nil()) -> c17()
            GCD(Nil(),Cons(z0,z1)) -> c16()
            GCD(Nil(),Nil()) -> c15()
            GOAL(z0,z1) -> c27(GCD(z0,z1))
            GT0(Cons(z0,z1),Cons(z2,z3)) -> c13(GT0(z1,z3))
            GT0(Cons(z0,z1),Nil()) -> c12()
            GT0(Nil(),z0) -> c14()
            LGTH(Cons(z0,z1)) -> c19(@'(Cons(Nil(),Nil()),lgth(z1)),LGTH(z1))
            LGTH(Nil()) -> c20()
            MONUS(z0,z1) -> c26(MONUS[ITE](eqList(lgth(z1),Cons(Nil(),Nil())),z0,z1)
                               ,EQLIST(lgth(z1),Cons(Nil(),Nil()))
                               ,LGTH(z1))
        - Weak TRS:
            @(Cons(z0,z1),z2) -> Cons(z0,@(z1,z2))
            @(Nil(),z0) -> z0
            AND(False(),False()) -> c()
            AND(False(),True()) -> c2()
            AND(True(),False()) -> c1()
            AND(True(),True()) -> c3()
            GCD[FALSE][ITE](False(),z0,z1) -> c8(GCD(z0,monus(z1,z0)),MONUS(z1,z0))
            GCD[FALSE][ITE](True(),z0,z1) -> c9(GCD(monus(z0,z1),z1),MONUS(z0,z1))
            GCD[ITE](False(),z0,z1) -> c6(GCD[FALSE][ITE](gt0(z0,z1),z0,z1),GT0(z0,z1))
            GCD[ITE](True(),z0,z1) -> c7()
            MONUS[ITE](False(),Cons(z0,z1),Cons(z2,z3)) -> c4(MONUS(z1,z3))
            MONUS[ITE](True(),Cons(z0,z1),z2) -> c5()
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(z0,z1),Cons(z2,z3)) -> and(eqList(z0,z2),eqList(z1,z3))
            eqList(Cons(z0,z1),Nil()) -> False()
            eqList(Nil(),Cons(z0,z1)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(z0,z1),Cons(z2,z3)) -> gcd[Ite](eqList(Cons(z0,z1),Cons(z2,z3)),Cons(z0,z1),Cons(z2,z3))
            gcd(Cons(z0,z1),Nil()) -> Nil()
            gcd(Nil(),Cons(z0,z1)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            gcd[False][Ite](False(),z0,z1) -> gcd(z0,monus(z1,z0))
            gcd[False][Ite](True(),z0,z1) -> gcd(monus(z0,z1),z1)
            gcd[Ite](False(),z0,z1) -> gcd[False][Ite](gt0(z0,z1),z0,z1)
            gcd[Ite](True(),z0,z1) -> z0
            goal(z0,z1) -> gcd(z0,z1)
            gt0(Cons(z0,z1),Cons(z2,z3)) -> gt0(z1,z3)
            gt0(Cons(z0,z1),Nil()) -> True()
            gt0(Nil(),z0) -> False()
            lgth(Cons(z0,z1)) -> @(Cons(Nil(),Nil()),lgth(z1))
            lgth(Nil()) -> Nil()
            monus(z0,z1) -> monus[Ite](eqList(lgth(z1),Cons(Nil(),Nil())),z0,z1)
            monus[Ite](False(),Cons(z0,z1),Cons(z2,z3)) -> monus(z1,z3)
            monus[Ite](True(),Cons(z0,z1),z2) -> z1
        - Signature:
            {@/2,@'/2,AND/2,EQLIST/2,GCD/2,GCD[FALSE][ITE]/3,GCD[ITE]/3,GOAL/2,GT0/2,LGTH/1,MONUS/2,MONUS[ITE]/3,and/2
            ,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3} / {Cons/2,False/0
            ,Nil/0,True/0,c/0,c1/0,c10/1,c11/0,c12/0,c13/1,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0,c21/2,c22/2
            ,c23/0,c24/0,c25/0,c26/3,c27/1,c3/0,c4/1,c5/0,c6/2,c7/0,c8/2,c9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,@',AND,EQLIST,GCD,GCD[FALSE][ITE],GCD[ITE],GOAL,GT0
            ,LGTH,MONUS,MONUS[ITE],and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth,monus
            ,monus[Ite]} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21
            ,c22,c23,c24,c25,c26,c27,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:
            @'(Cons(z0,z1),z2) -> c10(@'(z1,z2))
            @'(Nil(),z0) -> c11()
            EQLIST(Cons(z0,z1),Cons(z2,z3)) -> c21(AND(eqList(z0,z2),eqList(z1,z3)),EQLIST(z0,z2))
            EQLIST(Cons(z0,z1),Cons(z2,z3)) -> c22(AND(eqList(z0,z2),eqList(z1,z3)),EQLIST(z1,z3))
            EQLIST(Cons(z0,z1),Nil()) -> c23()
            EQLIST(Nil(),Cons(z0,z1)) -> c24()
            EQLIST(Nil(),Nil()) -> c25()
            GCD(Cons(z0,z1),Cons(z2,z3)) -> c18(GCD[ITE](eqList(Cons(z0,z1),Cons(z2,z3)),Cons(z0,z1),Cons(z2,z3))
                                               ,EQLIST(Cons(z0,z1),Cons(z2,z3)))
            GCD(Cons(z0,z1),Nil()) -> c17()
            GCD(Nil(),Cons(z0,z1)) -> c16()
            GCD(Nil(),Nil()) -> c15()
            GOAL(z0,z1) -> c27(GCD(z0,z1))
            GT0(Cons(z0,z1),Cons(z2,z3)) -> c13(GT0(z1,z3))
            GT0(Cons(z0,z1),Nil()) -> c12()
            GT0(Nil(),z0) -> c14()
            LGTH(Cons(z0,z1)) -> c19(@'(Cons(Nil(),Nil()),lgth(z1)),LGTH(z1))
            LGTH(Nil()) -> c20()
            MONUS(z0,z1) -> c26(MONUS[ITE](eqList(lgth(z1),Cons(Nil(),Nil())),z0,z1)
                               ,EQLIST(lgth(z1),Cons(Nil(),Nil()))
                               ,LGTH(z1))
        - Weak TRS:
            @(Cons(z0,z1),z2) -> Cons(z0,@(z1,z2))
            @(Nil(),z0) -> z0
            AND(False(),False()) -> c()
            AND(False(),True()) -> c2()
            AND(True(),False()) -> c1()
            AND(True(),True()) -> c3()
            GCD[FALSE][ITE](False(),z0,z1) -> c8(GCD(z0,monus(z1,z0)),MONUS(z1,z0))
            GCD[FALSE][ITE](True(),z0,z1) -> c9(GCD(monus(z0,z1),z1),MONUS(z0,z1))
            GCD[ITE](False(),z0,z1) -> c6(GCD[FALSE][ITE](gt0(z0,z1),z0,z1),GT0(z0,z1))
            GCD[ITE](True(),z0,z1) -> c7()
            MONUS[ITE](False(),Cons(z0,z1),Cons(z2,z3)) -> c4(MONUS(z1,z3))
            MONUS[ITE](True(),Cons(z0,z1),z2) -> c5()
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            eqList(Cons(z0,z1),Cons(z2,z3)) -> and(eqList(z0,z2),eqList(z1,z3))
            eqList(Cons(z0,z1),Nil()) -> False()
            eqList(Nil(),Cons(z0,z1)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(z0,z1),Cons(z2,z3)) -> gcd[Ite](eqList(Cons(z0,z1),Cons(z2,z3)),Cons(z0,z1),Cons(z2,z3))
            gcd(Cons(z0,z1),Nil()) -> Nil()
            gcd(Nil(),Cons(z0,z1)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            gcd[False][Ite](False(),z0,z1) -> gcd(z0,monus(z1,z0))
            gcd[False][Ite](True(),z0,z1) -> gcd(monus(z0,z1),z1)
            gcd[Ite](False(),z0,z1) -> gcd[False][Ite](gt0(z0,z1),z0,z1)
            gcd[Ite](True(),z0,z1) -> z0
            goal(z0,z1) -> gcd(z0,z1)
            gt0(Cons(z0,z1),Cons(z2,z3)) -> gt0(z1,z3)
            gt0(Cons(z0,z1),Nil()) -> True()
            gt0(Nil(),z0) -> False()
            lgth(Cons(z0,z1)) -> @(Cons(Nil(),Nil()),lgth(z1))
            lgth(Nil()) -> Nil()
            monus(z0,z1) -> monus[Ite](eqList(lgth(z1),Cons(Nil(),Nil())),z0,z1)
            monus[Ite](False(),Cons(z0,z1),Cons(z2,z3)) -> monus(z1,z3)
            monus[Ite](True(),Cons(z0,z1),z2) -> z1
        - Signature:
            {@/2,@'/2,AND/2,EQLIST/2,GCD/2,GCD[FALSE][ITE]/3,GCD[ITE]/3,GOAL/2,GT0/2,LGTH/1,MONUS/2,MONUS[ITE]/3,and/2
            ,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3} / {Cons/2,False/0
            ,Nil/0,True/0,c/0,c1/0,c10/1,c11/0,c12/0,c13/1,c14/0,c15/0,c16/0,c17/0,c18/2,c19/2,c2/0,c20/0,c21/2,c22/2
            ,c23/0,c24/0,c25/0,c26/3,c27/1,c3/0,c4/1,c5/0,c6/2,c7/0,c8/2,c9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,@',AND,EQLIST,GCD,GCD[FALSE][ITE],GCD[ITE],GOAL,GT0
            ,LGTH,MONUS,MONUS[ITE],and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth,monus
            ,monus[Ite]} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21
            ,c22,c23,c24,c25,c26,c27,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          @'(y,z){y -> Cons(x,y)} =
            @'(Cons(x,y),z) ->^+ c10(@'(y,z))
              = C[@'(y,z) = @'(y,z){}]

WORST_CASE(Omega(n^1),?)