YES(?,O(n^1)) Problem: \(x,x) -> e() /(x,x) -> e() .(e(),x) -> x .(x,e()) -> x \(e(),x) -> x /(x,e()) -> x .(x,\(x,y)) -> y .(/(y,x),x) -> y \(x,.(x,y)) -> y /(.(y,x),x) -> y /(x,\(y,x)) -> y \(/(x,y),x) -> y Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {5} transitions: e1() -> 5* \0(5,5) -> 5* /0(5,5) -> 5* .0(5,5) -> 5* problem: Qed