let p be autonomic halting FinPartState of SCM+FSA ; :: thesis: ( IC SCM+FSA in dom p implies for k being Element of NAT holds DataPart (Result (ProgramPart p),p) = DataPart (Result (ProgramPart (Relocated p,k)),(Relocated p,k)) )
assume A1: IC SCM+FSA in dom p ; :: thesis: for k being Element of NAT holds DataPart (Result (ProgramPart p),p) = DataPart (Result (ProgramPart (Relocated p,k)),(Relocated p,k))
let k be Element of NAT ; :: thesis: DataPart (Result (ProgramPart p),p) = DataPart (Result (ProgramPart (Relocated p,k)),(Relocated p,k))
consider s being State of SCM+FSA such that
A2: p c= s by PBOOLE:156;
A3: Relocated p,k is autonomic by A1, Th16;
A4: Relocated p,k is halting by A1, Th13;
ProgramPart s halts_on s by A2, AMI_1:def 26;
then consider j1 being Element of NAT such that
A5: Result (ProgramPart s),s = Comput (ProgramPart s),s,j1 and
A6: CurInstr (ProgramPart s),(Result (ProgramPart s),s) = halt SCM+FSA by AMI_1:def 22;
consider t being State of SCM+FSA such that
A7: Relocated p,k c= t by PBOOLE:156;
(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 COMPOS_1:38
.= IncAddr (CurInstr (ProgramPart s),(Comput (ProgramPart s),s,j1)),k by A1, A2, A7, Th12
.= halt SCM+FSA by A5, A6, SCMFSA_4:8 ;
then A8: Result (ProgramPart t),t = Comput (ProgramPart t),t,j1 by AMI_1:56;
thus DataPart (Result (ProgramPart p),p) = DataPart ((Result (ProgramPart s),s) | (dom p)) by A2, AMI_1:def 29
.= (Result (ProgramPart s),s) | ((dom p) /\ (Int-Locations \/ FinSeq-Locations )) by RELAT_1:100, SCMFSA_2:127
.= (Result (ProgramPart s),s) | (dom (DataPart p)) by RELAT_1:90, SCMFSA_2:127
.= (Result (ProgramPart t),t) | (dom (DataPart (Relocated p,k))) by A1, A2, A5, A7, A8, Th12
.= (Result (ProgramPart t),t) | ((dom (Relocated p,k)) /\ (Int-Locations \/ FinSeq-Locations )) by RELAT_1:90, SCMFSA_2:127
.= DataPart ((Result (ProgramPart t),t) | (dom (Relocated p,k))) by RELAT_1:100, SCMFSA_2:127
.= DataPart (Result (ProgramPart (Relocated p,k)),(Relocated p,k)) by A7, A4, A3, AMI_1:def 29 ; :: thesis: verum
reconsider s3 = s +* (DataPart t) as State of SCM+FSA ;