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, Th14;

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; :: thesis: verum

( 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, Th14;

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; :: thesis: verum