WORST_CASE(?,O(n^1))
* Step 1: DependencyPairs WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            +Full(0(),y) -> y
            +Full(S(x),y) -> +Full(x,S(y))
            f(x) -> *(x,x)
            goal(xs) -> map(xs)
            map(Cons(x,xs)) -> Cons(f(x),map(xs))
            map(Nil()) -> Nil()
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,S(0())) -> x
            *(x,S(S(y))) -> +(x,*(x,S(y)))
            *(0(),y) -> 0()
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          +Full#(0(),y) -> c_1()
          +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
          f#(x) -> c_3(*#(x,x))
          goal#(xs) -> c_4(map#(xs))
          map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
          map#(Nil()) -> c_6()
        Weak DPs
          *#(x,0()) -> c_7()
          *#(x,S(0())) -> c_8()
          *#(x,S(S(y))) -> c_9(*#(x,S(y)))
          *#(0(),y) -> c_10()
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(0(),y) -> c_1()
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            f#(x) -> c_3(*#(x,x))
            goal#(xs) -> c_4(map#(xs))
            map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
            map#(Nil()) -> c_6()
        - Weak DPs:
            *#(x,0()) -> c_7()
            *#(x,S(0())) -> c_8()
            *#(x,S(S(y))) -> c_9(*#(x,S(y)))
            *#(0(),y) -> c_10()
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,S(0())) -> x
            *(x,S(S(y))) -> +(x,*(x,S(y)))
            *(0(),y) -> 0()
            +Full(0(),y) -> y
            +Full(S(x),y) -> +Full(x,S(y))
            f(x) -> *(x,x)
            goal(xs) -> map(xs)
            map(Cons(x,xs)) -> Cons(f(x),map(xs))
            map(Nil()) -> Nil()
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,6}
        by application of
          Pre({1,3,6}) = {2,4,5}.
        Here rules are labelled as follows:
          1: +Full#(0(),y) -> c_1()
          2: +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
          3: f#(x) -> c_3(*#(x,x))
          4: goal#(xs) -> c_4(map#(xs))
          5: map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
          6: map#(Nil()) -> c_6()
          7: *#(x,0()) -> c_7()
          8: *#(x,S(0())) -> c_8()
          9: *#(x,S(S(y))) -> c_9(*#(x,S(y)))
          10: *#(0(),y) -> c_10()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            goal#(xs) -> c_4(map#(xs))
            map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
        - Weak DPs:
            *#(x,0()) -> c_7()
            *#(x,S(0())) -> c_8()
            *#(x,S(S(y))) -> c_9(*#(x,S(y)))
            *#(0(),y) -> c_10()
            +Full#(0(),y) -> c_1()
            f#(x) -> c_3(*#(x,x))
            map#(Nil()) -> c_6()
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,S(0())) -> x
            *(x,S(S(y))) -> +(x,*(x,S(y)))
            *(0(),y) -> 0()
            +Full(0(),y) -> y
            +Full(S(x),y) -> +Full(x,S(y))
            f(x) -> *(x,x)
            goal(xs) -> map(xs)
            map(Cons(x,xs)) -> Cons(f(x),map(xs))
            map(Nil()) -> Nil()
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
             -->_1 +Full#(0(),y) -> c_1():8
             -->_1 +Full#(S(x),y) -> c_2(+Full#(x,S(y))):1
          
          2:S:goal#(xs) -> c_4(map#(xs))
             -->_1 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
             -->_1 map#(Nil()) -> c_6():10
          
          3:S:map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
             -->_1 f#(x) -> c_3(*#(x,x)):9
             -->_2 map#(Nil()) -> c_6():10
             -->_2 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
          
          4:W:*#(x,0()) -> c_7()
             
          
          5:W:*#(x,S(0())) -> c_8()
             
          
          6:W:*#(x,S(S(y))) -> c_9(*#(x,S(y)))
             -->_1 *#(0(),y) -> c_10():7
             -->_1 *#(x,S(S(y))) -> c_9(*#(x,S(y))):6
             -->_1 *#(x,S(0())) -> c_8():5
          
          7:W:*#(0(),y) -> c_10()
             
          
          8:W:+Full#(0(),y) -> c_1()
             
          
          9:W:f#(x) -> c_3(*#(x,x))
             -->_1 *#(0(),y) -> c_10():7
             -->_1 *#(x,S(S(y))) -> c_9(*#(x,S(y))):6
             -->_1 *#(x,S(0())) -> c_8():5
             -->_1 *#(x,0()) -> c_7():4
          
          10:W:map#(Nil()) -> c_6()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          10: map#(Nil()) -> c_6()
          9: f#(x) -> c_3(*#(x,x))
          4: *#(x,0()) -> c_7()
          6: *#(x,S(S(y))) -> c_9(*#(x,S(y)))
          5: *#(x,S(0())) -> c_8()
          7: *#(0(),y) -> c_10()
          8: +Full#(0(),y) -> c_1()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            goal#(xs) -> c_4(map#(xs))
            map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,S(0())) -> x
            *(x,S(S(y))) -> +(x,*(x,S(y)))
            *(0(),y) -> 0()
            +Full(0(),y) -> y
            +Full(S(x),y) -> +Full(x,S(y))
            f(x) -> *(x,x)
            goal(xs) -> map(xs)
            map(Cons(x,xs)) -> Cons(f(x),map(xs))
            map(Nil()) -> Nil()
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
             -->_1 +Full#(S(x),y) -> c_2(+Full#(x,S(y))):1
          
          2:S:goal#(xs) -> c_4(map#(xs))
             -->_1 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
          
          3:S:map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
             -->_2 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          map#(Cons(x,xs)) -> c_5(map#(xs))
* Step 5: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            goal#(xs) -> c_4(map#(xs))
            map#(Cons(x,xs)) -> c_5(map#(xs))
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,S(0())) -> x
            *(x,S(S(y))) -> +(x,*(x,S(y)))
            *(0(),y) -> 0()
            +Full(0(),y) -> y
            +Full(S(x),y) -> +Full(x,S(y))
            f(x) -> *(x,x)
            goal(xs) -> map(xs)
            map(Cons(x,xs)) -> Cons(f(x),map(xs))
            map(Nil()) -> Nil()
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
          goal#(xs) -> c_4(map#(xs))
          map#(Cons(x,xs)) -> c_5(map#(xs))
* Step 6: RemoveHeads WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            goal#(xs) -> c_4(map#(xs))
            map#(Cons(x,xs)) -> c_5(map#(xs))
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
           -->_1 +Full#(S(x),y) -> c_2(+Full#(x,S(y))):1
        
        2:S:goal#(xs) -> c_4(map#(xs))
           -->_1 map#(Cons(x,xs)) -> c_5(map#(xs)):3
        
        3:S:map#(Cons(x,xs)) -> c_5(map#(xs))
           -->_1 map#(Cons(x,xs)) -> c_5(map#(xs)):3
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(2,goal#(xs) -> c_4(map#(xs)))]
* Step 7: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            map#(Cons(x,xs)) -> c_5(map#(xs))
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_2) = {1},
            uargs(c_5) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(*) = [0]                  
                 p(+) = [1] x1 + [1] x2 + [0]
             p(+Full) = [0]                  
                 p(0) = [0]                  
              p(Cons) = [1] x1 + [1] x2 + [1]
               p(Nil) = [0]                  
                 p(S) = [1] x1 + [0]         
                 p(f) = [0]                  
              p(goal) = [0]                  
               p(map) = [0]                  
                p(*#) = [0]                  
            p(+Full#) = [0]                  
                p(f#) = [0]                  
             p(goal#) = [0]                  
              p(map#) = [9] x1 + [0]         
               p(c_1) = [0]                  
               p(c_2) = [1] x1 + [0]         
               p(c_3) = [0]                  
               p(c_4) = [0]                  
               p(c_5) = [1] x1 + [0]         
               p(c_6) = [0]                  
               p(c_7) = [0]                  
               p(c_8) = [0]                  
               p(c_9) = [0]                  
              p(c_10) = [0]                  
          
          Following rules are strictly oriented:
          map#(Cons(x,xs)) = [9] x + [9] xs + [9]
                           > [9] xs + [0]        
                           = c_5(map#(xs))       
          
          
          Following rules are (at-least) weakly oriented:
          +Full#(S(x),y) =  [0]                
                         >= [0]                
                         =  c_2(+Full#(x,S(y)))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
        - Weak DPs:
            map#(Cons(x,xs)) -> c_5(map#(xs))
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_2) = {1},
            uargs(c_5) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(*) = [0]                  
                 p(+) = [1] x1 + [1] x2 + [0]
             p(+Full) = [0]                  
                 p(0) = [1]                  
              p(Cons) = [1] x1 + [1] x2 + [0]
               p(Nil) = [0]                  
                 p(S) = [1] x1 + [3]         
                 p(f) = [0]                  
              p(goal) = [0]                  
               p(map) = [0]                  
                p(*#) = [0]                  
            p(+Full#) = [9] x1 + [0]         
                p(f#) = [0]                  
             p(goal#) = [0]                  
              p(map#) = [2] x1 + [0]         
               p(c_1) = [0]                  
               p(c_2) = [1] x1 + [0]         
               p(c_3) = [0]                  
               p(c_4) = [0]                  
               p(c_5) = [1] x1 + [0]         
               p(c_6) = [0]                  
               p(c_7) = [0]                  
               p(c_8) = [0]                  
               p(c_9) = [0]                  
              p(c_10) = [0]                  
          
          Following rules are strictly oriented:
          +Full#(S(x),y) = [9] x + [27]       
                         > [9] x + [0]        
                         = c_2(+Full#(x,S(y)))
          
          
          Following rules are (at-least) weakly oriented:
          map#(Cons(x,xs)) =  [2] x + [2] xs + [0]
                           >= [2] xs + [0]        
                           =  c_5(map#(xs))       
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
            map#(Cons(x,xs)) -> c_5(map#(xs))
        - Signature:
            {*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
            ,S}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))