let I, J, K be MacroInstruction of SCM+FSA ; :: thesis: (I ";" J) ';' K = I ";" (J ';' K)
thus (I ";" J) ';' K = ((stop (Directed I)) ';' J) ';' K
.= (stop (Directed I)) ';' (J ';' K) by COMPOS_1:29
.= I ";" (J ';' K) ; :: thesis: verum