YES

Problem:
 a(x,y) -> b(x,b(0(),c(y)))
 c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
 b(y,0()) -> y

Proof:
 DP Processor:
  DPs:
   a#(x,y) -> c#(y)
   a#(x,y) -> b#(0(),c(y))
   a#(x,y) -> b#(x,b(0(),c(y)))
   c#(b(y,c(x))) -> a#(0(),0())
   c#(b(y,c(x))) -> b#(a(0(),0()),y)
   c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
   c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
  TRS:
   a(x,y) -> b(x,b(0(),c(y)))
   c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
   b(y,0()) -> y
  EDG Processor:
   DPs:
    a#(x,y) -> c#(y)
    a#(x,y) -> b#(0(),c(y))
    a#(x,y) -> b#(x,b(0(),c(y)))
    c#(b(y,c(x))) -> a#(0(),0())
    c#(b(y,c(x))) -> b#(a(0(),0()),y)
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
   TRS:
    a(x,y) -> b(x,b(0(),c(y)))
    c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
    b(y,0()) -> y
   graph:
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> a#(0(),0())
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> b#(a(0(),0()),y)
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) ->
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> a#(0(),0())
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> b#(a(0(),0()),y)
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) ->
    c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
    c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> c#(y)
    c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(0(),c(y))
    c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(x,b(0(),c(y)))
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> a#(0(),0())
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> b#(a(0(),0()),y)
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
   SCC Processor:
    #sccs: 1
    #rules: 4
    #arcs: 15/49
    DPs:
     c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
     c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
     c#(b(y,c(x))) -> a#(0(),0())
     a#(x,y) -> c#(y)
    TRS:
     a(x,y) -> b(x,b(0(),c(y)))
     c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
     b(y,0()) -> y
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [c#](x0) = x0,
      
      [a#](x0, x1) = x1 + 1,
      
      [b](x0, x1) = x0 + x1,
      
      [c](x0) = 1,
      
      [0] = 0,
      
      [a](x0, x1) = x0 + 1
     orientation:
      c#(b(y,c(x))) = y + 1 >= y + 1 = c#(b(a(0(),0()),y))
      
      c#(b(y,c(x))) = y + 1 >= 1 = c#(c(b(a(0(),0()),y)))
      
      c#(b(y,c(x))) = y + 1 >= 1 = a#(0(),0())
      
      a#(x,y) = y + 1 >= y = c#(y)
      
      a(x,y) = x + 1 >= x + 1 = b(x,b(0(),c(y)))
      
      c(b(y,c(x))) = 1 >= 1 = c(c(b(a(0(),0()),y)))
      
      b(y,0()) = y >= y = y
     problem:
      DPs:
       c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
       c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
       c#(b(y,c(x))) -> a#(0(),0())
      TRS:
       a(x,y) -> b(x,b(0(),c(y)))
       c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
       b(y,0()) -> y
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [c#](x0) = 1,
       
       [a#](x0, x1) = 0,
       
       [b](x0, x1) = x0 + x1,
       
       [c](x0) = 0,
       
       [0] = 1,
       
       [a](x0, x1) = x0 + 1
      orientation:
       c#(b(y,c(x))) = 1 >= 1 = c#(b(a(0(),0()),y))
       
       c#(b(y,c(x))) = 1 >= 1 = c#(c(b(a(0(),0()),y)))
       
       c#(b(y,c(x))) = 1 >= 0 = a#(0(),0())
       
       a(x,y) = x + 1 >= x + 1 = b(x,b(0(),c(y)))
       
       c(b(y,c(x))) = 0 >= 0 = c(c(b(a(0(),0()),y)))
       
       b(y,0()) = y + 1 >= y = y
      problem:
       DPs:
        c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
        c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y)))
       TRS:
        a(x,y) -> b(x,b(0(),c(y)))
        c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
        b(y,0()) -> y
      Bounds Processor:
       bound: 3
       enrichment: match
       automaton:
        final states: {7}
        transitions:
         02() -> 16*
         a0(6,6) -> 6*
         c{#,2}(18) -> 7*
         00() -> 6*
         b3(26,25) -> 27*
         b3(16,27) -> 17*
         c1(6) -> 14*
         c1(13) -> 6,13
         03() -> 26*
         b1(11,14) -> 15*
         b1(6,15) -> 6*
         b1(12,6) -> 13*
         b1(12,12) -> 13*
         c3(16) -> 25*
         a1(11,11) -> 12*
         01() -> 11*
         c{#,1}(13) -> 7*
         c2(11) -> 21*
         c2(18) -> 13,18
         c2(13) -> 6*
         c{#,0}(6) -> 7*
         b2(11,22) -> 12*
         b2(16,21) -> 22*
         b2(17,12) -> 18*
         b0(6,6) -> 6*
         a2(16,16) -> 17*
         c0(6) -> 6*
         12 -> 13*
       problem:
        DPs:
         
        TRS:
         a(x,y) -> b(x,b(0(),c(y)))
         c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
         b(y,0()) -> y
       Qed