let a, b be Int-Location; 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 ; 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; ( ( i = b := (f,a) or i = (f,a) := b ) implies UsedInt*Loc i = {f} )
f in FinSeq-Locations
by SCMFSA_2:def 5;
then
{f} c= FinSeq-Locations
by ZFMISC_1:31;
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 )
; UsedInt*Loc i = {f}
then
( InsCode i = 9 or InsCode i = 10 )
by SCMFSA_2:26, SCMFSA_2:27;
then
UsedInt*Loc i = ab
by A1, Def4;
hence
UsedInt*Loc i = {f}
; verum