let p be preProgram of SCM+FSA ; :: thesis: 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
a in UsedIntLoc p
let ic be Instruction of SCM+FSA ; :: thesis: 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
a in UsedIntLoc p
let fa be FinSeq-Location ; :: thesis: for a being Int-Location st ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) holds
a in UsedIntLoc p
let a be Int-Location ; :: thesis: ( ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) implies a in UsedIntLoc p )
assume A1: ( ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) ) ; :: thesis: a in UsedIntLoc p
then A2: UsedIntLoc ic = {a} by SF_MASTR:22;
UsedIntLoc ic c= UsedIntLoc p by A1, SF_MASTR:23;
hence a in UsedIntLoc p by A2, ZFMISC_1:37; :: thesis: verum