YES(?,O(n^1)) Problem: app(app(app(uncurry(),f),x),y) -> app(app(f,x),y) Proof: Bounds Processor: bound: 0 enrichment: match automaton: final states: {2} transitions: app0(1,1) -> 2* uncurry0() -> 1* problem: Qed