:: deftheorem Def7 defines FirstNotUsed SF_MASTR:def 7 :
for p being preProgram of SCM+FSA
for b₂ being Int-Location holds
( b₂ = FirstNotUsed p iff ex sil being finite Subset of Int-Locations st
( sil = (UsedILoc p) \/ {(intloc 0)} & b₂ = FirstNotIn sil ) );