* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(x,xs),Nil()) -> Nil()
            gcd(Cons(x',xs'),Cons(x,xs)) -> gcd[Ite](eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
            gcd(Nil(),Cons(x,xs)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            goal(x,y) -> gcd(x,y)
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            gcd[False][Ite](False(),x,y) -> gcd(x,monus(y,x))
            gcd[False][Ite](True(),x,y) -> gcd(monus(x,y),y)
            gcd[Ite](False(),x,y) -> gcd[False][Ite](gt0(x,y),x,y)
            gcd[Ite](True(),x,y) -> x
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/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} / {Cons/2
            ,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth
            ,monus,monus[Ite]} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
            @(Nil(),ys) -> ys
            eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys))
            eqList(Cons(x,xs),Nil()) -> False()
            eqList(Nil(),Cons(y,ys)) -> False()
            eqList(Nil(),Nil()) -> True()
            gcd(Cons(x,xs),Nil()) -> Nil()
            gcd(Cons(x',xs'),Cons(x,xs)) -> gcd[Ite](eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs))
            gcd(Nil(),Cons(x,xs)) -> Nil()
            gcd(Nil(),Nil()) -> Nil()
            goal(x,y) -> gcd(x,y)
            gt0(Cons(x,xs),Nil()) -> True()
            gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs)
            gt0(Nil(),y) -> False()
            lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs))
            lgth(Nil()) -> Nil()
            monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y)
        - Weak TRS:
            and(False(),False()) -> False()
            and(False(),True()) -> False()
            and(True(),False()) -> False()
            and(True(),True()) -> True()
            gcd[False][Ite](False(),x,y) -> gcd(x,monus(y,x))
            gcd[False][Ite](True(),x,y) -> gcd(monus(x,y),y)
            gcd[Ite](False(),x,y) -> gcd[False][Ite](gt0(x,y),x,y)
            gcd[Ite](True(),x,y) -> x
            monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs)
            monus[Ite](True(),Cons(x,xs),y) -> xs
        - Signature:
            {@/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} / {Cons/2
            ,False/0,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth
            ,monus,monus[Ite]} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          @(y,z){y -> Cons(x,y)} =
            @(Cons(x,y),z) ->^+ Cons(x,@(y,z))
              = C[@(y,z) = @(y,z){}]

WORST_CASE(Omega(n^1),?)