let s be data-only FinPartState of SCM; :: thesis: for p being FinPartState of SCM
for k being Element of NAT holds Relocated ((p +* s),k) = (Relocated (p,k)) +* s
let p be FinPartState of SCM; :: thesis: for k being Element of NAT holds Relocated ((p +* s),k) = (Relocated (p,k)) +* s
let k be Element of NAT ; :: thesis: Relocated ((p +* s),k) = (Relocated (p,k)) +* s
dom s c= Data-Locations SCM by COMPOS_1:31;
then Y: dom s misses NAT by AMI_2:29, AMI_3:72, XBOOLE_1:63;
X: dom (Reloc ((ProgramPart p),k)) c= NAT by RELAT_1:def 18;
thus Relocated ((p +* s),k) = (IncrIC ((NPP (p +* s)),k)) +* (Reloc ((ProgramPart (p +* s)),k))
.= (IncrIC ((NPP (p +* s)),k)) +* (Reloc ((ProgramPart p),k)) by COMPOS_1:66
.= (IncrIC (((NPP p) +* s),k)) +* (Reloc ((ProgramPart p),k)) by COMPOS_1:67
.= ((IncrIC ((NPP p),k)) +* s) +* (Reloc ((ProgramPart p),k)) by COMPOS_1:60
.= (IncrIC ((NPP p),k)) +* (s +* (Reloc ((ProgramPart p),k))) by FUNCT_4:15
.= (IncrIC ((NPP p),k)) +* ((Reloc ((ProgramPart p),k)) +* s) by X, FUNCT_4:36, Y, XBOOLE_1:63
.= ((IncrIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k))) +* s by FUNCT_4:15
.= (Relocated (p,k)) +* s ; :: thesis: verum