let I be MacroInstruction of SCM+FSA ; :: thesis: stop (Directed I) = I ";" (Stop SCM+FSA)
thus I ";" (Stop SCM+FSA) = (stop (Directed I)) ';' (Stop SCM+FSA)
.= stop (Directed I) ; :: thesis: verum