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