theorem :: SCMFSA8A:23

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
Directed I is_pseudo-closed_on s,P by Lm2;