let a be Int-Location; :: thesis: for l being 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 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, Th16;

then A3: {a} c= UsedILoc p by A1, Th19;

not FirstNotUsed p in UsedILoc p by Th50;

hence FirstNotUsed p <> a by A3, ZFMISC_1:31; :: thesis: verum

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 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, Th16;

then A3: {a} c= UsedILoc p by A1, Th19;

not FirstNotUsed p in UsedILoc p by Th50;

hence FirstNotUsed p <> a by A3, ZFMISC_1:31; :: thesis: verum