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 k being Element of NAT
for p being FinPartState of S st IC in dom p holds
NPP (Relocated (p,k)) = IncIC ((NPP p),k)
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 k being Element of NAT
for p being FinPartState of S st IC in dom p holds
NPP (Relocated (p,k)) = IncIC ((NPP p),k)
let k be Element of NAT ; :: thesis: for p being FinPartState of S st IC in dom p holds
NPP (Relocated (p,k)) = IncIC ((NPP p),k)
let p be FinPartState of S; :: thesis: ( IC in dom p implies NPP (Relocated (p,k)) = IncIC ((NPP p),k) )
assume Z: IC in dom p ; :: thesis: NPP (Relocated (p,k)) = IncIC ((NPP p),k)
A: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:19
.= dom (Start-At (((IC p) + k),S)) by FUNCOP_1:19 ;
IC in dom (Relocated (p,k)) by Th119;
hence NPP (Relocated (p,k)) = (DataPart (Relocated (p,k))) +* (Start-At ((IC (Relocated (p,k))),S)) by Th74
.= (DataPart p) +* (Start-At ((IC (Relocated (p,k))),S)) by Th115
.= (DataPart p) +* (Start-At (((IC p) + k),S)) by Z, Th120
.= ((DataPart p) +* (Start-At ((IC p),S))) +* (Start-At (((IC p) + k),S)) by A, FUNCT_4:78
.= (NPP p) +* (Start-At (((IC p) + k),S)) by Z, Th74
.= (NPP p) +* (Start-At (((IC (NPP p)) + k),S)) by Z, Th72
.= IncIC ((NPP p),k) ;
:: thesis: verum