:: deftheorem defines Directed SCMFSA6A:def 1 :
for P being preProgram of SCM+FSA holds Directed P = P +~ ((halt SCM+FSA),(goto (card P)));