Hi, all.
As agreed yesterday during the lecture, next week's lecture will take place remotely via zoom at the following (password-protected) URL:
https://zoom.us/j/4911012202 Pwd: @cbc
The time will be the usual one (3pm to 6pm). The URL & pwd will be active from 2:30pm, in case you want to check your connection ahead of time.
I uploaded the slides and model of the course section we finished yesterday. The model includes the deadlock freedom theorem for machine m2, but *without the proof*, which needs manual intervention. I am leaving the discharging of the proof as an exercise for you. I have left hints on how to proceed (at least, one way that worked for me) in the comments in the model. If you take the right steps, it can be done in under five minutes.
Remember also that the "Proving" section of the course website (https://wp.software.imdea.org/cbc/proving-tips/) has some general tips that are applicable to this case also. Note: we tend to use p0 to work with the active hypotheses. ml is also good with arithmetic, so it may help as well.
Best,