let i be Instruction of SCM+FSA; :: thesis: for a being Int-Location st not i refers a holds
not Macro i refers a
let a be Int-Location; :: thesis: ( not i refers a implies not Macro i refers a )
A1: rng (Macro i) = {i,(halt SCM+FSA)} by COMPOS_1:67;
assume not i refers a ; :: thesis: not Macro i refers a
then for ii being Instruction of SCM+FSA st ii in rng (Macro i) holds
not ii refers a by A1, TARSKI:def 2;
hence not Macro i refers a ; :: thesis: verum