let a be Int-Location ; :: thesis: for i being Instruction of SCM+FSA st i = a :==1 holds
UsedInt*Loc i = {}
let i be Instruction of SCM+FSA; :: thesis: ( i = a :==1 implies UsedInt*Loc i = {} )
assume i = a :==1 ; :: thesis: UsedInt*Loc i = {}
then InsCode i = 13 by SCMFSA_2:137;
then UsedInt*Loc i = {} by Def3;
hence UsedInt*Loc i = {} ; :: thesis: verum