# atari-proofs
The goal of this project is to formally prove a lower bound on the time it takes to beat the game [*Dragster*](https://en.wikipedia.org/wiki/Dragster_(video_game)).
So far, I have implemented a specification of the Atari 2600 console, and used it to state the theorem. Now I just have to prove it!
Of course, that's easier said than done.
# Dependencies
- coq 8.13.2
- coq-record-update 0.3.0
- coq-mathcomp-ssreflect 1.14.0
- coq-mathcomp-algebra 1.14.0