theorem :: SCMFSA7B:2

for i being Instruction of SCM+FSA holds (Directed (Macro i)) . 1 = goto 2