not halt SCM+FSA in rng (Directed P,l) by FUNCT_4:106;
hence Directed P,l is halt-free by COMPOS_1:def 7; :: thesis: verum