YES(?,O(n^1))

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:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {5}
   transitions:
    b3(18,26) -> 20*
    b3(25,24) -> 26*
    c1(5) -> 9*
    c1(14) -> 9,5
    c1(23) -> 13*
    c1(13) -> 14*
    03() -> 25*
    b1(10,9) -> 11*
    b1(5,11) -> 5*
    b1(12,5) -> 13*
    b1(12,12) -> 23*
    c3(18) -> 24*
    a1(10,10) -> 12*
    01() -> 10*
    c2(10) -> 17*
    c2(22) -> 14*
    c2(21) -> 22*
    a0(5,5) -> 5*
    b2(18,17) -> 19*
    b2(10,19) -> 12*
    b2(20,12) -> 21*
    b0(5,5) -> 5*
    a2(18,18) -> 20*
    00() -> 5*
    02() -> 18*
    c0(5) -> 5*
    12 -> 13*
  problem:
   
  Qed