Stop SCM+FSA = (insloc 0 ) .--> (halt SCM+FSA ) ;
hence UsedIntLoc (Stop SCM+FSA ) = {} by Th7, SF_MASTR:17; :: thesis: verum