theorem :: SCMFSA6A:22

for I being preProgram of SCM+FSA st I is halt-free holds
Directed I = I by FUNCT_4:103;