let N be with_zero set ; 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 b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic b2 -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; for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic b1 -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; 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; ( 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
; for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let k be Nat; 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
; verum