let a be Int-Location ; :: thesis: for l being Element of NAT
for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds
FirstNotUsed p <> a
let l be Element of NAT ; :: thesis: for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds
FirstNotUsed p <> a
let p be preProgram of SCM+FSA; :: thesis: ( ( a =0_goto l in rng p or a >0_goto l in rng p ) implies FirstNotUsed p <> a )
assume ( a =0_goto l in rng p or a >0_goto l in rng p ) ; :: thesis: FirstNotUsed p <> a
then consider i being Instruction of SCM+FSA such that
A1: i in rng p and
A2: ( i = a =0_goto l or i = a >0_goto l ) ;
UsedIntLoc i = {a} by A2, Th20;
then A3: {a} c= UsedIntLoc p by A1, Th23;
not FirstNotUsed p in UsedIntLoc p by Th54;
hence FirstNotUsed p <> a by A3, ZFMISC_1:31; :: thesis: verum