let a be Int-Location ; :: thesis: for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds
UsedIntLoc i = {a}
let l be Instruction-Location of SCM+FSA ; :: thesis: for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds
UsedIntLoc i = {a}
let i be Instruction of SCM+FSA ; :: thesis: ( ( i = a =0_goto l or i = a >0_goto l ) implies UsedIntLoc i = {a} )
assume A1: ( i = a =0_goto l or i = a >0_goto l ) ; :: thesis: UsedIntLoc i = {a}
a in Int-Locations by SCMFSA_2:9;
then {a} c= Int-Locations by ZFMISC_1:37;
then reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def 5;
( InsCode i = 7 or InsCode i = 8 ) by A1, SCMFSA_2:48, SCMFSA_2:49;
then UsedIntLoc i = ab by A1, Def1;
hence UsedIntLoc i = {a} ; :: thesis: verum