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 UsedILoc p & b in UsedILoc 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 UsedILoc p & b in UsedILoc 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 UsedILoc p & b in UsedILoc p ) )
assume that
A1: ic in rng p and
A2: ( 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 UsedILoc p & b in UsedILoc p )
A3: UsedIntLoc ic = {a,b} by A2, SF_MASTR:14;
UsedIntLoc ic c= UsedILoc p by A1, SF_MASTR:19;
hence ( a in UsedILoc p & b in UsedILoc p ) by A3, ZFMISC_1:32; :: thesis: verum