YES(?,O(n^1)) 0.16/0.20 YES(?,O(n^1)) 0.16/0.20 0.16/0.20 Problem: 0.16/0.20 a(b(a(x))) -> b(a(x)) 0.16/0.20 0.16/0.20 Proof: 0.16/0.20 Bounds Processor: 0.16/0.20 bound: 2 0.16/0.20 enrichment: match 0.16/0.20 automaton: 0.16/0.20 final states: {3} 0.16/0.20 transitions: 0.16/0.20 b1(8) -> 9* 0.16/0.20 a1(7) -> 8* 0.16/0.20 b2(11) -> 12* 0.16/0.20 a0(3) -> 3* 0.16/0.20 a2(10) -> 11* 0.16/0.20 b0(3) -> 3* 0.16/0.20 3 -> 7* 0.16/0.20 7 -> 10* 0.16/0.20 9 -> 3* 0.16/0.20 12 -> 11,8 0.16/0.20 problem: 0.16/0.20 0.16/0.20 Qed 0.16/0.21 EOF