Dear all,
the slides and the model from yesterday's lecture are available at the course's website. As suggested, please do the following:
- Import it into Rodin.
- Check that the proof obligations for models m0 and m1 are all discharged (i.e., in green). If not, click on the undischarged ones, switch to theorem prover view and use the "PP" button to discharge then.
- Do the same for the proof obligations in machine m2. Some of the undischarged proofs can be proven this way, but others will need more (manual) intervention.
Please refer to
https://wp.software.imdea.org/cbc/rodin-installation-and-tips/
for basic instructions and to
https://wp.software.imdea.org/cbc/proving-tips/#proving
to learn more about what is available in the "Proving perspective".
Best,