YES

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

Proof:
 DP Processor:
  DPs:
   b#(x,y) -> a#(0(),x)
   b#(x,y) -> a#(c(y),a(0(),x))
   a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
   a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
   a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
  TRS:
   b(x,y) -> c(a(c(y),a(0(),x)))
   a(y,x) -> y
   a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
  TDG Processor:
   DPs:
    b#(x,y) -> a#(0(),x)
    b#(x,y) -> a#(c(y),a(0(),x))
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
   TRS:
    b(x,y) -> c(a(c(y),a(0(),x)))
    a(y,x) -> y
    a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
   graph:
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) ->
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0()) ->
    b#(x,y) -> a#(c(y),a(0(),x))
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0()) ->
    b#(x,y) -> a#(0(),x)
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y) ->
    b#(x,y) -> a#(c(y),a(0(),x))
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y) -> b#(x,y) -> a#(0(),x)
    b#(x,y) -> a#(0(),x) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
    b#(x,y) -> a#(0(),x) -> a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    b#(x,y) -> a#(0(),x) -> a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    b#(x,y) -> a#(c(y),a(0(),x)) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
    b#(x,y) -> a#(c(y),a(0(),x)) ->
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    b#(x,y) -> a#(c(y),a(0(),x)) -> a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [a#](x0, x1) = x0 + x1 + 0,
     
     [b#](x0, x1) = 1x0 + -1x1 + 2,
     
     [a](x0, x1) = x0 + 1x1 + 2,
     
     [0] = 0,
     
     [c](x0) = -1x0 + 2,
     
     [b](x0, x1) = 2x0 + -2x1 + 2
    orientation:
     b#(x,y) = 1x + -1y + 2 >= x + 0 = a#(0(),x)
     
     b#(x,y) = 1x + -1y + 2 >= 1x + -1y + 2 = a#(c(y),a(0(),x))
     
     a#(y,c(b(a(0(),x),0()))) = 2x + y + 3 >= -1y + 2 = b#(0(),y)
     
     a#(y,c(b(a(0(),x),0()))) = 2x + y + 3 >= x + -3y + 2 = a#(c(b(0(),y)),x)
     
     a#(y,c(b(a(0(),x),0()))) = 2x + y + 3 >= 2x + -2y + 3 = b#(a(c(b(0(),y)),x),0())
     
     b(x,y) = 2x + -2y + 2 >= 1x + -2y + 2 = c(a(c(y),a(0(),x)))
     
     a(y,x) = 1x + y + 2 >= y = y
     
     a(y,c(b(a(0(),x),0()))) = 3x + y + 4 >= 3x + -1y + 4 = b(a(c(b(0(),y)),x),0())
    problem:
     DPs:
      b#(x,y) -> a#(c(y),a(0(),x))
      a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
     TRS:
      b(x,y) -> c(a(c(y),a(0(),x)))
      a(y,x) -> y
      a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
    Matrix Interpretation Processor: dim=2
     
     interpretation:
      [a#](x0, x1) = [3 0]x1,
      
      [b#](x0, x1) = [2 2]x1,
      
                         [0 0]  
      [a](x0, x1) = x0 + [2 0]x1,
      
            [0]
      [0] = [1],
      
                [0 1]  
      [c](x0) = [0 0]x0,
      
                    [0 0]     [2 0]     [0]
      [b](x0, x1) = [1 0]x0 + [0 0]x1 + [1]
     orientation:
      b#(x,y) = [2 2]y >= [0] = a#(c(y),a(0(),x))
      
      a#(y,c(b(a(0(),x),0()))) = [3] >= [2] = b#(a(c(b(0(),y)),x),0())
      
               [0 0]    [2 0]    [0]    [0]                      
      b(x,y) = [1 0]x + [0 0]y + [1] >= [0] = c(a(c(y),a(0(),x)))
      
               [0 0]              
      a(y,x) = [2 0]x + y >= y = y
      
                                    [0]    [0]                          
      a(y,c(b(a(0(),x),0()))) = y + [2] >= [2] = b(a(c(b(0(),y)),x),0())
     problem:
      DPs:
       b#(x,y) -> a#(c(y),a(0(),x))
      TRS:
       b(x,y) -> c(a(c(y),a(0(),x)))
       a(y,x) -> y
       a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 13/1