thus UsedInt*Loc (Stop SCM+FSA) = UsedInt*Loc (0 .--> (halt SCM+FSA))
.= UsedInt*Loc (halt SCM+FSA) by Th8
.= {} by SF_MASTR:36 ; :: thesis: verum