now :: thesis: for i being Instruction of SCM+FSA st i in rng (a := k) holds
not i destroys intloc 0

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (a := k) implies not b₁ destroys intloc 0 )
A1: rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by Th23;
assume A2: i in rng (a := k) ; :: thesis: not b₁ destroys 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: not b₁ destroys intloc 0

hence not i destroys intloc 0 by Th5; :: thesis: verum

end;

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

hence not i destroys intloc 0 by Th6; :: thesis: verum

end;

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

hence not i destroys intloc 0 by Th7; :: thesis: verum

end;

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

hence not i destroys intloc 0 by Th8; :: thesis: verum

end;

end;

end;

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