1.   a.(b + c)    and    a.b + a.c
 
     Answer: no for all


2.1. a | b-   and   a.b- + b-.a

     Answer: no for all


2.2. a | b-   and   a.b- + b-.a,   with a =/= b

     Answer: yes for strong bisimulation and above


3.1. new a. (a- | a.P | a.tau.Q)    and    tau.P + tau.Q,  

     with a,b notin fn P,Q

     Answer: no for strong, but yes for observational and above


3.2. Same but without side condition.

     Answer: none (take P=a)


3.3. new a. (a- | a.P | a.Q)    and    tau.P + Q,  

     with a,b notin fn P,Q

     Answer: no for strong, no for observational, yes for weak

     RR =  { (new a. (a- | a.P | a.Q), tau.P + Q) }
         U { (new a. (P' | a.Q), P')   /  a notin fn P' }
         U { (new a. (a.P | Q'), Q')   /  a notin fn Q' }


4.   Alpha convert: x(x).new y.x-y.y(y).y-x

     Answer: x(x1).new y.x1-y.y(y1).y1-x1


5.   Derive the two steps of reaction

       new y. x-y. y(w).P | x(u).new y. u-y

     Answer:

        new y. x-y. y(w).P | x(u).new y. u-y
     == new y. (x-y. y(w).P | x(u).new y. u-y)
     -> new y. (y(z).P | new z. y-z)
     == new y. new z. (y(w).P | y-z),  z notin fn P
     -> new y. new z. {z/w}P


6.   Derive the first tau transition

     Answer:
    
     new y. x-y. y(w).P -x-(y)-> y(w).P    x(u).new y.u-y -xy-> new y.y-z
     ------------------------------------------------------------------------
     new y. x-y. y(w).P | x(u).new z. u-z   ->   new y. (y(z).P | new z. y-z)