let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
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 N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
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 standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
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 being Instruction-Location of S st S is realistic holds
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 be Instruction-Location of S; :: thesis: ( S is realistic implies for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k) )
assume A1: S is realistic ; :: 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 A2: ( il in dom (ProgramPart g) & I = g . il ) ; :: thesis: IncAddr I,k = (Relocated g,k) . (il + k)
A3: ProgramPart g c= g by RELAT_1:88;
consider i being natural number such that
A4: il = il. S,i by AMISTD_1:26;
reconsider ii = il as Element of NAT by ORDINAL1:def 13;
i is Element of NAT by ORDINAL1:def 13;
then il. S,(i + k) in { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) } by A2, A4;
then il. S,(i + k) in dom (ProgramPart (Relocated g,k)) by A1, Th49;
then A5: il + k in dom (ProgramPart (Relocated g,k)) by A4, AMISTD_1:def 13;
A6: il in dom (IncAddr (ProgramPart g),k) by A2, Def15;
A7: I = (ProgramPart g) . il by A2, A3, 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 A5, GRFUNC_1:8
.= (IncAddr (Shift (ProgramPart g),k),k) . (il + k) by A1, Th48
.= (Shift (IncAddr (ProgramPart g),k),k) . (il + k) by Th54
.= (IncAddr (ProgramPart g),k) . il by A6, Th65
.= IncAddr (pi (ProgramPart g),ii),k by A2, Th53
.= IncAddr I,k by A2, A7, AMI_1:def 47 ;
:: thesis: verum