let l be Element of NAT ; :: thesis: for p being l -started non program-free autonomic halting FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k))))
let p be l -started non program-free 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;
ProgramPart s halts_on s by A2, EXTPRO_1:def 10;
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 EXTPRO_1:def 8;
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 EXTPRO_1:8;
(Relocated (p,k)) +* (ProgramPart (Relocated (p,k))) = Relocated (p,k) by FUNCT_4:80;
then XX: Relocated (p,k) is Autonomy of ProgramPart (Relocated (p,k)) by A3, EXTPRO_1:def 11;
p +* (ProgramPart p) = p by FUNCT_4:80;
then p is Autonomy of ProgramPart p by EXTPRO_1:def 11;
hence DataPart (Result ((ProgramPart p),p)) = DataPart ((Result ((ProgramPart s),s)) | (dom p)) by A2, EXTPRO_1:def 12
.= (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, EXTPRO_1:def 12, XX ;
:: thesis: verum
reconsider s3 = s +* (DataPart t) as State of SCM+FSA ;