This entry provides a verified implementation of rank-based Büchi Complementation. The verification is done in three steps:
- Definition of odd rankings and proof that an automaton rejects a word iff there exists an odd ranking for it.
- Definition of the complement automaton and proof that it accepts exactly those words for which there is an odd ranking.
- Verified implementation of the complement automaton using the Isabelle Collections Framework.