let I be preProgram of SCM+FSA; 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 ; for a being Int-Location st not I destroys a holds
not Reloc (I,n) destroys a
let a be Int-Location; ( 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
; not Reloc (I,n) destroys a
now for i being Instruction of SCM+FSA st i in rng (Reloc (I,n)) holds
not i destroys alet i be
Instruction of
SCM+FSA;
( i in rng (Reloc (I,n)) implies not i destroys a )assume
i in rng (Reloc (I,n))
;
not i destroys athen 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;
verum end;
hence
not Reloc (I,n) destroys a
by SCMFSA7B:def 4; verum