For each construction e.g. 3x3 Join:

ThreeXThree represents the behaviour of the module 3x3 Join.
ThreeXThreeCon represents the construction using other modules (e.g. DM and 1x3 Join), achieved by placing components in CCS parallel-composition, and then restricting intermediate ports.
ThreeXThreeenv represents all possible behaviours of the environment when interacting with either the original module or its construction. (i.e. - send a1 and b1, then wait for c11).

Then the two agents ThreeXThreeBinding and ThreeXThreeConBinding represent the composition of the environment with the original module and the construction respectively.

Then we test that ThreeXThreeBinding and ThreeXThreeConBinding are weakly bisimilar, using the command

eq(ThreeXThreeBinding,ThreeXThreeConBinding);

If this returns true, then ThreeXThreeCon accurately simulates the external behaviour of 3x3 Join.

This is repeated for 1x3, 1x4, 3x3, 3x4, 4x4 Joins.