*** 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:
        Full
        basic terms: {ackin,u21}/{ackout,s,u22}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following weak dependency pairs:
      
      Strict DPs
        ackin#(s(X),s(Y)) -> c_1(u21#(ackin(s(X),Y),X))
        u21#(ackout(X),Y) -> c_2(ackin#(Y,X))
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        ackin#(s(X),s(Y)) -> c_1(u21#(ackin(s(X),Y),X))
        u21#(ackout(X),Y) -> c_2(ackin#(Y,X))
      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,ackin#/2,u21#/2} / {ackout/1,s/1,u22/1,c_1/1,c_2/1}
      Obligation:
        Full
        basic terms: {ackin#,u21#}/{ackout,s,u22}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 0, 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},
          uargs(u21#) = {1},
          uargs(c_1) = {1},
          uargs(c_2) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
           p(ackin) = [0]                  
          p(ackout) = [3]                  
               p(s) = [1] x1 + [0]         
             p(u21) = [1] x1 + [0]         
             p(u22) = [1] x1 + [0]         
          p(ackin#) = [8] x1 + [0]         
            p(u21#) = [1] x1 + [8] x2 + [0]
             p(c_1) = [1] x1 + [0]         
             p(c_2) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        u21#(ackout(X),Y) = [8] Y + [3]     
                          > [8] Y + [0]     
                          = c_2(ackin#(Y,X))
        
         u21(ackout(X),Y) = [3]             
                          > [0]             
                          = u22(ackin(Y,X)) 
        
        
        Following rules are (at-least) weakly oriented:
        ackin#(s(X),s(Y)) =  [8] X + [0]               
                          >= [8] X + [0]               
                          =  c_1(u21#(ackin(s(X),Y),X))
        
         ackin(s(X),s(Y)) =  [0]                       
                          >= [0]                       
                          =  u21(ackin(s(X),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(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        ackin#(s(X),s(Y)) -> c_1(u21#(ackin(s(X),Y),X))
      Strict TRS Rules:
        ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
      Weak DP Rules:
        u21#(ackout(X),Y) -> c_2(ackin#(Y,X))
      Weak TRS Rules:
        u21(ackout(X),Y) -> u22(ackin(Y,X))
      Signature:
        {ackin/2,u21/2,ackin#/2,u21#/2} / {ackout/1,s/1,u22/1,c_1/1,c_2/1}
      Obligation:
        Full
        basic terms: {ackin#,u21#}/{ackout,s,u22}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 0, 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},
          uargs(u21#) = {1},
          uargs(c_1) = {1},
          uargs(c_2) = {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 + [9]
             p(u21) = [1] x1 + [8]
             p(u22) = [1] x1 + [8]
          p(ackin#) = [1] x2 + [0]
            p(u21#) = [1] x1 + [0]
             p(c_1) = [1] x1 + [0]
             p(c_2) = [1] x1 + [0]
        
        Following rules are strictly oriented:
        ackin#(s(X),s(Y)) = [1] Y + [9]               
                          > [1] Y + [0]               
                          = c_1(u21#(ackin(s(X),Y),X))
        
         ackin(s(X),s(Y)) = [1] Y + [9]               
                          > [1] Y + [8]               
                          = u21(ackin(s(X),Y),X)      
        
        
        Following rules are (at-least) weakly oriented:
        u21#(ackout(X),Y) =  [1] X + [0]     
                          >= [1] X + [0]     
                          =  c_2(ackin#(Y,X))
        
         u21(ackout(X),Y) =  [1] X + [8]     
                          >= [1] X + [8]     
                          =  u22(ackin(Y,X)) 
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        ackin#(s(X),s(Y)) -> c_1(u21#(ackin(s(X),Y),X))
        u21#(ackout(X),Y) -> c_2(ackin#(Y,X))
      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,ackin#/2,u21#/2} / {ackout/1,s/1,u22/1,c_1/1,c_2/1}
      Obligation:
        Full
        basic terms: {ackin#,u21#}/{ackout,s,u22}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).