let a be Int-Location ; :: thesis: for f being FinSeq-Location
for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds
UsedIntLoc i = {a}
let f be FinSeq-Location ; :: thesis: for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds
UsedIntLoc i = {a}
let i be Instruction of SCM+FSA; :: thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) implies UsedIntLoc i = {a} )
a in Int-Locations by SCMFSA_2:2;
then {a} c= Int-Locations by ZFMISC_1:31;
then reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def 5;
assume A1: ( i = a :=len f or i = f :=<0,...,0> a ) ; :: thesis: UsedIntLoc i = {a}
then ( InsCode i = 11 or InsCode i = 12 ) by SCMFSA_2:28, SCMFSA_2:29;
then UsedIntLoc i = ab by A1, Def1;
hence UsedIntLoc i = {a} ; :: thesis: verum