# Re: Assistance requested on a Hoare-y problem

```Greetings -

In my formatting below, I write the expression a -> (P || Q) as

a ->      (P
||
Q)

Roy Wilson wrote:

>
>
> 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

NOISYVM = (coin -> clink -> choc -> clunk -> NOISYVM)

CUST = (coin -> (toffee -> CUST | curse -> choc -> CUST))

NOISYVM || CUST =         (coin -> clink -> choc -> clunk -> NOISYVM)
||
(coin -> (toffee -> CUST | curse ->
choc -> CUST))

by L4A:          =   coin ->         (clink -> choc -> clunk -> NOISYVM)
||
(toffee -> CUST | curse -> choc
-> CUST)

by L6:          =  coin ->        (clink ->     ((choc -> clunk -> NOISYVM)
||
(toffee -> CUST
| curse -> choc -> CUST))
|
(toffee ->     ((clink -> choc ->
clunk -> NOISYVM)
||
CUST))

Since NOISYVM cannot engage in toffee, but any occurrence of toffee must
involve both NOISYVM and CUST - since it appears in both alphabets - the event
toffee
can never occur - leading to

NOISYVM || CUST   =     coin ->         (clink ->     (choc -> clunk ->
NOISYVM))
||
(curse -> choc ->
CUST)

Using L6 again:

NOISYVM || CUST   = coin ->         (clink ->         ((choc -> clunk ->
NOISYVM)
||

(curse -> choc -> CUST)))
|
(curse ->
((clink -> choc -> clunk -> NOISYVM)
||

(choc -> CUST)))

Applying L5B to the first component of the |, and L5A to the second:

(NOISYVM || CUST)   =  coin ->      (clink -> curse  ->     ((choc -> clunk ->
NOISYVM)

||

(choc -> CUST)))
|
->     ((choc -> clunk -> NOISYVM)

||

(choc -> CUST)))

Applying L4A twice to both ||:

NOISYVM || CUST   =  coin ->        (clink -> curse  ->  choc ->   clunk ->
(NOISYVM

||

CUST))
|
choc ->  clunk ->    (NOISYVM

||

CUST))

NOISYVM || CUST = uX.(coin ->    ((clink -> curse  ->  choc ->   clunk ->  X)
|
choc ->  clunk ->   X))

Does this do it???

Dyke.

--
======================================================================
Dyke Stiles            >>>>>> new address!!>>> dyke.stiles@xxxxxxxxxxx