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 s . (intloc 0) = 1 holds
FinSeqMin (f,aa,bb,c) is_halting_on s,p