YES(?,O(n^1))

Problem:
 +(+(x,y),z) -> +(x,+(y,z))
 +(f(x),f(y)) -> f(+(x,y))
 +(f(x),+(f(y),z)) -> +(f(+(x,y)),z)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {2}
   transitions:
    f1(4) -> 4,2
    +1(1,1) -> 4*
    +0(1,1) -> 2*
    f0(1) -> 1*
  problem:
   
  Qed