YES(?,O(n^1))

Problem:
 h(x,c(y,z)) -> h(c(s(y),x),z)
 h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z)))

Proof:
 RT Transformation Processor:
  strict:
   h(x,c(y,z)) -> h(c(s(y),x),z)
   h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0] = 2,
    
    [s](x0) = x0 + 1,
    
    [h](x0, x1) = x0 + x1 + 11,
    
    [c](x0, x1) = x0 + x1 + 1
   orientation:
    h(x,c(y,z)) = x + y + z + 12 >= x + y + z + 13 = h(c(s(y),x),z)
    
    h(c(s(x),c(s(0()),y)),z) = x + y + z + 17 >= x + y + z + 16 = h(y,c(s(0()),c(x,z)))
   problem:
    strict:
     h(x,c(y,z)) -> h(c(s(y),x),z)
    weak:
     h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z)))
   Bounds Processor:
    bound: 2
    enrichment: match-rt
    automaton:
     final states: {4,3,2,1}
     transitions:
      h1(7,24) -> 1*
      h1(2,24) -> 1*
      h1(4,24) -> 1*
      h1(11,2) -> 1*
      h1(11,4) -> 1*
      h1(26,24) -> 1*
      h1(7,1) -> 1*
      h1(7,3) -> 1*
      h1(11,24) -> 1*
      h1(1,24) -> 1*
      h1(28,24) -> 1*
      h1(3,24) -> 1*
      h1(11,1) -> 1*
      h1(11,3) -> 1*
      h1(7,2) -> 1*
      h1(7,4) -> 1*
      c1(3,1) -> 21*
      c1(3,3) -> 21*
      c1(2,24) -> 21*
      c1(23,21) -> 24*
      c1(4,2) -> 21*
      c1(4,4) -> 21*
      c1(10,1) -> 7*
      c1(10,3) -> 7*
      c1(4,24) -> 21*
      c1(10,7) -> 7*
      c1(10,11) -> 7*
      c1(6,2) -> 7*
      c1(1,2) -> 21*
      c1(6,4) -> 7*
      c1(1,4) -> 21*
      c1(2,1) -> 21*
      c1(2,3) -> 21*
      c1(1,24) -> 21*
      c1(6,28) -> 7*
      c1(3,2) -> 21*
      c1(3,4) -> 21*
      c1(23,24) -> 24*
      c1(4,1) -> 21*
      c1(4,3) -> 21*
      c1(3,24) -> 21*
      c1(10,2) -> 11*
      c1(10,4) -> 7*
      c1(6,1) -> 7*
      c1(1,1) -> 21*
      c1(6,3) -> 7*
      c1(1,3) -> 21*
      c1(6,7) -> 7*
      c1(10,28) -> 7*
      c1(6,11) -> 7*
      c1(2,2) -> 21*
      c1(2,4) -> 21*
      s1(22) -> 23*
      s1(2) -> 6*
      s1(4) -> 10*
      s1(1) -> 10*
      s1(3) -> 6*
      01() -> 22*
      h2(28,1) -> 1*
      h2(28,3) -> 1*
      h2(26,24) -> 1*
      h2(28,2) -> 1*
      h2(28,4) -> 1*
      h2(28,24) -> 1*
      h2(26,21) -> 1*
      h0(3,1) -> 1*
      h0(3,3) -> 1*
      h0(4,2) -> 1*
      h0(4,4) -> 1*
      h0(1,2) -> 1*
      h0(1,4) -> 1*
      h0(2,1) -> 1*
      h0(2,3) -> 1*
      h0(3,2) -> 1*
      h0(3,4) -> 1*
      h0(4,1) -> 1*
      h0(4,3) -> 1*
      h0(1,1) -> 1*
      h0(1,3) -> 1*
      h0(2,2) -> 1*
      h0(2,4) -> 1*
      c2(27,26) -> 28*
      c2(25,1) -> 26*
      c2(25,3) -> 26*
      c2(25,7) -> 26*
      c2(25,11) -> 26*
      c2(25,2) -> 26*
      c2(25,4) -> 26*
      c2(25,26) -> 26*
      c2(25,28) -> 26*
      c0(3,1) -> 2*
      c0(3,3) -> 2*
      c0(4,2) -> 2*
      c0(4,4) -> 2*
      c0(1,2) -> 2*
      c0(1,4) -> 2*
      c0(2,1) -> 2*
      c0(2,3) -> 2*
      c0(3,2) -> 2*
      c0(3,4) -> 2*
      c0(4,1) -> 2*
      c0(4,3) -> 2*
      c0(1,1) -> 2*
      c0(1,3) -> 2*
      c0(2,2) -> 2*
      c0(2,4) -> 2*
      s2(2) -> 27*
      s2(4) -> 27*
      s2(1) -> 27*
      s2(23) -> 25*
      s2(3) -> 27*
      s0(2) -> 3*
      s0(4) -> 3*
      s0(1) -> 3*
      s0(3) -> 3*
      00() -> 4*
    problem:
     strict:
      
     weak:
      h(x,c(y,z)) -> h(c(s(y),x),z)
      h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z)))
    Qed