let p be autonomic halting FinPartState of SCM ; :: thesis: ( IC SCM in dom p implies for k being Element of NAT holds DataPart (Result (ProgramPart p),p) = DataPart (Result (Reloc (ProgramPart p),k),(Relocated p,k)) )
assume A1: IC SCM in dom p ; :: thesis: for k being Element of NAT holds DataPart (Result (ProgramPart p),p) = DataPart (Result (Reloc (ProgramPart p),k),(Relocated p,k))
let k be Element of NAT ; :: thesis: DataPart (Result (ProgramPart p),p) = DataPart (Result (Reloc (ProgramPart p),k),(Relocated p,k))
consider s being State of SCM such that
A2: p c= s by PBOOLE:156;
A3: ( Relocated p,k is halting & Relocated p,k is autonomic ) by A1, Th38, Th41;
ProgramPart s halts_on s by A2, AMI_1:def 26;
then consider j1 being Element of NAT such that
A4: Result (ProgramPart s),s = Comput (ProgramPart s),s,j1 and
A5: CurInstr (ProgramPart s),(Result (ProgramPart s),s) = halt SCM by AMI_1:def 22;
consider t being State of SCM such that
A6: Relocated p,k c= t by PBOOLE:156;
TY: ProgramPart t = ProgramPart (Comput (ProgramPart t),t,j1) by AMI_1:123;
U: IncAddr (halt SCM ),k = halt SCM by AMISTD_2:30;
Y: (ProgramPart (Comput (ProgramPart t),t,j1)) /. (IC (Comput (ProgramPart t),t,j1)) = (Comput (ProgramPart t),t,j1) . (IC (Comput (ProgramPart t),t,j1)) by COMPOS_1:38;
(ProgramPart t) . (IC (Comput (ProgramPart t),t,j1)) = t . (IC (Comput (ProgramPart t),t,j1)) by COMPOS_1:2
.= CurInstr (ProgramPart t),(Comput (ProgramPart t),t,j1) by Y, TY, AMI_1:54
.= IncAddr (CurInstr (ProgramPart s),(Comput (ProgramPart s),s,j1)),k by A1, A2, A6, Lm1
.= halt SCM by A4, A5, U, AMI_5:37 ;
then A7: Result (ProgramPart t),t = Comput (ProgramPart t),t,j1 by AMI_1:56;
A8: (Comput (ProgramPart t),t,j1) | (dom (DataPart (Relocated p,k))) = (Comput (ProgramPart s),s,j1) | (dom (DataPart p)) by A1, A2, A6, Lm1;
Reloc (ProgramPart p),k = ProgramPart (Relocated p,k) by AMISTD_2:69;
then X: Result (Reloc (ProgramPart p),k),(Relocated p,k) = (Result (ProgramPart t),t) | (dom (Relocated p,k)) by A6, A3, AMI_1:def 29;
thus DataPart (Result (ProgramPart p),p) = ((Result (ProgramPart s),s) | (dom p)) | SCM-Data-Loc by A2, AMI_1:def 29, AMI_3:72
.= (Result (ProgramPart s),s) | ((dom p) /\ SCM-Data-Loc ) by RELAT_1:100
.= (Result (ProgramPart s),s) | (dom (DataPart p)) by AMI_3:72, RELAT_1:90
.= (Result (ProgramPart t),t) | ((dom (Relocated p,k)) /\ SCM-Data-Loc ) by A4, A7, A8, AMI_3:72, RELAT_1:90
.= ((Result (ProgramPart t),t) | (dom (Relocated p,k))) | SCM-Data-Loc by RELAT_1:100
.= DataPart (Result (Reloc (ProgramPart p),k),(Relocated p,k)) by X, AMI_3:72 ; :: thesis: verum