let p be preProgram of SCM+FSA ; :: thesis: for ic being Instruction of SCM+FSA
for a, b being Int-Location st ic in rng p & ( ic = a := b or ic = AddTo a,b or ic = SubFrom a,b or ic = MultBy a,b or ic = Divide a,b ) holds
( a in UsedIntLoc p & b in UsedIntLoc p )
let ic be Instruction of SCM+FSA ; :: thesis: for a, b being Int-Location st ic in rng p & ( ic = a := b or ic = AddTo a,b or ic = SubFrom a,b or ic = MultBy a,b or ic = Divide a,b ) holds
( a in UsedIntLoc p & b in UsedIntLoc p )
let a, b be Int-Location ; :: thesis: ( ic in rng p & ( ic = a := b or ic = AddTo a,b or ic = SubFrom a,b or ic = MultBy a,b or ic = Divide a,b ) implies ( a in UsedIntLoc p & b in UsedIntLoc p ) )
assume A1: ( ic in rng p & ( ic = a := b or ic = AddTo a,b or ic = SubFrom a,b or ic = MultBy a,b or ic = Divide a,b ) ) ; :: thesis: ( a in UsedIntLoc p & b in UsedIntLoc p )
then A2: UsedIntLoc ic = {a,b} by SF_MASTR:18;
UsedIntLoc ic c= UsedIntLoc p by A1, SF_MASTR:23;
hence ( a in UsedIntLoc p & b in UsedIntLoc p ) by A2, ZFMISC_1:38; :: thesis: verum