let I be preProgram of SCM+FSA ; for n being Element of NAT
for a being Int-Location st not I destroysdestroy a holds
not ProgramPart (Relocated I,n) destroysdestroy a
let n be Element of NAT ; for a being Int-Location st not I destroysdestroy a holds
not ProgramPart (Relocated I,n) destroysdestroy a
let a be Int-Location ; ( not I destroysdestroy a implies not ProgramPart (Relocated I,n) destroysdestroy a )
A1: ProgramPart (Relocated I,n) =
Reloc (ProgramPart I),n
by AMISTD_2:69
.=
Reloc I,n
by RELAT_1:209
.=
Shift (IncAddr I,n),n
by AMISTD_2:75
;
A2:
dom (IncAddr I,n) = dom I
by AMISTD_2:def 15;
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 destroysdestroy a
; not ProgramPart (Relocated I,n) destroysdestroy a
now let i be
Instruction of
SCM+FSA ;
( i in rng (ProgramPart (Relocated I,n)) implies not i destroysdestroy a )assume
i in rng (ProgramPart (Relocated I,n))
;
not i destroysdestroy athen 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 destroysdestroy 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, AMISTD_2:def 15
.=
IncAddr ii,
n
by A2, A8, PARTFUN1:def 8
;
hence
not
i destroysdestroy a
by A10, Th22;
verum end;
hence
not ProgramPart (Relocated I,n) destroysdestroy a
by SCMFSA7B:def 4; verum