YES(?,O(n^1))

Problem:
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)
 if(0(),y,z) -> y
 if(s(x),y,z) -> z
 half(double(x)) -> x

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6,5,4,3}
   transitions:
    -1(1,2) -> 5*
    -1(2,1) -> 5*
    -1(1,1) -> 5*
    -1(2,2) -> 5*
    s1(12) -> 12,4
    s1(7) -> 8*
    s1(8) -> 7,3
    half1(2) -> 12*
    half1(1) -> 12*
    01() -> 12,7,4,3
    double1(2) -> 7*
    double1(1) -> 7*
    double0(2) -> 3*
    double0(1) -> 3*
    00() -> 1*
    s0(2) -> 2*
    s0(1) -> 2*
    half0(2) -> 4*
    half0(1) -> 4*
    -0(1,2) -> 5*
    -0(2,1) -> 5*
    -0(1,1) -> 5*
    -0(2,2) -> 5*
    if0(1,1,1) -> 6*
    if0(2,2,1) -> 6*
    if0(1,1,2) -> 6*
    if0(2,2,2) -> 6*
    if0(1,2,1) -> 6*
    if0(2,1,1) -> 6*
    if0(1,2,2) -> 6*
    if0(2,1,2) -> 6*
    1 -> 6,5
    2 -> 6,5
  problem:
   
  Qed