WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum.  WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
            MAP#2(plus_x(z0),Nil()) -> c2()
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
        - Weak TRS:
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
            MAP#2(plus_x(z0),Nil()) -> c2()
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
        - Weak TRS:
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:2: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
            MAP#2(plus_x(z0),Nil()) -> c2()
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
        - Weak TRS:
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          MAP#2(plus_x(x),z){z -> Cons(y,z)} =
            MAP#2(plus_x(x),Cons(y,z)) ->^+ c4(MAP#2(plus_x(x),z))
              = C[MAP#2(plus_x(x),z) = MAP#2(plus_x(x),z){}]

** Step 1.b:1: Ara.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
            MAP#2(plus_x(z0),Nil()) -> c2()
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
        - Weak TRS:
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False}
    + Details:
        Signatures used:
        ----------------
          F (TrsFun "0") :: [] -(0)-> "A"(1)
          F (TrsFun "0") :: [] -(0)-> "A"(0)
          F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "MAIN") :: ["A"(0) x "A"(1)] -(3)-> "A"(0)
          F (TrsFun "MAP#2") :: ["A"(1) x "A"(0)] -(1)-> "A"(0)
          F (TrsFun "Nil") :: [] -(0)-> "A"(0)
          F (TrsFun "PLUS_X#1") :: ["A"(1) x "A"(0)] -(1)-> "A"(0)
          F (TrsFun "S") :: ["A"(1)] -(1)-> "A"(1)
          F (TrsFun "S") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c") :: [] -(0)-> "A"(0)
          F (TrsFun "c1") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c2") :: [] -(0)-> "A"(0)
          F (TrsFun "c3") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c4") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c5") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "main") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "map#2") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "plus_x") :: ["A"(1)] -(1)-> "A"(1)
          F (TrsFun "plus_x") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "plus_x#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
        
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
          MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
          PLUS_X#1(0(),z0) -> c()
          PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
        2. Weak:
          MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
          MAP#2(plus_x(z0),Nil()) -> c2()
        
** Step 1.b:2: Ara.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
            MAP#2(plus_x(z0),Nil()) -> c2()
        - Weak TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False}
    + Details:
        Signatures used:
        ----------------
          F (TrsFun "0") :: [] -(0)-> "A"(0)
          F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "MAIN") :: ["A"(0) x "A"(0)] -(1)-> "A"(0)
          F (TrsFun "MAP#2") :: ["A"(0) x "A"(0)] -(1)-> "A"(0)
          F (TrsFun "Nil") :: [] -(0)-> "A"(0)
          F (TrsFun "PLUS_X#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "S") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c") :: [] -(0)-> "A"(0)
          F (TrsFun "c1") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c2") :: [] -(0)-> "A"(0)
          F (TrsFun "c3") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c4") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "c5") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "main") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "map#2") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "plus_x") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "plus_x#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
        
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          MAP#2(plus_x(z0),Nil()) -> c2()
        2. Weak:
          MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
        
** Step 1.b:3: NaturalMI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
        - Weak TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            MAP#2(plus_x(z0),Nil()) -> c2()
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(S) = {1},
          uargs(c1) = {1},
          uargs(c3) = {1},
          uargs(c4) = {1},
          uargs(c5) = {1}
        
        Following symbols are considered usable:
          {MAIN,MAP#2,PLUS_X#1,main,map#2,plus_x#1}
        TcT has computed the following interpretation:
                 p(0) = [1]                  
              p(Cons) = [1] x1 + [1] x2 + [2]
              p(MAIN) = [4] x1 + [13]        
             p(MAP#2) = [4] x2 + [9]         
               p(Nil) = [1]                  
          p(PLUS_X#1) = [0]                  
                 p(S) = [1] x1 + [0]         
                 p(c) = [0]                  
                p(c1) = [1] x1 + [0]         
                p(c2) = [1]                  
                p(c3) = [1] x1 + [0]         
                p(c4) = [1] x1 + [1]         
                p(c5) = [1] x1 + [4]         
              p(main) = [8] x1 + [5] x2 + [0]
             p(map#2) = [5] x1 + [1] x2 + [0]
            p(plus_x) = [1] x1 + [0]         
          p(plus_x#1) = [1] x2 + [0]         
        
        Following rules are strictly oriented:
        MAP#2(plus_x(z0),Cons(z1,z2)) = [4] z1 + [4] z2 + [17]  
                                      > [4] z2 + [10]           
                                      = c4(MAP#2(plus_x(z0),z2))
        
        
        Following rules are (at-least) weakly oriented:
                          MAIN(z0,z1) =  [4] z0 + [13]                             
                                      >= [4] z0 + [13]                             
                                      =  c5(MAP#2(plus_x(z1),z0))                  
        
        MAP#2(plus_x(z0),Cons(z1,z2)) =  [4] z1 + [4] z2 + [17]                    
                                      >= [0]                                       
                                      =  c3(PLUS_X#1(z0,z1))                       
        
              MAP#2(plus_x(z0),Nil()) =  [13]                                      
                                      >= [1]                                       
                                      =  c2()                                      
        
                     PLUS_X#1(0(),z0) =  [0]                                       
                                      >= [0]                                       
                                      =  c()                                       
        
                   PLUS_X#1(S(z0),z1) =  [0]                                       
                                      >= [0]                                       
                                      =  c1(PLUS_X#1(z0,z1))                       
        
                          main(z0,z1) =  [8] z0 + [5] z1 + [0]                     
                                      >= [1] z0 + [5] z1 + [0]                     
                                      =  map#2(plus_x(z1),z0)                      
        
        map#2(plus_x(z0),Cons(z1,z2)) =  [5] z0 + [1] z1 + [1] z2 + [2]            
                                      >= [5] z0 + [1] z1 + [1] z2 + [2]            
                                      =  Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
        
              map#2(plus_x(z0),Nil()) =  [5] z0 + [1]                              
                                      >= [1]                                       
                                      =  Nil()                                     
        
                     plus_x#1(0(),z0) =  [1] z0 + [0]                              
                                      >= [1] z0 + [0]                              
                                      =  z0                                        
        
                   plus_x#1(S(z0),z1) =  [1] z1 + [0]                              
                                      >= [1] z1 + [0]                              
                                      =  S(plus_x#1(z0,z1))                        
        
** Step 1.b:4: EmptyProcessor.  WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            MAIN(z0,z1) -> c5(MAP#2(plus_x(z1),z0))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c3(PLUS_X#1(z0,z1))
            MAP#2(plus_x(z0),Cons(z1,z2)) -> c4(MAP#2(plus_x(z0),z2))
            MAP#2(plus_x(z0),Nil()) -> c2()
            PLUS_X#1(0(),z0) -> c()
            PLUS_X#1(S(z0),z1) -> c1(PLUS_X#1(z0,z1))
            main(z0,z1) -> map#2(plus_x(z1),z0)
            map#2(plus_x(z0),Cons(z1,z2)) -> Cons(plus_x#1(z0,z1),map#2(plus_x(z0),z2))
            map#2(plus_x(z0),Nil()) -> Nil()
            plus_x#1(0(),z0) -> z0
            plus_x#1(S(z0),z1) -> S(plus_x#1(z0,z1))
        - Signature:
            {MAIN/2,MAP#2/2,PLUS_X#1/2,main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/1,c2/0,c3/1,c4/1,c5/1
            ,plus_x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,PLUS_X#1,main,map#2
            ,plus_x#1} and constructors {0,Cons,Nil,S,c,c1,c2,c3,c4,c5,plus_x}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))