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

not i destroys intloc 0

then
not a := k destroys intloc 0
;not i destroys intloc 0

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (a := k) implies not b_{1} destroys intloc 0 )

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: not b_{1} destroys intloc 0

end;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: not b

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;

end;

hence a := k is good ; :: thesis: verum