let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for il, k being Element of NAT
for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for g being FinPartState of S
for il, k being Element of NAT
for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k)
let g be FinPartState of S; :: thesis: for il, k being Element of NAT
for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k)
let il, k be Element of NAT ; :: thesis: for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k)
let I be Instruction of S; :: thesis: ( il in dom (ProgramPart g) & I = g . il implies IncAddr I,k = (Relocated g,k) . (il + k) )
assume that
A2: il in dom (ProgramPart g) and
A3: I = g . il ; :: thesis: IncAddr I,k = (Relocated g,k) . (il + k)
A4: ProgramPart g c= g by RELAT_1:88;
consider i being natural number such that
A5: il = i ;
reconsider ii = il as Element of NAT ;
i + k in { (j + k) where j is Element of NAT : j in dom (ProgramPart g) } by A2, A5;
then il + k in dom (Reloc (ProgramPart g),k) by A5, Th70;
then A6: il + k in dom (ProgramPart (Relocated g,k)) by Th69;
A7: il in dom (IncAddr (ProgramPart g),k) by A2, Def15;
A8: I = (ProgramPart g) . il by A2, A3, A4, GRFUNC_1:8;
ProgramPart (Relocated g,k) c= Relocated g,k by RELAT_1:88;
hence (Relocated g,k) . (il + k) = (ProgramPart (Relocated g,k)) . (il + k) by A6, GRFUNC_1:8
.= (IncAddr (Shift (ProgramPart g),k),k) . (il + k) by Th69
.= (Shift (IncAddr (ProgramPart g),k),k) . (il + k) by Th75
.= (IncAddr (ProgramPart g),k) . il by A7, VALUED_1:def 12
.= IncAddr ((ProgramPart g) /. ii),k by A2, Def15
.= IncAddr I,k by A2, A8, PARTFUN1:def 8 ;
:: thesis: verum