let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N; :: thesis:
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis:
let p be non empty q -autonomic q -halted FinPartState of S; :: thesis:
assume A1: IC in dom p ; :: thesis:
let k be Nat; :: thesis:
consider s being State of S such that
A2: p c= s by PBOOLE:141;
consider P being Instruction-Sequence of S such that
A3: q c= P by PBOOLE:145;
A4: ( IncIC (p,k) is Reloc (q,k) -halted & IncIC (p,k) is Reloc (q,k) -autonomic ) by A1, Th12, Th11;
A5: IncIC (p,k) is Autonomy of Reloc (q,k) by A4, EXTPRO_1:def 12;
P halts_on s by A2, A3, EXTPRO_1:def 11;
then consider j1 being Nat such that
A6: Result (P,s) = Comput (P,s,j1) and
A7: CurInstr (P,(Result (P,s))) = halt S by EXTPRO_1:def 9;
consider t being State of S such that
A8: IncIC (p,k) c= t by PBOOLE:141;
consider Q being Instruction-Sequence of S such that
A9: Reloc (q,k) c= Q by PBOOLE:145;
Q . (IC (Comput (Q,t,j1))) = CurInstr (Q,(Comput (Q,t,j1))) by PBOOLE:143
.= IncAddr ((CurInstr (P,(Comput (P,s,j1)))),k) by Def5, A3, A9, A2, A8
.= halt S by A6, A7, COMPOS_0:4 ;
then A10: Result (Q,t) = Comput (Q,t,j1) by EXTPRO_1:7;
A11: (Comput (Q,t,j1)) | (dom (DataPart p)) = (Comput (P,s,j1)) | (dom (DataPart p)) by Def6, A9, A3, A8, A2;
A12: DataPart p = DataPart (IncIC (p,k)) by MEMSTR_0:51;
A13: p is Autonomy of q by EXTPRO_1:def 12;
thus DataPart (Result (q,p)) = DataPart ((Result (P,s)) | (dom p)) by A2, A3, A13, EXTPRO_1:def 13
.= (Result (P,s)) | ((dom p) /\ (Data-Locations )) by RELAT_1:71
.= (Result (P,s)) | (dom (DataPart p)) by MEMSTR_0:14
.= (Result (Q,t)) | ((dom (IncIC (p,k))) /\ (Data-Locations )) by A6, A10, A11, A12, MEMSTR_0:14
.= ((Result (Q,t)) | (dom (IncIC (p,k)))) | (Data-Locations ) by RELAT_1:71
.= DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) by A5, A9, A8, EXTPRO_1:def 13 ; :: thesis: