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