let i be No-StopCode Instruction of SCM+FSA; :: thesis: Directed (Macro i) = (Macro i) ';' (Goto 1)
set A = {i,(halt SCM+FSA)};
A1: card (Macro i) = 2 by COMPOS_1:56;
then (card (Macro i)) - 1 = 1 ;
then A2: (card (Macro i)) -' 1 = 1 by XREAL_0:def 2;
A3: card (Load i) = 1 by AFINSQ_1:34;
A4: i <> halt SCM+FSA by COMPOS_0:def 12;
rng (Load i) = {i} by AFINSQ_1:33;
then not halt SCM+FSA in rng (Load i) by TARSKI:def 1, A4;
then A5: (Load i) +~ ((halt SCM+FSA),(goto 2)) = CutLastLoc (Macro i) by FUNCT_4:103;
A6: (Shift ((Stop SCM+FSA),1)) +~ ((halt SCM+FSA),(goto 2)) = Shift (((Stop SCM+FSA) +~ ((halt SCM+FSA),(goto 2))),1) by VALUED_1:67
.= Shift (<%(goto (1 + 1))%>,1) by AFINSQ_1:90
.= Reloc ((Goto 1),1) by SCMFSA8A:44 ;
thus Directed (Macro i) = ((Load i) +* (Shift ((Stop SCM+FSA),1))) +~ ((halt SCM+FSA),(goto 2)) by A3, AFINSQ_1:77, A1
.= (Macro i) ';' (Goto 1) by A5, A6, A2, FUNCT_7:117 ; :: thesis: verum