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 k being Element of NAT
for q being data-only FinPartState of S holds Relocated (g +* q),k = (Relocated g,k) +* q
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 k being Element of NAT
for q being data-only FinPartState of S holds Relocated (g +* q),k = (Relocated g,k) +* q
let g be FinPartState of S; :: thesis: for k being Element of NAT
for q being data-only FinPartState of S holds Relocated (g +* q),k = (Relocated g,k) +* q
let k be Element of NAT ; :: thesis: for q being data-only FinPartState of S holds Relocated (g +* q),k = (Relocated g,k) +* q
let s be data-only FinPartState of S; :: thesis: Relocated (g +* s),k = (Relocated g,k) +* s
A: NAT misses Data-Locations S by COMPOS_1:51;
dom s c= Data-Locations S by COMPOS_1:31;
then Y: dom s misses NAT by A, XBOOLE_1:63;
XX: dom (Reloc (ProgramPart g),k) c= NAT by RELAT_1:def 18;
thus Relocated (g +* s),k = (IncrIC (NPP (g +* s)),k) +* (Reloc (ProgramPart (g +* s)),k)
.= (IncrIC (NPP (g +* s)),k) +* (Reloc (ProgramPart g),k) by COMPOS_1:66
.= (IncrIC ((NPP g) +* s),k) +* (Reloc (ProgramPart g),k) by COMPOS_1:67
.= ((IncrIC (NPP g),k) +* s) +* (Reloc (ProgramPart g),k) by COMPOS_1:60
.= (IncrIC (NPP g),k) +* (s +* (Reloc (ProgramPart g),k)) by FUNCT_4:15
.= (IncrIC (NPP g),k) +* ((Reloc (ProgramPart g),k) +* s) by XX, Y, FUNCT_4:36, XBOOLE_1:63
.= ((IncrIC (NPP g),k) +* (Reloc (ProgramPart g),k)) +* s by FUNCT_4:15
.= (Relocated g,k) +* s ; :: thesis: verum