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