YES(?,O(n^1))
TRS:
 {
              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)))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                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)))
   }
  BOUND:
   Bound: match(-raise)-bounded by 2
   Automaton:
    {
           0_1() -> 4*
           0_0() -> 1*
          s_2(5) -> 8*
          s_2(1) -> 10*
          s_1(4) -> 5*
          s_1(1) -> 2*
          s_0(1) -> 1*
      c_2(10, 9) -> 11*
      c_2(8, 11) -> 9*
       c_2(8, 9) -> 9*
       c_2(8, 3) -> 9*
       c_2(8, 1) -> 9*
       c_1(5, 7) -> 7*
       c_1(5, 6) -> 7*
      c_1(2, 11) -> 3*
       c_1(2, 3) -> 3*
       c_1(2, 1) -> 3*
       c_1(1, 7) -> 6*
       c_1(1, 1) -> 6*
       c_0(1, 1) -> 1*
      h_2(11, 7) -> 1*
      h_2(11, 1) -> 1*
       h_2(9, 7) -> 1*
       h_2(9, 6) -> 1*
      h_1(11, 7) -> 1*
       h_1(9, 7) -> 1*
       h_1(3, 7) -> 1*
       h_1(3, 1) -> 1*
       h_1(1, 7) -> 1*
     h_0(1, 1) -> 1*
    }
   Strict:
    {}
   Qed