YES

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

Proof:
 DP Processor:
  DPs:
   c#(c(c(y))) -> b#(0(),y)
   c#(c(c(y))) -> c#(b(0(),y))
   c#(c(c(y))) -> a#(c(b(0(),y)),0())
   c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
   c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
   c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
   a#(y,0()) -> b#(y,0())
  TRS:
   b(b(0(),y),x) -> y
   c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
   a(y,0()) -> b(y,0())
  EDG Processor:
   DPs:
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> a#(c(b(0(),y)),0())
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    a#(y,0()) -> b#(y,0())
   TRS:
    b(b(0(),y),x) -> y
    c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
    a(y,0()) -> b(y,0())
   graph:
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0()) ->
    a#(y,0()) -> b#(y,0())
    c#(c(c(y))) -> a#(c(b(0(),y)),0()) ->
    a#(y,0()) -> b#(y,0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> a#(c(b(0(),y)),0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> a#(c(b(0(),y)),0())
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 14/49
    DPs:
     c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
     c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    TRS:
     b(b(0(),y),x) -> y
     c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
     a(y,0()) -> b(y,0())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [c#](x0) = x0,
      
      [a](x0, x1) = x0,
      
      [c](x0) = x0 + 1,
      
      [b](x0, x1) = x0 + x1,
      
      [0] = 0
     orientation:
      c#(c(c(y))) = y + 2 >= y + 1 = c#(a(a(c(b(0(),y)),0()),0()))
      
      c#(c(c(y))) = y + 2 >= y + 2 = c#(c(a(a(c(b(0(),y)),0()),0())))
      
      b(b(0(),y),x) = x + y >= y = y
      
      c(c(c(y))) = y + 3 >= y + 3 = c(c(a(a(c(b(0(),y)),0()),0())))
      
      a(y,0()) = y >= y = b(y,0())
     problem:
      DPs:
       c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
      TRS:
       b(b(0(),y),x) -> y
       c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
       a(y,0()) -> b(y,0())
     Bounds Processor:
      bound: 0
      enrichment: match-dp
      automaton:
       final states: {6}
       transitions:
        c{#,0}(11) -> 6*
        c0(10) -> 11*
        c0(7) -> 8*
        c0(2) -> 4*
        c0(4) -> 4*
        c0(1) -> 4*
        c0(3) -> 4*
        a0(8,1) -> 9*
        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(9,1) -> 10*
        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(8,1) -> 9*
        b0(3,1) -> 2*
        b0(3,3) -> 2*
        b0(4,2) -> 2*
        b0(4,4) -> 2*
        b0(1,2) -> 2*
        b0(1,4) -> 2*
        b0(2,1) -> 3,2
        b0(2,3) -> 2*
        b0(3,2) -> 2*
        b0(3,4) -> 2*
        b0(9,1) -> 10*
        b0(4,1) -> 3,2
        b0(4,3) -> 2*
        b0(1,1) -> 3,2
        b0(1,3) -> 2*
        b0(1,5) -> 7*
        b0(2,2) -> 2*
        b0(2,4) -> 2*
        00() -> 1*
        1 -> 3,2,5
        2 -> 3,5
        3 -> 2,5
        4 -> 2,5
      problem:
       DPs:
        
       TRS:
        b(b(0(),y),x) -> y
        c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
        a(y,0()) -> b(y,0())
      Qed