let a be Int-Location; :: thesis: for l being Nat

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

reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def 5;

assume A1: ( i = a =0_goto l or i = a >0_goto l ) ; :: thesis: UsedIntLoc i = {a}

then ( InsCode i = 7 or InsCode i = 8 ) by SCMFSA_2:24, SCMFSA_2:25;

then UsedIntLoc i = ab by A1, Def1;

hence UsedIntLoc i = {a} ; :: thesis: verum

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

reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def 5;

assume A1: ( i = a =0_goto l or i = a >0_goto l ) ; :: thesis: UsedIntLoc i = {a}

then ( InsCode i = 7 or InsCode i = 8 ) by SCMFSA_2:24, SCMFSA_2:25;

then UsedIntLoc i = ab by A1, Def1;

hence UsedIntLoc i = {a} ; :: thesis: verum