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:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    h1(12,16) -> 4*
    h1(2,16) -> 4*
    h1(8,1) -> 4*
    h1(8,3) -> 4*
    h1(1,16) -> 4*
    h1(12,1) -> 4*
    h1(12,3) -> 4*
    h1(8,2) -> 4*
    h1(8,16) -> 4*
    h1(3,16) -> 4*
    h1(12,2) -> 4*
    c1(2,16) -> 13*
    c1(3,1) -> 13*
    c1(3,3) -> 13*
    c1(7,28) -> 8*
    c1(7,30) -> 8*
    c1(7,34) -> 8*
    c1(15,13) -> 16*
    c1(11,2) -> 8*
    c1(1,2) -> 13*
    c1(11,8) -> 8*
    c1(11,12) -> 8*
    c1(1,16) -> 13*
    c1(7,1) -> 8*
    c1(2,1) -> 13*
    c1(7,3) -> 8*
    c1(2,3) -> 13*
    c1(11,28) -> 8*
    c1(11,30) -> 8*
    c1(11,34) -> 8*
    c1(3,2) -> 13*
    c1(3,16) -> 13*
    c1(15,16) -> 16*
    c1(11,1) -> 12*
    c1(1,1) -> 13*
    c1(11,3) -> 8*
    c1(1,3) -> 13*
    c1(7,2) -> 8*
    c1(2,2) -> 13*
    c1(7,8) -> 8*
    c1(7,12) -> 8*
    s1(2) -> 7*
    s1(14) -> 15*
    s1(1) -> 11*
    s1(3) -> 7*
    01() -> 14*
    h2(22,16) -> 4*
    h2(28,1) -> 4*
    h2(28,3) -> 4*
    h2(34,2) -> 4*
    h2(34,16) -> 4*
    h2(30,1) -> 4*
    h2(30,3) -> 4*
    h2(22,13) -> 4*
    h2(28,2) -> 4*
    h2(28,16) -> 4*
    h2(34,1) -> 4*
    h2(34,3) -> 4*
    h2(30,2) -> 4*
    h2(30,16) -> 4*
    h0(3,1) -> 4*
    h0(3,3) -> 4*
    h0(1,2) -> 4*
    h0(2,1) -> 4*
    h0(2,3) -> 4*
    h0(3,2) -> 4*
    h0(1,1) -> 4*
    h0(1,3) -> 4*
    h0(2,2) -> 4*
    c2(27,22) -> 28*
    c2(29,22) -> 30*
    c2(21,2) -> 22*
    c2(21,8) -> 22*
    c2(21,12) -> 22*
    c2(21,22) -> 22*
    c2(21,28) -> 22*
    c2(21,30) -> 22*
    c2(21,34) -> 22*
    c2(33,22) -> 34*
    c2(21,1) -> 22*
    c2(21,3) -> 22*
    c0(3,1) -> 1*
    c0(3,3) -> 1*
    c0(1,2) -> 1*
    c0(2,1) -> 1*
    c0(2,3) -> 1*
    c0(3,2) -> 1*
    c0(1,1) -> 1*
    c0(1,3) -> 1*
    c0(2,2) -> 1*
    s2(15) -> 21*
    s2(2) -> 27*
    s2(1) -> 33*
    s2(3) -> 29*
    s0(2) -> 2*
    s0(1) -> 2*
    s0(3) -> 2*
    00() -> 3*
  problem:
   
  Qed