Changes:
 - Now computations cannot have silent labels, as it is kind of the
point of the weak bisimulations that the ordering of computations is
preserved.
 - The above change propagated through
 - Full fork commutativity proof in the sense of providing a relation R
such that for all fork expressions the original and the swapped are in
relation and R obeys the weak bisimilarity. (This is quite a big change,
just shy of 4000 lines.)