YES(?,O(n^1)) 0.15/0.22 YES(?,O(n^1)) 0.15/0.22 0.15/0.22 Problem: 0.15/0.22 f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) 0.15/0.22 f(x,y,y) -> y 0.15/0.22 f(x,y,g(y)) -> x 0.15/0.22 f(x,x,y) -> x 0.15/0.22 f(g(x),x,y) -> y 0.15/0.22 0.15/0.22 Proof: 0.15/0.22 Bounds Processor: 0.15/0.22 bound: 0 0.15/0.22 enrichment: match 0.15/0.22 automaton: 0.15/0.22 final states: {3,2} 0.15/0.22 transitions: 0.15/0.22 f0(1,1,1) -> 2* 0.15/0.22 f0(1,3,1) -> 2* 0.15/0.22 f0(3,1,1) -> 2* 0.15/0.22 f0(3,3,1) -> 2* 0.15/0.22 f0(1,1,3) -> 2* 0.15/0.22 f0(1,3,3) -> 2* 0.15/0.22 f0(3,1,3) -> 2* 0.15/0.22 f0(3,3,3) -> 2* 0.15/0.22 g0(1) -> 3*,2,1 0.15/0.22 g0(3) -> 2,3* 0.15/0.22 1 -> 2* 0.15/0.22 3 -> 2* 0.15/0.22 problem: 0.15/0.22 0.15/0.22 Qed 0.15/0.23 EOF