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,3,2,1}
   transitions:
    h1(3,23) -> 1*
    h1(15,1) -> 1*
    h1(15,3) -> 1*
    h1(15,23) -> 1*
    h1(7,1) -> 1*
    h1(7,3) -> 1*
    h1(7,23) -> 1*
    h1(2,23) -> 1*
    h1(15,2) -> 1*
    h1(15,4) -> 1*
    h1(4,23) -> 1*
    h1(7,2) -> 1*
    h1(7,4) -> 1*
    h1(1,23) -> 1*
    c1(6,33) -> 7*
    c1(22,20) -> 23*
    c1(6,37) -> 7*
    c1(3,1) -> 20*
    c1(3,3) -> 20*
    c1(14,2) -> 15*
    c1(4,2) -> 20*
    c1(14,4) -> 7*
    c1(3,23) -> 20*
    c1(4,4) -> 20*
    c1(6,2) -> 7*
    c1(1,2) -> 20*
    c1(6,4) -> 7*
    c1(1,4) -> 20*
    c1(2,1) -> 20*
    c1(2,3) -> 20*
    c1(22,23) -> 23*
    c1(3,2) -> 20*
    c1(2,23) -> 20*
    c1(3,4) -> 20*
    c1(14,1) -> 7*
    c1(4,1) -> 20*
    c1(14,3) -> 7*
    c1(4,3) -> 20*
    c1(14,7) -> 7*
    c1(14,15) -> 7*
    c1(4,23) -> 20*
    c1(14,33) -> 7*
    c1(14,37) -> 7*
    c1(6,1) -> 7*
    c1(1,1) -> 20*
    c1(6,3) -> 7*
    c1(1,3) -> 20*
    c1(6,7) -> 7*
    c1(6,15) -> 7*
    c1(2,2) -> 20*
    c1(1,23) -> 20*
    c1(2,4) -> 20*
    s1(2) -> 6*
    s1(4) -> 14*
    s1(21) -> 22*
    s1(1) -> 14*
    s1(3) -> 6*
    01() -> 21*
    h2(33,1) -> 1*
    h2(33,3) -> 1*
    h2(33,23) -> 1*
    h2(37,1) -> 1*
    h2(31,20) -> 1*
    h2(37,3) -> 1*
    h2(33,2) -> 1*
    h2(37,23) -> 1*
    h2(33,4) -> 1*
    h2(37,2) -> 1*
    h2(37,4) -> 1*
    h2(31,23) -> 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(30,1) -> 31*
    c2(30,3) -> 31*
    c2(30,7) -> 31*
    c2(30,15) -> 31*
    c2(30,31) -> 31*
    c2(30,33) -> 31*
    c2(30,37) -> 31*
    c2(32,31) -> 33*
    c2(30,2) -> 31*
    c2(30,4) -> 31*
    c2(36,31) -> 37*
    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(22) -> 30*
    s2(2) -> 32*
    s2(4) -> 36*
    s2(1) -> 36*
    s2(3) -> 32*
    s0(2) -> 3*
    s0(4) -> 3*
    s0(1) -> 3*
    s0(3) -> 3*
    00() -> 4*
  problem:
   
  Qed