let p be preProgram of ; :: thesis: for ic being Instruction of
for a being Int-Location
for la being Instruction-Location of SCM+FSA st ic in rng p & ( ic = a =0_goto la or ic = a >0_goto la ) holds
a in UsedIntLoc p
let ic be Instruction of ; :: thesis: for a being Int-Location
for la being Instruction-Location of SCM+FSA st ic in rng p & ( ic = a =0_goto la or ic = a >0_goto la ) holds
a in UsedIntLoc p
let a be Int-Location ; :: thesis: for la being Instruction-Location of SCM+FSA st ic in rng p & ( ic = a =0_goto la or ic = a >0_goto la ) holds
a in UsedIntLoc p
let la be Instruction-Location of SCM+FSA ; :: thesis: ( ic in rng p & ( ic = a =0_goto la or ic = a >0_goto la ) implies a in UsedIntLoc p )
assume that
A1: ic in rng p and
A2: ( ic = a =0_goto la or ic = a >0_goto la ) ; :: thesis: a in UsedIntLoc p
A3: UsedIntLoc ic = {a} by A2, SF_MASTR:20;
UsedIntLoc ic c= UsedIntLoc p by A1, SF_MASTR:23;
hence a in UsedIntLoc p by A3, ZFMISC_1:37; :: thesis: verum