*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(x,+(y,z)) -> +(*(x,y),*(x,z))
        *(x,1()) -> x
        *(+(x,y),z) -> +(*(x,z),*(y,z))
        *(1(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {*/2} / {+/2,1/0}
      Obligation:
        Full
        basic terms: {*}/{+,1}
    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(+) = {1,2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(*) = x1 + 4*x1*x2 + 4*x2
        p(+) = 1 + x1 + x2        
        p(1) = 0                  
      
      Following rules are strictly oriented:
      *(x,+(y,z)) = 4 + 5*x + 4*x*y + 4*x*z + 4*y + 4*z
                  > 1 + 2*x + 4*x*y + 4*x*z + 4*y + 4*z
                  = +(*(x,y),*(x,z))                   
      
      
      Following rules are (at-least) weakly oriented:
         *(x,1()) =  x                              
                  >= x                              
                  =  x                              
      
      *(+(x,y),z) =  1 + x + 4*x*z + y + 4*y*z + 8*z
                  >= 1 + x + 4*x*z + y + 4*y*z + 8*z
                  =  +(*(x,z),*(y,z))               
      
         *(1(),y) =  4*y                            
                  >= y                              
                  =  y                              
      
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(x,1()) -> x
        *(+(x,y),z) -> +(*(x,z),*(y,z))
        *(1(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        *(x,+(y,z)) -> +(*(x,y),*(x,z))
      Signature:
        {*/2} / {+/2,1/0}
      Obligation:
        Full
        basic terms: {*}/{+,1}
    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(+) = {1,2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(*) = 1 + 7*x1 + 7*x1*x2 + 4*x2
        p(+) = 1 + x1 + x2              
        p(1) = 0                        
      
      Following rules are strictly oriented:
         *(x,1()) = 1 + 7*x                             
                  > x                                   
                  = x                                   
      
      *(+(x,y),z) = 8 + 7*x + 7*x*z + 7*y + 7*y*z + 11*z
                  > 3 + 7*x + 7*x*z + 7*y + 7*y*z + 8*z 
                  = +(*(x,z),*(y,z))                    
      
         *(1(),y) = 1 + 4*y                             
                  > y                                   
                  = y                                   
      
      
      Following rules are (at-least) weakly oriented:
      *(x,+(y,z)) =  5 + 14*x + 7*x*y + 7*x*z + 4*y + 4*z
                  >= 3 + 14*x + 7*x*y + 7*x*z + 4*y + 4*z
                  =  +(*(x,y),*(x,z))                    
      
*** 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)) -> +(*(x,y),*(x,z))
        *(x,1()) -> x
        *(+(x,y),z) -> +(*(x,z),*(y,z))
        *(1(),y) -> y
      Signature:
        {*/2} / {+/2,1/0}
      Obligation:
        Full
        basic terms: {*}/{+,1}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).