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: {5}
   transitions:
    h1(9,10) -> 5*
    h1(5,13) -> 5*
    h1(5,25) -> 5*
    h1(17,13) -> 5*
    h1(17,25) -> 5*
    h1(9,5) -> 5*
    h1(19,13) -> 5*
    h1(9,13) -> 5*
    h1(19,25) -> 5*
    h1(9,25) -> 5*
    h1(5,10) -> 5*
    c1(12,24) -> 25*
    c1(8,5) -> 9*
    c1(8,9) -> 9*
    c1(8,19) -> 9*
    c1(5,5) -> 10*
    c1(5,13) -> 10*
    c1(5,25) -> 10*
    c1(12,5) -> 24*
    c1(12,13) -> 13*
    c1(12,25) -> 10*
    c1(5,10) -> 10*
    c1(5,24) -> 10*
    c1(12,10) -> 13*
    s1(5) -> 8*
    s1(11) -> 12*
    01() -> 11*
    h2(17,24) -> 5*
    h2(19,10) -> 5*
    h2(19,24) -> 5*
    h2(17,5) -> 5*
    h2(17,13) -> 5*
    h2(17,25) -> 5*
    h2(19,5) -> 5*
    h2(19,13) -> 5*
    h2(19,25) -> 5*
    h2(17,10) -> 5*
    h0(5,5) -> 5*
    c2(18,5) -> 17*
    c2(18,9) -> 17*
    c2(18,17) -> 19*
    c2(18,19) -> 17*
    c2(16,5) -> 17*
    c2(16,9) -> 19*
    c2(16,17) -> 17*
    c2(16,19) -> 17*
    c0(5,5) -> 5*
    s2(5) -> 18*
    s2(12) -> 16*
    s0(5) -> 5*
    00() -> 5*
  problem:
   
  Qed