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
fa in UsedInt*Loc 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
fa in UsedInt*Loc 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
fa in UsedInt*Loc p
let b, a be Int-Location ; :: thesis: ( ic in rng p & ( ic = b := fa,a or ic = fa,a := b ) implies fa in UsedInt*Loc p )
assume A1: ( ic in rng p & ( ic = b := fa,a or ic = fa,a := b ) ) ; :: thesis: fa in UsedInt*Loc p
then A2: UsedInt*Loc ic = {fa} by SF_MASTR:37;
UsedInt*Loc ic c= UsedInt*Loc p by A1, SF_MASTR:39;
hence fa in UsedInt*Loc p by A2, ZFMISC_1:37; :: thesis: verum