let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat holds (Goto k) ";" I = (Macro (goto k)) ';' I
let k be Nat; :: thesis: (Goto k) ";" I = (Macro (goto k)) ';' I
rng (Goto k) = {(goto k)} by AFINSQ_1:33;
then not halt SCM+FSA in rng (Goto k) by TARSKI:def 1;
then Directed (Goto k) = Goto k by FUNCT_4:103;
hence (Goto k) ";" I = (Macro (goto k)) ';' I ; :: thesis: verum