let I be preProgram of SCM+FSA ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( I does_not_destroy a implies [(ProgramPart (Relocated I,n))] does_not_destroy a )
assume A1:
I does_not_destroy a
; :: thesis: [(ProgramPart (Relocated I,n))] does_not_destroy a
A2: 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
;
A3:
dom (IncAddr I,n) = dom I
by SCMFSA_4:def 6;
A4:
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;
now let i be
Instruction of
SCM+FSA ;
:: thesis: ( i in rng (ProgramPart (Relocated I,n)) implies i does_not_destroy a )assume
i in rng (ProgramPart (Relocated I,n))
;
:: thesis: 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 A2, 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 A4, A5;
A9:
I . (insloc m) in rng I
by A3, A8, FUNCT_1:def 5;
rng I c= the
Instructions of
SCM+FSA
by AMI_1:118;
then reconsider ii =
I . (insloc m) as
Instruction of
SCM+FSA by A9;
A10:
ii does_not_destroy a
by A1, A9, SCMFSA7B:def 4;
i =
(IncAddr I,n) . (insloc m)
by A6, A7, A8, VALUED_1:def 12
.=
IncAddr (pi I,m),
n
by A3, A8, SCMFSA_4:def 6
.=
IncAddr ii,
n
by A3, A8, AMI_1:def 47
;
hence
i does_not_destroy a
by A10, Th22;
:: thesis: verum end;
hence
[(ProgramPart (Relocated I,n))] does_not_destroy a
by SCMFSA7B:def 4; :: thesis: verum