theorem Th16: :: SCMFSA8C:24

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )