halt SCM+FSA <> goto l by SCMFSA_2:47, SCMFSA_2:124;
then not halt SCM+FSA in rng (Directed P,l) by FUNCT_4:106;
hence Directed P,l is halt-free by AMI_1:def 53; :: thesis: verum