D1,D2,D3:Dsys. D1 
D2 
D2 D3 D1 D3M1,M2,M3:MsgA. M1 M2 M2 M3 M1 M3| Rank | Theorem | Name |
| 8 | D1,D2,D3:Dsys. D1 D2 D2 D3 D1 D3 | [d-sub_transitivity] |
| cites the following: | ||
| 7 | M1,M2,M3:MsgA. M1 M2 M2 M3 M1 M3 | [ma-sub_transitivity] |