let I be preProgram of SCM+FSA ; for n being Element of NAT
for a being Int-Location st I does_not_destroy a holds
ProgramPart (Relocated I,n) does_not_destroy a
let n be Element of NAT ; for a being Int-Location st I does_not_destroy a holds
ProgramPart (Relocated I,n) does_not_destroy a
let a be Int-Location ; ( I does_not_destroy a implies ProgramPart (Relocated I,n) does_not_destroy a )
A1: ProgramPart (Relocated I,n) =
IncAddr (Shift (ProgramPart I),n),n
by SCMFSA_5:2
.=
IncAddr (Shift I,n),n
by AMI_1:105
.=
Shift (IncAddr I,n),n
by SCMFSA_4:35
;
A2:
dom (IncAddr I,n) = dom I
by SCMFSA_4:def 6;
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:
I does_not_destroy a
; ProgramPart (Relocated I,n) does_not_destroy a
now let i be
Instruction of
SCM+FSA ;
( i in rng (ProgramPart (Relocated I,n)) implies i does_not_destroy a )assume
i in rng (ProgramPart (Relocated I,n))
;
i does_not_destroy 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 AMI_1:118;
then reconsider ii =
I . m as
Instruction of
SCM+FSA by A9;
A10:
ii does_not_destroy a
by A4, A9, SCMFSA7B:def 4;
i =
(IncAddr I,n) . m
by A6, A7, A8, VALUED_1:def 12
.=
IncAddr (pi I,m),
n
by A2, A8, SCMFSA_4:def 6
.=
IncAddr ii,
n
by A2, A8, AMI_1:def 47
;
hence
i does_not_destroy a
by A10, Th22;
verum end;
hence
ProgramPart (Relocated I,n) does_not_destroy a
by SCMFSA7B:def 4; verum