theorem :: SCMFSA6A:1

for I being Program of holds not halt SCM+FSA in rng (Directed I) by FUNCT_4:100;