Dear René
... all states are renamed to integers 0 .. n-1.
Thank you for working on this. I updated my timing and profiling data https://github.com/jwaldmann/ceta-postproc/issues/25#issuecomment-1219982858 it's down 15 percent, and now red-black tree operations dominate everything. So, perhaps - use a better implementation of sets (like containers:Data.IntMap - but I understand you want that certified first ... perhaps it can be imported with "sorry", just to get an idea of the run-time) - remove sets altogether from (the hot code of) checking bounds (what do they represent? why are they needed? the automaton is non-deterministic, because it can have epsilon transitions? ) well, clearly that work should be sponsored by the authors of tools that use match-bounds... Best regards, Johannes.