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

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

hence
not Reloc (I,n) destroys a
by SCMFSA7B:def 4; :: thesis: verumnot 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;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