theorem Th29: :: SFMASTR3:31

for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|)