one documented rewriting is not applied?
Fanda reported that the automaton produced for
FGa | (GFa & GFb) could be easily reduced by one state.
Looking at the formula, I do not understand why it is not rewritten to
F(Ga | (GFa & GFb)) using the last rule of page 23 just before section 5.4.3. This rewriting would be enough to remove that extra state.