for i being Instruction of SCM+FSA holds
( ( i = halt SCM+FSA implies (Directed (Macro i)) . 0 = goto 2 ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) )