Renamed to better reflect contents
Cleaning up a bit
Formalization of the CEK machine