thus UsedI*Loc (Stop SCM+FSA) = UsedInt*Loc (halt SCM+FSA) by Th2
.= {} by SF_MASTR:32 ; :: thesis: verum