feat: unbundled design for automata theory

[ctchou]

This patch ports automata theory to an unbundled design, building on top of #141. The main changes are:

• Finite-ness assumptions are removed. There are no more DFA, NFA, and EpsilonNFA. In their stead, the theory works with DA, NA, and EpsilonNA directly.
• Acceptance conditions are separated out into the file Accept.lean and are made orthogonal to automata proper (DA and NA).
• Buchi and Muller acceptance conditions are introduced to illustrate the last point, though no theorems about them have been proved.
• All previous results in automata theory (the equivalence between DA and NA on finite words, the closure properties of regular languages under boolean operations, etc) are ported to the new design.