let a be Int-Location; :: thesis: for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

First*NotUsed p <> f

let f be FinSeq-Location ; :: thesis: for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

First*NotUsed p <> f

let p be preProgram of SCM+FSA; :: thesis: ( ( a :=len f in rng p or f :=<0,...,0> a in rng p ) implies First*NotUsed p <> f )

assume ( a :=len f in rng p or f :=<0,...,0> a in rng p ) ; :: thesis: First*NotUsed p <> f

then consider i being Instruction of SCM+FSA such that

A1: i in rng p and

A2: ( i = a :=len f or i = f :=<0,...,0> a ) ;

UsedInt*Loc i = {f} by A2, Th34;

then A3: {f} c= UsedI*Loc p by A1, Th35;

not First*NotUsed p in UsedI*Loc p by Th57;

hence First*NotUsed p <> f by A3, ZFMISC_1:31; :: thesis: verum

for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

First*NotUsed p <> f

let f be FinSeq-Location ; :: thesis: for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

First*NotUsed p <> f

let p be preProgram of SCM+FSA; :: thesis: ( ( a :=len f in rng p or f :=<0,...,0> a in rng p ) implies First*NotUsed p <> f )

assume ( a :=len f in rng p or f :=<0,...,0> a in rng p ) ; :: thesis: First*NotUsed p <> f

then consider i being Instruction of SCM+FSA such that

A1: i in rng p and

A2: ( i = a :=len f or i = f :=<0,...,0> a ) ;

UsedInt*Loc i = {f} by A2, Th34;

then A3: {f} c= UsedI*Loc p by A1, Th35;

not First*NotUsed p in UsedI*Loc p by Th57;

hence First*NotUsed p <> f by A3, ZFMISC_1:31; :: thesis: verum