let N be non empty with_non-empty_elements set ; :: thesis: for S being standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized relocable1 AMI-Struct of N st S is relocable1 & S is relocable2 & S is CurIns-recognized & S is proper-halt holds
for q being NAT -defined the Instructions of b₁ -valued finite non halt-free Function
for p being non empty b₂ -autonomic b₂ -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let S be standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized relocable1 AMI-Struct of N; :: thesis: ( S is relocable1 & S is relocable2 & S is CurIns-recognized & S is proper-halt implies for q being NAT -defined the Instructions of S -valued finite non halt-free Function
for p being non empty b₁ -autonomic b₁ -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) )
assume A1: ( S is relocable1 & S is relocable2 & S is CurIns-recognized & S is proper-halt ) ; :: thesis: for q being NAT -defined the Instructions of S -valued finite non halt-free Function
for p being non empty b₁ -autonomic b₁ -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let q be NAT -defined the Instructions of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic q -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let p be non empty q -autonomic q -halted FinPartState of S; :: thesis: ( IC in dom p implies for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) )
assume A2: IC in dom p ; :: thesis: for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let k be Element of NAT ; :: thesis: DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
consider s being State of S such that
A4: p c= s by PBOOLE:141;
consider P being Instruction-Sequence of S such that
C4: q c= P by PBOOLE:145;
B4: p c= s by A4;
A6: ( IncIC (p,k) is Reloc (q,k) -halted & IncIC (p,k) is Reloc (q,k) -autonomic ) by A2, Th12, Th11, A1;
A7: IncIC (p,k) is Autonomy of Reloc (q,k) by A6, EXTPRO_1:def 12;
P halts_on s by B4, C4, EXTPRO_1:def 11;
then consider j1 being Element of NAT such that
A8: Result (P,s) = Comput (P,s,j1) and
A9: CurInstr (P,(Result (P,s))) = halt S by EXTPRO_1:def 9;
consider t being State of S such that
A10: IncIC (p,k) c= t by PBOOLE:141;
consider Q being Instruction-Sequence of S such that
C10: Reloc (q,k) c= Q by PBOOLE:145;
B10: IncIC (p,k) c= t by A10;
Q . (IC (Comput (Q,t,j1))) = CurInstr (Q,(Comput (Q,t,j1))) by PBOOLE:143
.= IncAddr ((CurInstr (P,(Comput (P,s,j1)))),k) by A2, Def5, C4, C10, B4, B10
.= halt S by A8, A9, COMPOS_1:11 ;
then A12: Result (Q,t) = Comput (Q,t,j1) by EXTPRO_1:7;
A13: (Comput (Q,t,j1)) | (dom (DataPart p)) = (Comput (P,s,j1)) | (dom (DataPart p)) by A2, A1, Def6, C10, C4, B10, B4;
DPDP: DataPart p = DataPart (IncIC (p,k)) by MEMSTR_0:51;
aa: p is Autonomy of q by EXTPRO_1:def 12;
thus DataPart (Result (q,p)) = DataPart ((Result (P,s)) | (dom p)) by A4, C4, aa, 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 A8, A12, A13, DPDP, 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 A7, C10, B10, EXTPRO_1:def 13 ; :: thesis: verum