let p be preProgram of SCM+FSA; for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for a being Int-Location st ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds
fa in UsedI*Loc p
let ic be Instruction of SCM+FSA; for fa being FinSeq-Location
for a being Int-Location st ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds
fa in UsedI*Loc p
let fa be FinSeq-Location ; for a being Int-Location st ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds
fa in UsedI*Loc p
let a be Int-Location; ( ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) implies fa in UsedI*Loc p )
assume that
A1:
ic in rng p
and
A2:
( ic = a :=len fa or ic = fa :=<0,...,0> a )
; fa in UsedI*Loc p
A3:
UsedInt*Loc ic = {fa}
by A2, SF_MASTR:34;
UsedInt*Loc ic c= UsedI*Loc p
by A1, SF_MASTR:35;
hence
fa in UsedI*Loc p
by A3, ZFMISC_1:31; verum