*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
        u21(ackout(X),Y) -> u22(ackin(Y,X))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {ackin/2,u21/2} / {ackout/1,s/1,u22/1}
      Obligation:
        Innermost
        basic terms: {ackin,u21}/{ackout,s,u22}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(u21) = {1},
        uargs(u22) = {1}
      
      Following symbols are considered usable:
        {ackin,u21}
      TcT has computed the following interpretation:
         p(ackin) = [0]         
        p(ackout) = [1]         
             p(s) = [2]         
           p(u21) = [8] x1 + [0]
           p(u22) = [1] x1 + [2]
      
      Following rules are strictly oriented:
      u21(ackout(X),Y) = [8]            
                       > [2]            
                       = u22(ackin(Y,X))
      
      
      Following rules are (at-least) weakly oriented:
      ackin(s(X),s(Y)) =  [0]                 
                       >= [0]                 
                       =  u21(ackin(s(X),Y),X)
      
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
      Weak DP Rules:
        
      Weak TRS Rules:
        u21(ackout(X),Y) -> u22(ackin(Y,X))
      Signature:
        {ackin/2,u21/2} / {ackout/1,s/1,u22/1}
      Obligation:
        Innermost
        basic terms: {ackin,u21}/{ackout,s,u22}
    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(u21) = {1},
          uargs(u22) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
           p(ackin) = [1] x2 + [0]
          p(ackout) = [1] x1 + [0]
               p(s) = [1] x1 + [1]
             p(u21) = [1] x1 + [0]
             p(u22) = [1] x1 + [0]
        
        Following rules are strictly oriented:
        ackin(s(X),s(Y)) = [1] Y + [1]         
                         > [1] Y + [0]         
                         = u21(ackin(s(X),Y),X)
        
        
        Following rules are (at-least) weakly oriented:
        u21(ackout(X),Y) =  [1] X + [0]    
                         >= [1] X + [0]    
                         =  u22(ackin(Y,X))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
        u21(ackout(X),Y) -> u22(ackin(Y,X))
      Signature:
        {ackin/2,u21/2} / {ackout/1,s/1,u22/1}
      Obligation:
        Innermost
        basic terms: {ackin,u21}/{ackout,s,u22}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).