let a, b 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: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 ) ; :: thesis: 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} ; :: thesis: verum

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: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 ) ; :: thesis: 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} ; :: thesis: verum