-
P || Q = Q || P
parallelism is symmetric.
-
P || (Q || R) = (P || Q) || R
we do not care what order you said things were parallel in.
-
P || STOP = STOP
i.e. deadlock is infectious.
-
(c #tex2html_wrap_inline4134# P) || (c #tex2html_wrap_inline4138#Q) = (c #tex2html_wrap_inline4140# (P || Q))
i.e. if the alarm rings then we run out
and the alarm rings then we start shouting,
its the same as the alarm ringing and (we run out shouting.
-
(c #tex2html_wrap_inline4144# P) || (d #tex2html_wrap_inline4148# Q) = STOP (c #tex2html_wrap_inline4150# d)
-
In general, if both of 2 procs offer a choice of initial event
the combined proc will only engage in events they both offer:
This lets us rewrite concurrent systems in terms of choice and
prefix: e.g.
if
#equation1094#
and
#equation1096#
then
#equation1098#
so we now have a proc that could be defined:
#equation1100#