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