YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   c(c(c(y))) -> c(c(a(y,0())))
   c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
   c(y) -> y
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [a](x0, x1) = x0 + x1 + 2,
    
    [0] = 31,
    
    [c](x0) = x0 + 1
   orientation:
    c(c(c(y))) = y + 3 >= y + 35 = c(c(a(y,0())))
    
    c(a(a(0(),x),y)) = x + y + 36 >= y + 36 = a(c(c(c(0()))),y)
    
    c(y) = y + 1 >= y = y
   problem:
    strict:
     c(c(c(y))) -> c(c(a(y,0())))
     c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
    weak:
     c(y) -> y
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [a](x0, x1) = x0 + x1 + 9,
     
     [0] = 11,
     
     [c](x0) = x0
    orientation:
     c(c(c(y))) = y >= y + 20 = c(c(a(y,0())))
     
     c(a(a(0(),x),y)) = x + y + 29 >= y + 20 = a(c(c(c(0()))),y)
     
     c(y) = y >= y = y
    problem:
     strict:
      c(c(c(y))) -> c(c(a(y,0())))
     weak:
      c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      c(y) -> y
    Bounds Processor:
     bound: 3
     enrichment: match-rt
     automaton:
      final states: {4}
      transitions:
       c3(27) -> 28*
       c3(28) -> 25*
       c1(10) -> 4*
       c1(12) -> 13*
       c1(9) -> 10*
       c1(11) -> 12*
       c1(8) -> 11*
       a3(14,26) -> 27*
       a1(9,8) -> 9*
       a1(4,8) -> 9*
       a1(13,4) -> 4*
       a1(13,8) -> 10*
       a1(10,8) -> 9*
       03() -> 26*
       01() -> 8*
       c2(15) -> 16*
       c2(24) -> 25*
       c2(14) -> 23*
       c2(16) -> 13*
       c2(23) -> 24*
       c0(4) -> 4*
       a2(8,14) -> 15*
       a2(25,8) -> 10,4
       a0(4,4) -> 4*
       02() -> 14*
       00() -> 4*
       8 -> 11*
       9 -> 10*
       10 -> 4*
       11 -> 12*
       12 -> 13*
       14 -> 23*
       15 -> 16*
       16 -> 13*
       23 -> 24*
       24 -> 25*
       27 -> 28*
       28 -> 25*
     problem:
      strict:
       
      weak:
       c(c(c(y))) -> c(c(a(y,0())))
       c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
       c(y) -> y
     Qed