let I be preProgram of SCM+FSA; :: thesis: for n being Element of NAT
for a being Int-Location st not I destroys a holds
not Reloc (I,n) destroys a

let n be Element of NAT ; :: thesis: for a being Int-Location st not I destroys a holds
not Reloc (I,n) destroys a

let a be Int-Location; :: thesis: ( not I destroys a implies not Reloc (I,n) destroys a )
A1: dom (IncAddr (I,n)) = dom I by COMPOS_1:def 21;
A2: dom (Shift ((IncAddr (I,n)),n)) = { (m + n) where m is Nat : m in dom (IncAddr (I,n)) } by VALUED_1:def 12;
assume A3: not I destroys a ; :: thesis: not Reloc (I,n) destroys a
now :: thesis: for i being Instruction of SCM+FSA st i in rng (Reloc (I,n)) holds
not i destroys a
let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Reloc (I,n)) implies not i destroys a )
assume i in rng (Reloc (I,n)) ; :: thesis: not i destroys a
then consider x being object such that
A4: x in dom (Shift ((IncAddr (I,n)),n)) and
A5: i = (Shift ((IncAddr (I,n)),n)) . x by FUNCT_1:def 3;
consider m being Nat such that
A6: x = m + n and
A7: m in dom (IncAddr (I,n)) by A2, A4;
A8: I . m in rng I by ;
rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
then reconsider ii = I . m as Instruction of SCM+FSA by A8;
A9: not ii destroys a by ;
i = (IncAddr (I,n)) . m by
.= IncAddr ((I /. m),n) by
.= IncAddr (ii,n) by ;
hence not i destroys a by ; :: thesis: verum
end;
hence not Reloc (I,n) destroys a by SCMFSA7B:def 4; :: thesis: verum