*** 1 Progress [(?,O(n^1))]  ***
    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:
        Innermost
        basic terms: {:}/{+,a,f,g}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a())))
        :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
        :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a())))
        :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
        :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
      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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
      Obligation:
        Innermost
        basic terms: {:#}/{+,a,f,g}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {1}
      by application of
        Pre({1}) = {2,3}.
      Here rules are labelled as follows:
        1: :#(z,+(x,f(y))) -> c_1(:#(g(z,y)    
                                    ,+(x,a())))
        2: :#(+(x,y),z) -> c_2(:#(x,z)         
                              ,:#(y,z))        
        3: :#(:(x,y),z) -> c_3(:#(x,:(y,z))    
                              ,:#(y,z))        
*** 1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
        :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
      Strict TRS Rules:
        
      Weak DP Rules:
        :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a())))
      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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
      Obligation:
        Innermost
        basic terms: {:#}/{+,a,f,g}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S::#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
           -->_2 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
           -->_1 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
           -->_2 :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a()))):3
           -->_1 :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a()))):3
           -->_2 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
           -->_1 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
        
        2:S::#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
           -->_2 :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a()))):3
           -->_1 :#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a()))):3
           -->_2 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
           -->_1 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
           -->_2 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
           -->_1 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
        
        3:W::#(z,+(x,f(y))) -> c_1(:#(g(z,y),+(x,a())))
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        3: :#(z,+(x,f(y))) -> c_1(:#(g(z,y)    
                                    ,+(x,a())))
*** 1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
        :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
      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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
      Obligation:
        Innermost
        basic terms: {:#}/{+,a,f,g}
    Applied Processor:
      PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
    Proof:
      We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
        2: :#(:(x,y),z) -> c_3(:#(x,:(y,z))
                              ,:#(y,z))    
        
      The strictly oriented rules are moved into the weak component.
  *** 1.1.1.1.1 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
          :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
        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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
        Obligation:
          Innermost
          basic terms: {:#}/{+,a,f,g}
      Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
      Proof:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1,2},
          uargs(c_3) = {1,2}
        
        Following symbols are considered usable:
          {:#}
        TcT has computed the following interpretation:
            p(+) = [1] x1 + [1] x2 + [0]
            p(:) = [5] x1 + [3] x2 + [2]
            p(a) = [0]                  
            p(f) = [0]                  
            p(g) = [0]                  
           p(:#) = [1] x1 + [0]         
          p(c_1) = [0]                  
          p(c_2) = [1] x1 + [1] x2 + [0]
          p(c_3) = [4] x1 + [2] x2 + [0]
        
        Following rules are strictly oriented:
        :#(:(x,y),z) = [5] x + [3] y + [2]      
                     > [4] x + [2] y + [0]      
                     = c_3(:#(x,:(y,z)),:#(y,z))
        
        
        Following rules are (at-least) weakly oriented:
        :#(+(x,y),z) =  [1] x + [1] y + [0] 
                     >= [1] x + [1] y + [0] 
                     =  c_2(:#(x,z),:#(y,z))
        
  *** 1.1.1.1.1.1 Progress [(?,O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
        Strict TRS Rules:
          
        Weak DP Rules:
          :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
        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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
        Obligation:
          Innermost
          basic terms: {:#}/{+,a,f,g}
      Applied Processor:
        Assumption
      Proof:
        ()
  
  *** 1.1.1.1.2 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
        Strict TRS Rules:
          
        Weak DP Rules:
          :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
        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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
        Obligation:
          Innermost
          basic terms: {:#}/{+,a,f,g}
      Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
      Proof:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
          1: :#(+(x,y),z) -> c_2(:#(x,z) 
                                ,:#(y,z))
          
        The strictly oriented rules are moved into the weak component.
    *** 1.1.1.1.2.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
          Strict TRS Rules:
            
          Weak DP Rules:
            :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
          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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
          Obligation:
            Innermost
            basic terms: {:#}/{+,a,f,g}
        Applied Processor:
          NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
        Proof:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_2) = {1,2},
            uargs(c_3) = {1,2}
          
          Following symbols are considered usable:
            {:#}
          TcT has computed the following interpretation:
              p(+) = [1] x1 + [1] x2 + [3]
              p(:) = [2] x1 + [1] x2 + [0]
              p(a) = [4]                  
              p(f) = [14]                 
              p(g) = [1]                  
             p(:#) = [8] x1 + [0]         
            p(c_1) = [1] x1 + [0]         
            p(c_2) = [1] x1 + [1] x2 + [9]
            p(c_3) = [2] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
          :#(+(x,y),z) = [8] x + [8] y + [24]
                       > [8] x + [8] y + [9] 
                       = c_2(:#(x,z),:#(y,z))
          
          
          Following rules are (at-least) weakly oriented:
          :#(:(x,y),z) =  [16] x + [8] y + [0]     
                       >= [16] x + [8] y + [0]     
                       =  c_3(:#(x,:(y,z)),:#(y,z))
          
    *** 1.1.1.1.2.1.1 Progress [(?,O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
            :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
          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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
          Obligation:
            Innermost
            basic terms: {:#}/{+,a,f,g}
        Applied Processor:
          Assumption
        Proof:
          ()
    
    *** 1.1.1.1.2.2 Progress [(O(1),O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
            :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
          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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
          Obligation:
            Innermost
            basic terms: {:#}/{+,a,f,g}
        Applied Processor:
          RemoveWeakSuffixes
        Proof:
          Consider the dependency graph
            1:W::#(+(x,y),z) -> c_2(:#(x,z),:#(y,z))
               -->_2 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
               -->_1 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
               -->_2 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
               -->_1 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
            
            2:W::#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z))
               -->_2 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
               -->_1 :#(:(x,y),z) -> c_3(:#(x,:(y,z)),:#(y,z)):2
               -->_2 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
               -->_1 :#(+(x,y),z) -> c_2(:#(x,z),:#(y,z)):1
            
          The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
            1: :#(+(x,y),z) -> c_2(:#(x,z)     
                                  ,:#(y,z))    
            2: :#(:(x,y),z) -> c_3(:#(x,:(y,z))
                                  ,:#(y,z))    
    *** 1.1.1.1.2.2.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} / {+/2,a/0,f/1,g/2,c_1/1,c_2/2,c_3/2}
          Obligation:
            Innermost
            basic terms: {:#}/{+,a,f,g}
        Applied Processor:
          EmptyProcessor
        Proof:
          The problem is already closed. The intended complexity is O(1).