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 ProgramPart (Relocated (I,n)) destroys a
let n be Element of NAT ; :: thesis: for a being Int-Location st not I destroys a holds
not ProgramPart (Relocated (I,n)) destroys a
let a be Int-Location ; :: thesis: ( not I destroys a implies not ProgramPart (Relocated (I,n)) destroys a )
A1: ProgramPart (Relocated (I,n)) = Reloc ((ProgramPart I),n) by COMPOS_1:116
.= Reloc (I,n) by RELAT_1:209
.= Shift ((IncAddr (I,n)),n) by COMPOS_1:121 ;
A2: dom (IncAddr (I,n)) = dom I by COMPOS_1:def 40;
A3: dom (Shift ((IncAddr (I,n)),n)) = { (m + n) where m is Element of NAT : m in dom (IncAddr (I,n)) } by VALUED_1:def 12;
assume A4: not I destroys a ; :: thesis: not ProgramPart (Relocated (I,n)) destroys a

now

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (ProgramPart (Relocated (I,n))) implies not i destroys a )
assume i in rng (ProgramPart (Relocated (I,n))) ; :: thesis: not i destroys a
then consider x being set such that
A5: x in dom (Shift ((IncAddr (I,n)),n)) and
A6: i = (Shift ((IncAddr (I,n)),n)) . x by A1, FUNCT_1:def 5;
consider m being Element of NAT such that
A7: x = m + n and
A8: m in dom (IncAddr (I,n)) by A3, A5;
A9: I . m in rng I by A2, A8, FUNCT_1:def 5;
rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
then reconsider ii = I . m as Instruction of SCM+FSA by A9;
A10: not ii destroys a by A4, A9, SCMFSA7B:def 4;
i = (IncAddr (I,n)) . m by A6, A7, A8, VALUED_1:def 12
.= IncAddr ((I /. m),n) by A2, A8, COMPOS_1:def 40
.= IncAddr (ii,n) by A2, A8, PARTFUN1:def 8 ;
hence not i destroys a by A10, Th22; :: thesis: verum

end;

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