for a being Int-Location
for l being Nat
for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds
FirstNotUsed p <> a