now :: thesis:

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

per cases by A2, A1, ENUMSET1:def 2;

suppose i = halt SCM+FSA ; :: thesis:

hence not i destroys intloc 0 ; :: thesis:

end;

suppose i = a := (intloc 0) ; :: thesis:

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

end;

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

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

end;

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

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

end;

end;

end;

then not a := k destroys intloc 0 ;
hence a := k is good ; :: thesis: