WORST_CASE(?,O(n^2))
* Step 1: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
            add0(Nil(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
            mul0(Nil(),y) -> Nil()
        - Signature:
            {add0/2,goal/2,mul0/2} / {Cons/2,Nil/0,S/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,mul0} and constructors {Cons,Nil,S}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          Cons :: [A(7) x A(7)] -(7)-> A(7)
          Cons :: [A(11) x A(11)] -(11)-> A(11)
          Nil :: [] -(0)-> A(7)
          Nil :: [] -(0)-> A(11)
          Nil :: [] -(0)-> A(13)
          S :: [] -(0)-> A(15)
          add0 :: [A(7) x A(7)] -(7)-> A(7)
          goal :: [A(13) x A(14)] -(3)-> A(0)
          mul0 :: [A(11) x A(0)] -(3)-> A(7)
        
        
        Cost-free Signatures used:
        --------------------------
          Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          Nil :: [] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          Cons_A :: [A(1) x A(1)] -(1)-> A(1)
          Nil_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
          mul0(Nil(),y) -> Nil()
        2. Weak:
          add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
          add0(Nil(),y) -> y
          goal(xs,ys) -> mul0(xs,ys)
* Step 2: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
            add0(Nil(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
        - Weak TRS:
            mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
            mul0(Nil(),y) -> Nil()
        - Signature:
            {add0/2,goal/2,mul0/2} / {Cons/2,Nil/0,S/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,mul0} and constructors {Cons,Nil,S}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          Cons :: [A(1) x A(1)] -(1)-> A(1)
          Cons :: [A(13) x A(13)] -(13)-> A(13)
          Nil :: [] -(0)-> A(1)
          Nil :: [] -(0)-> A(13)
          Nil :: [] -(0)-> A(7)
          S :: [] -(0)-> A(15)
          add0 :: [A(1) x A(1)] -(2)-> A(1)
          goal :: [A(15) x A(15)] -(9)-> A(0)
          mul0 :: [A(13) x A(1)] -(8)-> A(1)
        
        
        Cost-free Signatures used:
        --------------------------
          Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          Nil :: [] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          Cons_A :: [A(1) x A(1)] -(1)-> A(1)
          Nil_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          add0(Nil(),y) -> y
        2. Weak:
          add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
          goal(xs,ys) -> mul0(xs,ys)
* Step 3: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
            goal(xs,ys) -> mul0(xs,ys)
        - Weak TRS:
            add0(Nil(),y) -> y
            mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
            mul0(Nil(),y) -> Nil()
        - Signature:
            {add0/2,goal/2,mul0/2} / {Cons/2,Nil/0,S/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,mul0} and constructors {Cons,Nil,S}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          Cons :: [A(0) x A(0)] -(0)-> A(0)
          Cons :: [A(0) x A(0)] -(0)-> A(8)
          Nil :: [] -(0)-> A(0)
          Nil :: [] -(0)-> A(6)
          S :: [] -(0)-> A(14)
          add0 :: [A(0) x A(0)] -(0)-> A(0)
          goal :: [A(14) x A(10)] -(14)-> A(0)
          mul0 :: [A(0) x A(0)] -(1)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          Nil :: [] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          Cons_A :: [A(0) x A(0)] -(0)-> A(1)
          Nil_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          goal(xs,ys) -> mul0(xs,ys)
        2. Weak:
          add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
* Step 4: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
        - Weak TRS:
            add0(Nil(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
            mul0(Nil(),y) -> Nil()
        - Signature:
            {add0/2,goal/2,mul0/2} / {Cons/2,Nil/0,S/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,mul0} and constructors {Cons,Nil,S}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          Cons :: [A(13, 0) x A(13, 0)] -(13)-> A(13, 0)
          Cons :: [A(15, 15) x A(15, 15)] -(15)-> A(0, 15)
          Cons :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0)
          Nil :: [] -(0)-> A(13, 0)
          Nil :: [] -(0)-> A(0, 15)
          Nil :: [] -(0)-> A(7, 7)
          S :: [] -(0)-> A(7, 13)
          add0 :: [A(13, 0) x A(0, 0)] -(11)-> A(0, 0)
          goal :: [A(14, 15) x A(15, 14)] -(12)-> A(0, 0)
          mul0 :: [A(0, 15) x A(1, 0)] -(2)-> A(0, 0)
        
        
        Cost-free Signatures used:
        --------------------------
          Cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          Cons :: [A_cf(15, 0) x A_cf(15, 0)] -(15)-> A_cf(15, 0)
          Cons :: [A_cf(14, 0) x A_cf(14, 0)] -(14)-> A_cf(14, 0)
          Nil :: [] -(0)-> A_cf(0, 0)
          Nil :: [] -(0)-> A_cf(15, 0)
          Nil :: [] -(0)-> A_cf(14, 0)
          Nil :: [] -(0)-> A_cf(15, 10)
          S :: [] -(0)-> A_cf(0, 0)
          S :: [] -(0)-> A_cf(15, 11)
          add0 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          add0 :: [A_cf(14, 0) x A_cf(14, 0)] -(0)-> A_cf(14, 0)
          mul0 :: [A_cf(15, 0) x A_cf(1, 0)] -(0)-> A_cf(14, 0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          Cons_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0)
          Cons_A :: [A(1, 1) x A(1, 1)] -(1)-> A(0, 1)
          Nil_A :: [] -(0)-> A(1, 0)
          Nil_A :: [] -(0)-> A(0, 1)
          S_A :: [] -(0)-> A(1, 0)
          S_A :: [] -(0)-> A(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
        2. Weak:
          
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            add0(Cons(x,xs),y) -> add0(xs,Cons(S(),y))
            add0(Nil(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            mul0(Cons(x,xs),y) -> add0(mul0(xs,y),y)
            mul0(Nil(),y) -> Nil()
        - Signature:
            {add0/2,goal/2,mul0/2} / {Cons/2,Nil/0,S/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,mul0} and constructors {Cons,Nil,S}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))