let I be Program of SCM+FSA ; :: thesis: not halt SCM+FSA in rng (Directed I)
halt SCM+FSA <> goto (insloc (card I)) by SCMFSA_2:47, SCMFSA_2:124;
hence not halt SCM+FSA in rng (Directed I) by FUNCT_4:106; :: thesis: verum