let a, b be Int-Location; 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
( FirstNotUsed p <> a & FirstNotUsed p <> b )
let f be FinSeq-Location ; for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds
( FirstNotUsed p <> a & FirstNotUsed p <> b )
let p be preProgram of SCM+FSA; ( ( b := (f,a) in rng p or (f,a) := b in rng p ) implies ( FirstNotUsed p <> a & FirstNotUsed p <> b ) )
assume
( b := (f,a) in rng p or (f,a) := b in rng p )
; ( FirstNotUsed p <> a & FirstNotUsed p <> b )
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 )
;
UsedIntLoc i = {a,b}
by A2, Th17;
then A3:
{a,b} c= UsedILoc p
by A1, Th19;
not FirstNotUsed p in UsedILoc p
by Th50;
hence
( FirstNotUsed p <> a & FirstNotUsed p <> b )
by A3, ZFMISC_1:32; verum