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