let a, b be Int-Location ; :: thesis: for p being preProgram of SCM+FSA st ( a := b in rng p or AddTo a,b in rng p or SubFrom a,b in rng p or MultBy a,b in rng p or Divide a,b in rng p ) holds
( FirstNotUsed p <> a & FirstNotUsed p <> b )
let p be preProgram of SCM+FSA ; :: thesis: ( ( a := b in rng p or AddTo a,b in rng p or SubFrom a,b in rng p or MultBy a,b in rng p or Divide a,b in rng p ) implies ( FirstNotUsed p <> a & FirstNotUsed p <> b ) )
assume ( a := b in rng p or AddTo a,b in rng p or SubFrom a,b in rng p or MultBy a,b in rng p or Divide 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 and
A2: ( i = a := b or i = AddTo a,b or i = SubFrom a,b or i = MultBy a,b or i = Divide a,b ) ;
UsedIntLoc i = {a,b} by A2, Th18;
then A3: {a,b} c= UsedIntLoc p by A1, Th23;
not FirstNotUsed p in UsedIntLoc p by Th54;
hence ( FirstNotUsed p <> a & FirstNotUsed p <> b ) by A3, ZFMISC_1:38; :: thesis: verum