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
  TDG 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))) -> c#(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#(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))) -> a#(0(),0())
    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))) -> 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))) -> 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))) -> a#(0(),0()) -> a#(x,y) -> b#(x,b(0(),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) -> c#(y)
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(c(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))) -> b#(a(0(),0()),y)
    a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> a#(0(),0())
   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))) -> a#(0(),0())
     a#(x,y) -> c#(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
    CDG Processor:
     DPs:
      c#(b(y,c(x))) -> c#(b(a(0(),0()),y))
      c#(b(y,c(x))) -> a#(0(),0())
      a#(x,y) -> c#(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))) -> a#(0(),0()) -> a#(x,y) -> 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))) -> 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: 2
      #arcs: 4/16
      DPs:
       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
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [c#](x0) = x0 + 0,
        
        [a#](x0, x1) = x0 + x1 + 0,
        
        [b](x0, x1) = x0 + x1 + 0,
        
        [c](x0) = x0 + 1,
        
        [0] = 0,
        
        [a](x0, x1) = 1x0 + 1x1 + 1
       orientation:
        c#(b(y,c(x))) = x + y + 1 >= 0 = a#(0(),0())
        
        a#(x,y) = x + y + 0 >= y + 0 = c#(y)
        
        a(x,y) = 1x + 1y + 1 >= x + y + 1 = b(x,b(0(),c(y)))
        
        c(b(y,c(x))) = x + y + 1 >= y + 1 = c(c(b(a(0(),0()),y)))
        
        b(y,0()) = y + 0 >= y = y
       problem:
        DPs:
         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
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 2/1