# Re: Assistance requested on a Hoare-y problem - corrected and cleaned up...

```Well - the formatting was a disaster...and there was an unnecessary step...

"G. S. Stiles" wrote:

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

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

Note: the alphabet of NOISYVM includes toffee... but NOISYVM does not
do toffee.

>
> 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)
>
> 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:
>
> 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)))
>                 |
>                    (curse -> clink ->   ((choc -> clunk -> NOISYVM)
>                                               ||
>                                                  (choc -> CUST)))
>
> Applying L4A twice to both ||:
>
> NOISYVM || CUST   =

coin ->    (clink -> curse  ->  choc ->   clunk ->    (NOISYVM

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

uX.(coin ->    ((clink -> curse  ->  choc ->   clunk ->  X)

>                          |
>                              (curse -> clink -> choc ->  clunk ->   X))
>
> Does this do it???
> It was certainly more fun than the lecture I was working on.

>
> Dyke.
>
> --
> ======================================================================
> Dyke Stiles            >>>>>> new address!!>>> dyke.stiles@xxxxxxxxxxx
> Professor and Chair, Graduate Committee
> Department of Electrical and Computer Engineering
> Utah State University
> 4120 Old Main Hill
> Logan UT 84322-4120
> Voice: +1-435-797-2840                          FAX:   +1-435-797-3054
> Research:            http://www.engineering.usu.edu/ece/research/rtpc/
> Play:  http://www.engineering.usu.edu/ece/research/rtpc/utah/utah.html
> ======================================================================

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