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