let a be Int-Location ; :: thesis: for f being FinSeq-Location
for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds
FirstNotUsed p <> a
let f be FinSeq-Location ; :: thesis: for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds
FirstNotUsed p <> a
let p be preProgram of SCM+FSA ; :: thesis: ( ( a :=len f in rng p or f :=<0,...,0> a in rng p ) implies FirstNotUsed p <> a )
assume ( a :=len f in rng p or f :=<0,...,0> a in rng p ) ; :: thesis: FirstNotUsed p <> a
then consider i being Instruction of SCM+FSA such that
A1: ( i in rng p & ( i = a :=len f or i = f :=<0,...,0> a ) ) ;
UsedIntLoc i = {a} by A1, Th22;
then ( {a} c= UsedIntLoc p & not FirstNotUsed p in UsedIntLoc p ) by A1, Th23, Th54;
hence FirstNotUsed p <> a by ZFMISC_1:37; :: thesis: verum