let i be Instruction of SCM+FSA; :: thesis: ( not i destroys intloc 0 implies Macro i is good )

set I = Macro i;

A1: rng (Macro i) = {i,(halt SCM+FSA)} by COMPOS_1:67;

assume A2: not i destroys intloc 0 ; :: thesis: Macro i is good

hence Macro i is good by SCMFSA7B:def 5; :: thesis: verum

set I = Macro i;

A1: rng (Macro i) = {i,(halt SCM+FSA)} by COMPOS_1:67;

assume A2: not i destroys intloc 0 ; :: thesis: Macro i is good

now :: thesis: for x being Instruction of SCM+FSA st x in rng (Macro i) holds

not x destroys intloc 0

then
not Macro i destroys intloc 0
by SCMFSA7B:def 4;not x destroys intloc 0

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

assume A3: x in rng (Macro i) ; :: thesis: not b_{1} destroys intloc 0

end;assume A3: x in rng (Macro i) ; :: thesis: not b

hence Macro i is good by SCMFSA7B:def 5; :: thesis: verum