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