set I = Load (goto l);
not halt SCM+FSA in rng (Load (goto l)) by Lm1;
hence Goto l is halt-free ; :: thesis: Goto l is good
now :: thesis: for x being Instruction of SCM+FSA st x in rng (Load (goto l)) holds
not x destroys intloc 0
let x be Instruction of SCM+FSA; :: thesis: ( x in rng (Load (goto l)) implies not x destroys intloc 0 )
A1: rng (Load (goto l)) = {(goto l)} by AFINSQ_1:33;
assume x in rng (Load (goto l)) ; :: thesis: not x destroys intloc 0
then x = goto l by A1, TARSKI:def 1;
hence not x destroys intloc 0 by SCMFSA7B:11; :: thesis: verum
end;
then not Load (goto l) destroys intloc 0 by SCMFSA7B:def 4;
hence Goto l is good by SCMFSA7B:def 5; :: thesis: verum