dom (Directed (I,0)) = dom I by FUNCT_4:105;
then Directed (I,0) <> {} ;
hence Directed (I,0) is halt-free Program of SCM+FSA ; :: thesis: verum