*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        +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 DP Rules:
        
      Weak TRS Rules:
        *(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
        basic terms: {*,+Full,f,goal,map}/{+,0,Cons,Nil,S}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {2},
          uargs(Cons) = {1,2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(*) = [12] x1 + [3]        
              p(+) = [1] x2 + [0]         
          p(+Full) = [3] x2 + [0]         
              p(0) = [0]                  
           p(Cons) = [1] x1 + [1] x2 + [0]
            p(Nil) = [0]                  
              p(S) = [8]                  
              p(f) = [12] x1 + [1]        
           p(goal) = [13] x1 + [1]        
            p(map) = [13] x1 + [12]       
        
        Following rules are strictly oriented:
        map(Nil()) = [12] 
                   > [0]  
                   = Nil()
        
        
        Following rules are (at-least) weakly oriented:
               *(x,0()) =  [12] x + [3]           
                        >= [0]                    
                        =  0()                    
        
            *(x,S(0())) =  [12] x + [3]           
                        >= [1] x + [0]            
                        =  x                      
        
           *(x,S(S(y))) =  [12] x + [3]           
                        >= [12] x + [3]           
                        =  +(x,*(x,S(y)))         
        
               *(0(),y) =  [3]                    
                        >= [0]                    
                        =  0()                    
        
           +Full(0(),y) =  [3] y + [0]            
                        >= [1] y + [0]            
                        =  y                      
        
          +Full(S(x),y) =  [3] y + [0]            
                        >= [24]                   
                        =  +Full(x,S(y))          
        
                   f(x) =  [12] x + [1]           
                        >= [12] x + [3]           
                        =  *(x,x)                 
        
               goal(xs) =  [13] xs + [1]          
                        >= [13] xs + [12]         
                        =  map(xs)                
        
        map(Cons(x,xs)) =  [13] x + [13] xs + [12]
                        >= [12] x + [13] xs + [13]
                        =  Cons(f(x),map(xs))     
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        +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))
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,0()) -> 0()
        *(x,S(0())) -> x
        *(x,S(S(y))) -> +(x,*(x,S(y)))
        *(0(),y) -> 0()
        map(Nil()) -> Nil()
      Signature:
        {*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
      Obligation:
        Innermost
        basic terms: {*,+Full,f,goal,map}/{+,0,Cons,Nil,S}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {2},
          uargs(Cons) = {1,2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(*) = [2] x1 + [12]        
              p(+) = [1] x2 + [0]         
          p(+Full) = [8] x2 + [1]         
              p(0) = [4]                  
           p(Cons) = [1] x1 + [1] x2 + [3]
            p(Nil) = [4]                  
              p(S) = [0]                  
              p(f) = [2] x1 + [4]         
           p(goal) = [7] x1 + [0]         
            p(map) = [7] x1 + [2]         
        
        Following rules are strictly oriented:
           +Full(0(),y) = [8] y + [1]          
                        > [1] y + [0]          
                        = y                    
        
        map(Cons(x,xs)) = [7] x + [7] xs + [23]
                        > [2] x + [7] xs + [9] 
                        = Cons(f(x),map(xs))   
        
        
        Following rules are (at-least) weakly oriented:
             *(x,0()) =  [2] x + [12]  
                      >= [4]           
                      =  0()           
        
          *(x,S(0())) =  [2] x + [12]  
                      >= [1] x + [0]   
                      =  x             
        
         *(x,S(S(y))) =  [2] x + [12]  
                      >= [2] x + [12]  
                      =  +(x,*(x,S(y)))
        
             *(0(),y) =  [20]          
                      >= [4]           
                      =  0()           
        
        +Full(S(x),y) =  [8] y + [1]   
                      >= [1]           
                      =  +Full(x,S(y)) 
        
                 f(x) =  [2] x + [4]   
                      >= [2] x + [12]  
                      =  *(x,x)        
        
             goal(xs) =  [7] xs + [0]  
                      >= [7] xs + [2]  
                      =  map(xs)       
        
           map(Nil()) =  [30]          
                      >= [4]           
                      =  Nil()         
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        +Full(S(x),y) -> +Full(x,S(y))
        f(x) -> *(x,x)
        goal(xs) -> map(xs)
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,0()) -> 0()
        *(x,S(0())) -> x
        *(x,S(S(y))) -> +(x,*(x,S(y)))
        *(0(),y) -> 0()
        +Full(0(),y) -> y
        map(Cons(x,xs)) -> Cons(f(x),map(xs))
        map(Nil()) -> Nil()
      Signature:
        {*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
      Obligation:
        Innermost
        basic terms: {*,+Full,f,goal,map}/{+,0,Cons,Nil,S}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {2},
          uargs(Cons) = {1,2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(*) = [1] x1 + [0]         
              p(+) = [1] x2 + [0]         
          p(+Full) = [8] x1 + [1] x2 + [5]
              p(0) = [0]                  
           p(Cons) = [1] x1 + [1] x2 + [0]
            p(Nil) = [1]                  
              p(S) = [1] x1 + [0]         
              p(f) = [2] x1 + [0]         
           p(goal) = [4] x1 + [10]        
            p(map) = [4] x1 + [1]         
        
        Following rules are strictly oriented:
        goal(xs) = [4] xs + [10]
                 > [4] xs + [1] 
                 = map(xs)      
        
        
        Following rules are (at-least) weakly oriented:
               *(x,0()) =  [1] x + [0]         
                        >= [0]                 
                        =  0()                 
        
            *(x,S(0())) =  [1] x + [0]         
                        >= [1] x + [0]         
                        =  x                   
        
           *(x,S(S(y))) =  [1] x + [0]         
                        >= [1] x + [0]         
                        =  +(x,*(x,S(y)))      
        
               *(0(),y) =  [0]                 
                        >= [0]                 
                        =  0()                 
        
           +Full(0(),y) =  [1] y + [5]         
                        >= [1] y + [0]         
                        =  y                   
        
          +Full(S(x),y) =  [8] x + [1] y + [5] 
                        >= [8] x + [1] y + [5] 
                        =  +Full(x,S(y))       
        
                   f(x) =  [2] x + [0]         
                        >= [1] x + [0]         
                        =  *(x,x)              
        
        map(Cons(x,xs)) =  [4] x + [4] xs + [1]
                        >= [2] x + [4] xs + [1]
                        =  Cons(f(x),map(xs))  
        
             map(Nil()) =  [5]                 
                        >= [1]                 
                        =  Nil()               
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        +Full(S(x),y) -> +Full(x,S(y))
        f(x) -> *(x,x)
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,0()) -> 0()
        *(x,S(0())) -> x
        *(x,S(S(y))) -> +(x,*(x,S(y)))
        *(0(),y) -> 0()
        +Full(0(),y) -> y
        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,0/0,Cons/2,Nil/0,S/1}
      Obligation:
        Innermost
        basic terms: {*,+Full,f,goal,map}/{+,0,Cons,Nil,S}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {2},
          uargs(Cons) = {1,2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(*) = [1] x1 + [2] x2 + [0]
              p(+) = [1] x2 + [8]         
          p(+Full) = [4] x1 + [5] x2 + [1]
              p(0) = [4]                  
           p(Cons) = [1] x1 + [1] x2 + [8]
            p(Nil) = [3]                  
              p(S) = [1] x1 + [4]         
              p(f) = [3] x1 + [8]         
           p(goal) = [3] x1 + [4]         
            p(map) = [3] x1 + [4]         
        
        Following rules are strictly oriented:
        f(x) = [3] x + [8]
             > [3] x + [0]
             = *(x,x)     
        
        
        Following rules are (at-least) weakly oriented:
               *(x,0()) =  [1] x + [8]          
                        >= [4]                  
                        =  0()                  
        
            *(x,S(0())) =  [1] x + [16]         
                        >= [1] x + [0]          
                        =  x                    
        
           *(x,S(S(y))) =  [1] x + [2] y + [16] 
                        >= [1] x + [2] y + [16] 
                        =  +(x,*(x,S(y)))       
        
               *(0(),y) =  [2] y + [4]          
                        >= [4]                  
                        =  0()                  
        
           +Full(0(),y) =  [5] y + [17]         
                        >= [1] y + [0]          
                        =  y                    
        
          +Full(S(x),y) =  [4] x + [5] y + [17] 
                        >= [4] x + [5] y + [21] 
                        =  +Full(x,S(y))        
        
               goal(xs) =  [3] xs + [4]         
                        >= [3] xs + [4]         
                        =  map(xs)              
        
        map(Cons(x,xs)) =  [3] x + [3] xs + [28]
                        >= [3] x + [3] xs + [20]
                        =  Cons(f(x),map(xs))   
        
             map(Nil()) =  [13]                 
                        >= [3]                  
                        =  Nil()                
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        +Full(S(x),y) -> +Full(x,S(y))
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,0()) -> 0()
        *(x,S(0())) -> x
        *(x,S(S(y))) -> +(x,*(x,S(y)))
        *(0(),y) -> 0()
        +Full(0(),y) -> 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,0/0,Cons/2,Nil/0,S/1}
      Obligation:
        Innermost
        basic terms: {*,+Full,f,goal,map}/{+,0,Cons,Nil,S}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {2},
          uargs(Cons) = {1,2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(*) = [8] x1 + [9]         
              p(+) = [1] x2 + [0]         
          p(+Full) = [6] x1 + [4] x2 + [1]
              p(0) = [2]                  
           p(Cons) = [1] x1 + [1] x2 + [2]
            p(Nil) = [0]                  
              p(S) = [1] x1 + [4]         
              p(f) = [8] x1 + [9]         
           p(goal) = [10] x1 + [8]        
            p(map) = [8] x1 + [6]         
        
        Following rules are strictly oriented:
        +Full(S(x),y) = [6] x + [4] y + [25]
                      > [6] x + [4] y + [17]
                      = +Full(x,S(y))       
        
        
        Following rules are (at-least) weakly oriented:
               *(x,0()) =  [8] x + [9]          
                        >= [2]                  
                        =  0()                  
        
            *(x,S(0())) =  [8] x + [9]          
                        >= [1] x + [0]          
                        =  x                    
        
           *(x,S(S(y))) =  [8] x + [9]          
                        >= [8] x + [9]          
                        =  +(x,*(x,S(y)))       
        
               *(0(),y) =  [25]                 
                        >= [2]                  
                        =  0()                  
        
           +Full(0(),y) =  [4] y + [13]         
                        >= [1] y + [0]          
                        =  y                    
        
                   f(x) =  [8] x + [9]          
                        >= [8] x + [9]          
                        =  *(x,x)               
        
               goal(xs) =  [10] xs + [8]        
                        >= [8] xs + [6]         
                        =  map(xs)              
        
        map(Cons(x,xs)) =  [8] x + [8] xs + [22]
                        >= [8] x + [8] xs + [17]
                        =  Cons(f(x),map(xs))   
        
             map(Nil()) =  [6]                  
                        >= [0]                  
                        =  Nil()                
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        *(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,0/0,Cons/2,Nil/0,S/1}
      Obligation:
        Innermost
        basic terms: {*,+Full,f,goal,map}/{+,0,Cons,Nil,S}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).