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 A1, A7, FUNCT_1:def 3;
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 A3, A8, SCMFSA7B:def 4;
i = (IncAddr (I,n)) . m by A5, A6, A7, VALUED_1:def 12
.= IncAddr ((I /. m),n) by A1, A7, COMPOS_1:def 21
.= IncAddr (ii,n) by A1, A7, PARTFUN1:def 6 ;
hence not i destroys a by A9, Th1; :: thesis: verum

end;

hence not Reloc (I,n) destroys a by SCMFSA7B:def 4; :: thesis: verum