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 homogeneous regular J/A-independent COM-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 homogeneous regular J/A-independent COM-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