let b, a be Int-Location ; :: thesis: for f being FinSeq-Location
for i being Instruction of SCM+FSA st ( i = b := f,a or i = f,a := b ) holds
UsedInt*Loc i = {f}
let f be FinSeq-Location ; :: thesis: for i being Instruction of SCM+FSA st ( i = b := f,a or i = f,a := b ) holds
UsedInt*Loc i = {f}
let i be Instruction of SCM+FSA ; :: thesis: ( ( i = b := f,a or i = f,a := b ) implies UsedInt*Loc i = {f} )
f in FinSeq-Locations by SCMFSA_2:10;
then {f} c= FinSeq-Locations by ZFMISC_1:37;
then reconsider ab = {f} as Element of Fin FinSeq-Locations by FINSUB_1:def 5;
assume A1: ( i = b := f,a or i = f,a := b ) ; :: thesis: UsedInt*Loc i = {f}
then ( InsCode i = 9 or InsCode i = 10 ) by SCMFSA_2:50, SCMFSA_2:51;
then UsedInt*Loc i = ab by A1, Def3;
hence UsedInt*Loc i = {f} ; :: thesis: verum