let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N

for q being NAT -defined the InstructionsF of b_{1} -valued finite non halt-free Function

for p being non empty b_{2} -autonomic b_{2} -halted FinPartState of S st IC in dom p holds

for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

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: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b_{1} -autonomic b_{1} -halted FinPartState of S st IC in dom p holds

for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

let q be NAT -defined the InstructionsF 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 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 Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) )

assume A1: IC in dom p ; :: thesis: for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

let k be Nat; :: thesis: DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

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: verum

for q being NAT -defined the InstructionsF of b

for p being non empty b

for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

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: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b

for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

let q be NAT -defined the InstructionsF 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 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 Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) )

assume A1: IC in dom p ; :: thesis: for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

let k be Nat; :: thesis: DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

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: verum