YES(?,O(n^1)) Problem: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {8,7,6,5,4,3} transitions: ql1(41) -> 42* ql1(43) -> 44* ql1(33) -> 34* 11(25) -> 26* 11(22) -> 23* 01(15) -> 16* 01(12) -> 13* m1(35) -> 36* m1(32) -> 33* qr1(23) -> 24* qr1(13) -> 14* r00(2) -> 3* r00(1) -> 3* 00(2) -> 5* 00(1) -> 5* 10(2) -> 6* 10(1) -> 6* m0(2) -> 7* m0(1) -> 7* r10(2) -> 4* r10(1) -> 4* b0(2) -> 8* b0(1) -> 8* qr0(2) -> 1* qr0(1) -> 1* ql0(2) -> 2* ql0(1) -> 2* 1 -> 35,25,15 2 -> 32,22,12 13 -> 41* 14 -> 16,13,41,5 16 -> 13* 23 -> 43* 24 -> 26,23,43,6 26 -> 23* 34 -> 36,33,7 36 -> 33* 42 -> 13,41,5 44 -> 23,43,6 problem: Qed