- added ProductTheory.agda, DFA.agda, and Regualar.agda
- ProductTheory contains a 3-ary existential
- DFA.agda defines DFAs and their languages
- Regular.agda defines regular languages mathematically
- All of the "primitive" NFA combinators have now been defined and proven
  correct