*** 1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a(c(d(x))) -> c(x)
        u(b(d(d(x)))) -> b(x)
        v(a(a(x))) -> u(v(x))
        v(a(c(x))) -> u(b(d(x)))
        v(c(x)) -> b(x)
        w(a(a(x))) -> u(w(x))
        w(a(c(x))) -> u(b(d(x)))
        w(c(x)) -> b(x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {a/1,u/1,v/1,w/1} / {b/1,c/1,d/1}
      Obligation:
        Full
        basic terms: {a,u,v,w}/{b,c,d}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following weak dependency pairs:
      
      Strict DPs
        a#(c(d(x))) -> c_1(x)
        u#(b(d(d(x)))) -> c_2(x)
        v#(a(a(x))) -> c_3(u#(v(x)))
        v#(a(c(x))) -> c_4(u#(b(d(x))))
        v#(c(x)) -> c_5(x)
        w#(a(a(x))) -> c_6(u#(w(x)))
        w#(a(c(x))) -> c_7(u#(b(d(x))))
        w#(c(x)) -> c_8(x)
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        a#(c(d(x))) -> c_1(x)
        u#(b(d(d(x)))) -> c_2(x)
        v#(a(a(x))) -> c_3(u#(v(x)))
        v#(a(c(x))) -> c_4(u#(b(d(x))))
        v#(c(x)) -> c_5(x)
        w#(a(a(x))) -> c_6(u#(w(x)))
        w#(a(c(x))) -> c_7(u#(b(d(x))))
        w#(c(x)) -> c_8(x)
      Strict TRS Rules:
        a(c(d(x))) -> c(x)
        u(b(d(d(x)))) -> b(x)
        v(a(a(x))) -> u(v(x))
        v(a(c(x))) -> u(b(d(x)))
        v(c(x)) -> b(x)
        w(a(a(x))) -> u(w(x))
        w(a(c(x))) -> u(b(d(x)))
        w(c(x)) -> b(x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
      Obligation:
        Full
        basic terms: {a#,u#,v#,w#}/{b,c,d}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        a#(c(d(x))) -> c_1(x)
        u#(b(d(d(x)))) -> c_2(x)
        v#(c(x)) -> c_5(x)
        w#(c(x)) -> c_8(x)
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        a#(c(d(x))) -> c_1(x)
        u#(b(d(d(x)))) -> c_2(x)
        v#(c(x)) -> c_5(x)
        w#(c(x)) -> c_8(x)
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
      Obligation:
        Full
        basic terms: {a#,u#,v#,w#}/{b,c,d}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following constant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          none
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
            p(a) = [0]         
            p(b) = [0]         
            p(c) = [5]         
            p(d) = [0]         
            p(u) = [0]         
            p(v) = [0]         
            p(w) = [0]         
           p(a#) = [0]         
           p(u#) = [5]         
           p(v#) = [1]         
           p(w#) = [1] x1 + [2]
          p(c_1) = [0]         
          p(c_2) = [0]         
          p(c_3) = [0]         
          p(c_4) = [0]         
          p(c_5) = [0]         
          p(c_6) = [0]         
          p(c_7) = [0]         
          p(c_8) = [0]         
        
        Following rules are strictly oriented:
        u#(b(d(d(x)))) = [5]   
                       > [0]   
                       = c_2(x)
        
              v#(c(x)) = [1]   
                       > [0]   
                       = c_5(x)
        
              w#(c(x)) = [7]   
                       > [0]   
                       = c_8(x)
        
        
        Following rules are (at-least) weakly oriented:
        a#(c(d(x))) =  [0]   
                    >= [0]   
                    =  c_1(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:
        a#(c(d(x))) -> c_1(x)
      Strict TRS Rules:
        
      Weak DP Rules:
        u#(b(d(d(x)))) -> c_2(x)
        v#(c(x)) -> c_5(x)
        w#(c(x)) -> c_8(x)
      Weak TRS Rules:
        
      Signature:
        {a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
      Obligation:
        Full
        basic terms: {a#,u#,v#,w#}/{b,c,d}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
      The following argument positions are considered usable:
        none
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
          p(a) = [0]         
          p(b) = [0]         
          p(c) = [0]         
          p(d) = [0]         
          p(u) = [0]         
          p(v) = [4] x1 + [0]
          p(w) = [1] x1 + [2]
         p(a#) = [4]         
         p(u#) = [0]         
         p(v#) = [0]         
         p(w#) = [0]         
        p(c_1) = [0]         
        p(c_2) = [0]         
        p(c_3) = [0]         
        p(c_4) = [0]         
        p(c_5) = [0]         
        p(c_6) = [0]         
        p(c_7) = [0]         
        p(c_8) = [0]         
      
      Following rules are strictly oriented:
      a#(c(d(x))) = [4]   
                  > [0]   
                  = c_1(x)
      
      
      Following rules are (at-least) weakly oriented:
      u#(b(d(d(x)))) =  [0]   
                     >= [0]   
                     =  c_2(x)
      
            v#(c(x)) =  [0]   
                     >= [0]   
                     =  c_5(x)
      
            w#(c(x)) =  [0]   
                     >= [0]   
                     =  c_8(x)
      
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        a#(c(d(x))) -> c_1(x)
        u#(b(d(d(x)))) -> c_2(x)
        v#(c(x)) -> c_5(x)
        w#(c(x)) -> c_8(x)
      Weak TRS Rules:
        
      Signature:
        {a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
      Obligation:
        Full
        basic terms: {a#,u#,v#,w#}/{b,c,d}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).