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