not 0 in {1,2,3,4,5} ;
hence UsedIntLoc (halt SCM+FSA ) = {} by Def1, SCMFSA_2:124; :: thesis: verum