[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Assistance requested on a Hoare-y problem

Title: Assistance requested on a Hoare-y problem


I'm working my way through Hoare's Communicating Sequential Processes book. I am semi-stuck on Example X1 on p. 69. It seems that the chief tool ought to be L6 on p. 71, but I've had no luck.

I have done graduate work (in the US :-)) in theory of computation, category theory, and the kind of stuff in Appendix A of Roscoe's book, so I'm not a stranger to symbolic manipulation, despite my possible stupidity in this matter.

If anyone who has actually done a line by line derivation would care to communicate the first and second lines (please, no use of "clearly" :-)) of the proof, I'd be most appreciative.


Roy Wilson