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

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