let b, a 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
( FirstNotUsed p <> a & FirstNotUsed p <> b )
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
( FirstNotUsed p <> a & FirstNotUsed p <> b )
let p be preProgram of SCM+FSA ; :: thesis: ( ( 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 ) ; :: thesis: ( FirstNotUsed p <> a & FirstNotUsed p <> b )
then consider i being Instruction of SCM+FSA such that
A1: ( i in rng p & ( i = b := f,a or i = f,a := b ) ) ;
UsedIntLoc i = {a,b} by A1, Th21;
then ( {a,b} c= UsedIntLoc p & not FirstNotUsed p in UsedIntLoc p ) by A1, Th23, Th54;
hence ( FirstNotUsed p <> a & FirstNotUsed p <> b ) by ZFMISC_1:38; :: thesis: verum