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