Convert Julian's automata formalization to HOA data types
https://www.isa-afp.org/browser_info/current/AFP/Transition_Systems_and_Automata/BA_Implement.html
-
convert arbitrary states and atomic propositions to nat -
convert rabin acceptance to hoa representation (using markers) -
define conversion between runs -
proof acceptance equivalence