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 UsedILoc 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 UsedILoc 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 UsedILoc p
let a be Int-Location; :: thesis: ( ic in rng p & ( ic = a :=len fa or ic = fa :=<0,...,0> a ) implies a in UsedILoc p )
assume that
A1: ic in rng p and
A2: ( ic = a :=len fa or ic = fa :=<0,...,0> a ) ; :: thesis: a in UsedILoc p
A3: UsedIntLoc ic = {a} by A2, SF_MASTR:18;
UsedIntLoc ic c= UsedILoc p by A1, SF_MASTR:19;
hence a in UsedILoc p by A3, ZFMISC_1:31; :: thesis: verum