dom (Directed (I,0)) = dom I by FUNCT_4:99;
hence Directed (I,0) is halt-free Program of SCM+FSA ; :: thesis: verum