:: deftheorem defines -thNotUsed SFMASTR1:def 4 :
for n being Element of NAT
for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedILoc p);