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())
  EDG 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#(0(),y)
    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#(a(c(b(0(),y)),x),0())
    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#(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#(0(),y) ->
    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))
    b#(x,y) -> a#(0(),x) -> a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    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#(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#(0(),y)
    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#(a(c(b(0(),y)),x),0())
   Bounds Processor:
    bound: 2
    enrichment: match
    automaton:
     final states: {6,5}
     transitions:
      b1(14,10) -> 14*
      b1(10,1) -> 20*
      b1(10,3) -> 20*
      b1(10,21) -> 20*
      b1(10,2) -> 20*
      b1(10,4) -> 20*
      b1(10,10) -> 33*
      b1(22,10) -> 22,3
      a1(18,17) -> 24*
      a1(10,1) -> 17*
      a1(10,3) -> 14*
      a1(15,17) -> 24*
      a1(21,2) -> 22*
      a1(21,4) -> 22*
      a1(18,14) -> 24*
      a1(10,2) -> 14*
      a1(10,4) -> 17*
      a1(15,14) -> 24*
      a1(21,1) -> 22*
      a1(21,3) -> 22*
      c1(20) -> 21*
      c1(2) -> 15*
      c1(24) -> 4*
      c1(4) -> 15*
      c1(1) -> 18*
      c1(33) -> 10*
      c1(3) -> 18*
      01() -> 10*
      b{#,1}(14,10) -> 5*
      b{#,1}(10,1) -> 6*
      b{#,1}(10,3) -> 6*
      b{#,1}(10,21) -> 6*
      b{#,1}(10,2) -> 6*
      b{#,1}(10,4) -> 6*
      b{#,1}(10,10) -> 5*
      b{#,1}(22,10) -> 6*
      a{#,1}(18,17) -> 5*
      a{#,1}(10,1) -> 5*
      a{#,1}(10,3) -> 5*
      a{#,1}(15,17) -> 5*
      a{#,1}(21,2) -> 6*
      a{#,1}(21,4) -> 6*
      a{#,1}(18,14) -> 5*
      a{#,1}(10,2) -> 5*
      a{#,1}(10,4) -> 5*
      a{#,1}(15,14) -> 5*
      a{#,1}(21,1) -> 6*
      a{#,1}(21,3) -> 6*
      c2(10) -> 30*
      c2(2) -> 32*
      c2(34) -> 22,3
      c2(4) -> 32*
      c2(36) -> 20*
      c2(21) -> 32*
      c2(38) -> 14,33
      c2(3) -> 32*
      b{#,0}(3,1) -> 5*
      b{#,0}(3,3) -> 5*
      b{#,0}(4,2) -> 5*
      b{#,0}(4,4) -> 5*
      b{#,0}(1,2) -> 5*
      b{#,0}(1,4) -> 5*
      b{#,0}(2,1) -> 5*
      b{#,0}(2,3) -> 5*
      b{#,0}(3,2) -> 5*
      b{#,0}(3,4) -> 5*
      b{#,0}(4,1) -> 5*
      b{#,0}(4,3) -> 5*
      b{#,0}(1,1) -> 5*
      b{#,0}(1,3) -> 5*
      b{#,0}(2,2) -> 5*
      b{#,0}(2,4) -> 5*
      a2(27,22) -> 29*
      a2(30,29) -> 34*
      a2(30,31) -> 38*
      a2(32,31) -> 36*
      a2(27,10) -> 31*
      a2(27,14) -> 31*
      a{#,0}(3,1) -> 6*
      a{#,0}(3,3) -> 6*
      a{#,0}(4,2) -> 6*
      a{#,0}(4,4) -> 6*
      a{#,0}(1,2) -> 6*
      a{#,0}(1,4) -> 6*
      a{#,0}(2,1) -> 6*
      a{#,0}(2,3) -> 6*
      a{#,0}(3,2) -> 6*
      a{#,0}(3,4) -> 6*
      a{#,0}(4,1) -> 6*
      a{#,0}(4,3) -> 6*
      a{#,0}(1,1) -> 6*
      a{#,0}(1,3) -> 6*
      a{#,0}(2,2) -> 6*
      a{#,0}(2,4) -> 6*
      02() -> 27*
      00() -> 1*
      a{#,2}(27,14) -> 5*
      a{#,2}(27,22) -> 6*
      a{#,2}(30,29) -> 6*
      a{#,2}(30,31) -> 5*
      a{#,2}(32,31) -> 6*
      a{#,2}(27,10) -> 5,6
      c0(2) -> 2*
      c0(4) -> 2*
      c0(1) -> 2*
      c0(3) -> 2*
      a0(3,1) -> 3*
      a0(3,3) -> 3*
      a0(4,2) -> 3*
      a0(4,4) -> 3*
      a0(1,2) -> 3*
      a0(1,4) -> 3*
      a0(2,1) -> 3*
      a0(2,3) -> 3*
      a0(3,2) -> 3*
      a0(3,4) -> 3*
      a0(4,1) -> 3*
      a0(4,3) -> 3*
      a0(1,1) -> 3*
      a0(1,3) -> 3*
      a0(2,2) -> 3*
      a0(2,4) -> 3*
      b0(3,1) -> 4*
      b0(3,3) -> 4*
      b0(4,2) -> 4*
      b0(4,4) -> 4*
      b0(1,2) -> 4*
      b0(1,4) -> 4*
      b0(2,1) -> 4*
      b0(2,3) -> 4*
      b0(3,2) -> 4*
      b0(3,4) -> 4*
      b0(4,1) -> 4*
      b0(4,3) -> 4*
      b0(1,1) -> 4*
      b0(1,3) -> 4*
      b0(2,2) -> 4*
      b0(2,4) -> 4*
      1 -> 3*
      2 -> 3*
      4 -> 3*
      10 -> 14,17
      15 -> 24*
      18 -> 24*
      21 -> 22*
      27 -> 29,31
      30 -> 38,34
      32 -> 36*
    problem:
     DPs:
      
     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())
    Qed