*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(x,*(y,z)) -> *(otimes(x,y),z)
        *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
        *(+(x,y),z) -> oplus(*(x,z),*(y,z))
        *(1(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {*/2} / {+/2,1/0,oplus/2,otimes/2}
      Obligation:
        Innermost
        basic terms: {*}/{+,1,oplus,otimes}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(oplus) = {1,2}
      
      Following symbols are considered usable:
        {*}
      TcT has computed the following interpretation:
             p(*) = x1 + 2*x1*x2 + 2*x2
             p(+) = 1 + x1 + x2        
             p(1) = 0                  
         p(oplus) = 1 + x1 + x2        
        p(otimes) = x1 + x2            
      
      Following rules are strictly oriented:
      *(x,oplus(y,z)) = 2 + 3*x + 2*x*y + 2*x*z + 2*y + 2*z
                      > 1 + 2*x + 2*x*y + 2*x*z + 2*y + 2*z
                      = oplus(*(x,y),*(x,z))               
      
      
      Following rules are (at-least) weakly oriented:
      *(x,*(y,z)) =  x + 2*x*y + 4*x*y*z + 4*x*z + 2*y + 4*y*z + 4*z
                  >= x + 2*x*z + y + 2*y*z + 2*z                    
                  =  *(otimes(x,y),z)                               
      
      *(+(x,y),z) =  1 + x + 2*x*z + y + 2*y*z + 4*z                
                  >= 1 + x + 2*x*z + y + 2*y*z + 4*z                
                  =  oplus(*(x,z),*(y,z))                           
      
         *(1(),y) =  2*y                                            
                  >= y                                              
                  =  y                                              
      
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(x,*(y,z)) -> *(otimes(x,y),z)
        *(+(x,y),z) -> oplus(*(x,z),*(y,z))
        *(1(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
      Signature:
        {*/2} / {+/2,1/0,oplus/2,otimes/2}
      Obligation:
        Innermost
        basic terms: {*}/{+,1,oplus,otimes}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(oplus) = {1,2}
      
      Following symbols are considered usable:
        {*}
      TcT has computed the following interpretation:
             p(*) = 2*x1 + 2*x1*x2 + x2
             p(+) = 1 + x1 + x2        
             p(1) = 0                  
         p(oplus) = 1 + x1 + x2        
        p(otimes) = x1 + x2            
      
      Following rules are strictly oriented:
      *(+(x,y),z) = 2 + 2*x + 2*x*z + 2*y + 2*y*z + 3*z
                  > 1 + 2*x + 2*x*z + 2*y + 2*y*z + 2*z
                  = oplus(*(x,z),*(y,z))               
      
      
      Following rules are (at-least) weakly oriented:
          *(x,*(y,z)) =  2*x + 4*x*y + 4*x*y*z + 2*x*z + 2*y + 2*y*z + z
                      >= 2*x + 2*x*z + 2*y + 2*y*z + z                  
                      =  *(otimes(x,y),z)                               
      
      *(x,oplus(y,z)) =  1 + 4*x + 2*x*y + 2*x*z + y + z                
                      >= 1 + 4*x + 2*x*y + 2*x*z + y + z                
                      =  oplus(*(x,y),*(x,z))                           
      
             *(1(),y) =  y                                              
                      >= y                                              
                      =  y                                              
      
*** 1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(x,*(y,z)) -> *(otimes(x,y),z)
        *(1(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
        *(+(x,y),z) -> oplus(*(x,z),*(y,z))
      Signature:
        {*/2} / {+/2,1/0,oplus/2,otimes/2}
      Obligation:
        Innermost
        basic terms: {*}/{+,1,oplus,otimes}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(oplus) = {1,2}
      
      Following symbols are considered usable:
        {*}
      TcT has computed the following interpretation:
             p(*) = 2*x1 + 2*x1*x2 + 2*x2
             p(+) = 1 + x1 + x2          
             p(1) = 1                    
         p(oplus) = 1 + x1 + x2          
        p(otimes) = 0                    
      
      Following rules are strictly oriented:
      *(1(),y) = 2 + 4*y
               > y      
               = y      
      
      
      Following rules are (at-least) weakly oriented:
          *(x,*(y,z)) =  2*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z
                      >= 2*z                                              
                      =  *(otimes(x,y),z)                                 
      
      *(x,oplus(y,z)) =  2 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z              
                      >= 1 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z              
                      =  oplus(*(x,y),*(x,z))                             
      
          *(+(x,y),z) =  2 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z              
                      >= 1 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z              
                      =  oplus(*(x,z),*(y,z))                             
      
*** 1.1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(x,*(y,z)) -> *(otimes(x,y),z)
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
        *(+(x,y),z) -> oplus(*(x,z),*(y,z))
        *(1(),y) -> y
      Signature:
        {*/2} / {+/2,1/0,oplus/2,otimes/2}
      Obligation:
        Innermost
        basic terms: {*}/{+,1,oplus,otimes}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(oplus) = {1,2}
      
      Following symbols are considered usable:
        {*}
      TcT has computed the following interpretation:
             p(*) = 1 + 2*x1 + 2*x1*x2 + 2*x2
             p(+) = 1 + x1 + x2              
             p(1) = 1                        
         p(oplus) = 1 + x1 + x2              
        p(otimes) = 0                        
      
      Following rules are strictly oriented:
      *(x,*(y,z)) = 3 + 4*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z
                  > 1 + 2*z                                              
                  = *(otimes(x,y),z)                                     
      
      
      Following rules are (at-least) weakly oriented:
      *(x,oplus(y,z)) =  3 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z
                      >= 3 + 4*x + 2*x*y + 2*x*z + 2*y + 2*z
                      =  oplus(*(x,y),*(x,z))               
      
          *(+(x,y),z) =  3 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z
                      >= 3 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z
                      =  oplus(*(x,z),*(y,z))               
      
             *(1(),y) =  3 + 4*y                            
                      >= y                                  
                      =  y                                  
      
*** 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,*(y,z)) -> *(otimes(x,y),z)
        *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
        *(+(x,y),z) -> oplus(*(x,z),*(y,z))
        *(1(),y) -> y
      Signature:
        {*/2} / {+/2,1/0,oplus/2,otimes/2}
      Obligation:
        Innermost
        basic terms: {*}/{+,1,oplus,otimes}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).