now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (a := k) implies b₁ does_not_destroy intloc 0 )
A1: rng (a := k) c= {(halt SCM+FSA ),(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))} by Th30;
assume A2: i in rng (a := k) ; :: thesis: b₁ does_not_destroy intloc 0

per cases ( i = halt SCM+FSA or i = a := (intloc 0 ) or i = AddTo a,(intloc 0 ) or i = SubFrom a,(intloc 0 ) ) by A2, A1, ENUMSET1:def 2;

suppose i = halt SCM+FSA ; :: thesis: b₁ does_not_destroy intloc 0

hence i does_not_destroy intloc 0 by Th11; :: thesis: verum

end;

suppose i = a := (intloc 0 ) ; :: thesis: b₁ does_not_destroy intloc 0

hence i does_not_destroy intloc 0 by Th12; :: thesis: verum

end;

suppose i = AddTo a,(intloc 0 ) ; :: thesis: b₁ does_not_destroy intloc 0

hence i does_not_destroy intloc 0 by Th13; :: thesis: verum

end;

suppose i = SubFrom a,(intloc 0 ) ; :: thesis: b₁ does_not_destroy intloc 0

hence i does_not_destroy intloc 0 by Th14; :: thesis: verum

end;

end;

end;

then a := k does_not_destroy intloc 0 by Def4;
hence a := k is good by Def5; :: thesis: verum