let a be Int-Location; 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 ; 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; ( ( 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 )
; FirstNotUsed p <> a
then consider i being Instruction of SCM+FSA such that
A1:
i in rng p
and
A2:
( i = a :=len f or i = f :=<0,...,0> a )
;
UsedIntLoc i = {a}
by A2, Th18;
then A3:
{a} c= UsedILoc p
by A1, Th19;
not FirstNotUsed p in UsedILoc p
by Th50;
hence
FirstNotUsed p <> a
by A3, ZFMISC_1:31; verum