let p be preProgram of SCM+FSA; :: thesis: for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for b, a being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedIntLoc p & b in UsedIntLoc p )
let ic be Instruction of SCM+FSA; :: thesis: for fa being FinSeq-Location
for b, a being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedIntLoc p & b in UsedIntLoc p )
let fa be FinSeq-Location ; :: thesis: for b, a being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedIntLoc p & b in UsedIntLoc p )
let b, a be Int-Location ; :: thesis: ( ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) implies ( a in UsedIntLoc p & b in UsedIntLoc p ) )
assume that
A1: ic in rng p and
A2: ( ic = b := (fa,a) or ic = (fa,a) := b ) ; :: thesis: ( a in UsedIntLoc p & b in UsedIntLoc p )
A3: UsedIntLoc ic = {a,b} by A2, SF_MASTR:17;
UsedIntLoc ic c= UsedIntLoc p by A1, SF_MASTR:19;
hence ( a in UsedIntLoc p & b in UsedIntLoc p ) by A3, ZFMISC_1:32; :: thesis: verum