let a, b be Int-Location; :: thesis: for f being FinSeq-Location
for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds
First*NotUsed p <> f
let f be FinSeq-Location ; :: thesis: for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds
First*NotUsed p <> f
let p be preProgram of SCM+FSA; :: thesis: ( ( b := (f,a) in rng p or (f,a) := b in rng p ) implies First*NotUsed p <> f )
assume ( b := (f,a) in rng p or (f,a) := b in rng p ) ; :: thesis: First*NotUsed p <> f
then consider i being Instruction of SCM+FSA such that
A1: i in rng p and
A2: ( i = b := (f,a) or i = (f,a) := b ) ;
UsedInt*Loc i = {f} by A2, Th33;
then A3: {f} c= UsedI*Loc p by A1, Th35;
not First*NotUsed p in UsedI*Loc p by Th57;
hence First*NotUsed p <> f by A3, ZFMISC_1:31; :: thesis: verum