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