:: deftheorem Def8 defines First*NotUsed SF_MASTR:def 9 :
for p being preProgram of SCM+FSA
for b₂ being FinSeq-Location holds
( b₂ = First*NotUsed p iff ex sil being finite Subset of FinSeq-Locations st
( sil = UsedI*Loc p & b₂ = First*NotIn sil ) );