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
UsedIntLoc i = {a,b}
let f be FinSeq-Location ; :: thesis: for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds
UsedIntLoc i = {a,b}
let i be Instruction of SCM+FSA; :: thesis: ( ( i = b := (f,a) or i = (f,a) := b ) implies UsedIntLoc i = {a,b} )
reconsider ab = {a,b} as Element of Fin Int-Locations by FINSUB_1:def 5;
assume A1: ( i = b := (f,a) or i = (f,a) := b ) ; :: thesis: UsedIntLoc i = {a,b}
then ( InsCode i = 9 or InsCode i = 10 ) by SCMFSA_2:26, SCMFSA_2:27;
then UsedIntLoc i = ab by A1, Def1;
hence UsedIntLoc i = {a,b} ; :: thesis: verum