YES(?,O(n^1)) 0.15/0.20 YES(?,O(n^1)) 0.15/0.20 0.15/0.20 Problem: 0.15/0.20 f(g(x)) -> g(g(f(x))) 0.15/0.20 f(g(x)) -> g(g(g(x))) 0.15/0.20 0.15/0.20 Proof: 0.15/0.20 Bounds Processor: 0.15/0.20 bound: 1 0.15/0.20 enrichment: match 0.15/0.20 automaton: 0.15/0.20 final states: {2} 0.15/0.20 transitions: 0.15/0.20 g1(5) -> 6* 0.15/0.20 g1(4) -> 5* 0.15/0.20 g1(13) -> 14* 0.15/0.20 f1(3) -> 4* 0.15/0.20 f0(1) -> 2* 0.15/0.20 g0(1) -> 1* 0.15/0.20 1 -> 13,3 0.15/0.20 6 -> 4,2 0.15/0.20 14 -> 4* 0.15/0.20 problem: 0.15/0.20 0.15/0.20 Qed 0.15/0.20 EOF