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