theorem Th1: :: SFMASTR3:2

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (IExec ((Stop SCM+FSA),p,s)) = DataPart s