let a be Int-Location; :: thesis: not Stop SCM+FSA destroys a
now :: thesis: for i being Instruction of SCM+FSA st i in rng (Stop SCM+FSA) holds
not i destroys a
let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Stop SCM+FSA) implies not i destroys a )
A1: rng (Stop SCM+FSA) = {(halt SCM+FSA)} by AFINSQ_1:33;
assume i in rng (Stop SCM+FSA) ; :: thesis: not i destroys a
then i = halt SCM+FSA by A1, TARSKI:def 1;
hence not i destroys a ; :: thesis: verum
end;
hence not Stop SCM+FSA destroys a ; :: thesis: verum