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