Hi,
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
Roy Wilson
designrw@xxxxxxxxxxxxxxxx