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 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 homogeneous regular J/A-independent COM-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 Th51;
dom s c= Data-Locations S by Th31;
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 Th66
.= (IncrIC (((NPP g) +* s),k)) +* (Reloc ((ProgramPart g),k)) by Th67
.= ((IncrIC ((NPP g),k)) +* s) +* (Reloc ((ProgramPart g),k)) by Th60
.= (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