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= SCM-Data-Loc by AMI_3:72, COMPOS_1:31;
then Y: dom s misses NAT by AMI_2:29, XBOOLE_1:63;
dom (Reloc (ProgramPart p),k) c= NAT by RELAT_1:def 18;
then X: dom (Reloc (ProgramPart p),k) misses dom s by Y, XBOOLE_1:63;
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
.= ((IncrIC (NPP p),k) +* (Reloc (ProgramPart p),k)) +* s by FUNCT_4:15
.= (Relocated p,k) +* s ; :: thesis: verum