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.