YES(?,O(n^1)) Problem: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {5,4,3} transitions: 11(20) -> 21* 11(7) -> 8* 01(8) -> 9* R1(6) -> 7* R1(18) -> 19* 21(9) -> 10* 10(2) -> 3* 10(1) -> 3* 20(2) -> 1* 20(1) -> 1* 00(2) -> 4* 00(1) -> 4* L0(2) -> 5* L0(1) -> 5* R0(2) -> 2* R0(1) -> 2* 1 -> 18* 2 -> 6* 9 -> 20* 10 -> 3* 19 -> 7* 21 -> 4* problem: Qed