theorem Th11: :: SCMBSORT:12

for p being 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