let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving steady-programmed relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving steady-programmed relocable IC-recognized AMI-Struct of N; :: thesis: ( S is CurIns-recognized implies for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k)) )
assume A1: S is CurIns-recognized ; :: thesis: for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k))
let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k))
let p be autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st p c= s holds
for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k)) )
assume A2: IC in dom p ; :: thesis: for s being State of S st p c= s holds
for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k))
let s be State of S; :: thesis: ( p c= s implies for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k)) )
assume A4: p c= s ; :: thesis: for i being Element of NAT holds Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k))
A5: ProgramPart p c= ProgramPart s by A4, RELAT_1:105;
defpred S1[ Element of NAT ] means Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),$1) = (IncIC ((Comput ((ProgramPart s),s,$1)),k)) +* (Reloc ((ProgramPart p),k));
A6: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A7: Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i) = (IncIC ((Comput ((ProgramPart s),s,i)),k)) +* (Reloc ((ProgramPart p),k)) ; :: thesis: S1[i + 1]
reconsider kk = IC (Comput ((ProgramPart s),s,i)) as Element of NAT ;
dom (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),S)) = {(IC )} by FUNCOP_1:19;
then A8: IC in dom (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),S)) by TARSKI:def 1;
Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;
then not IC in dom (Reloc ((ProgramPart p),k)) by COMPOS_1:12;
then A9: IC (((Comput ((ProgramPart s),s,i)) +* (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),S))) +* (Reloc ((ProgramPart p),k))) = ((Comput ((ProgramPart s),s,i)) +* (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),S))) . (IC ) by FUNCT_4:12
.= (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),S)) . (IC ) by A8, FUNCT_4:14
.= (IC (Comput ((ProgramPart s),s,i))) + k by FUNCOP_1:87 ;
A10: ProgramPart p c= Comput ((ProgramPart s),s,i) by A4, AMI_1:99;
not p is NAT -defined by A2, COMPOS_1:19;
then A11: IC (Comput ((ProgramPart s),s,i)) in dom (ProgramPart p) by A4, A5, Def4, A1;
then A12: IC (Comput ((ProgramPart s),s,i)) in dom (IncAddr ((ProgramPart p),k)) by COMPOS_1:def 40;
A13: ProgramPart (s +* (Relocated (p,k))) = ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) by AMI_1:123;
A14: (ProgramPart (s +* (Relocated (p,k)))) /. (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) = (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) by A13, COMPOS_1:38;
A15: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i)) by AMI_1:123;
A16: (ProgramPart s) /. (IC (Comput ((ProgramPart s),s,i))) = (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by A15, COMPOS_1:38;
A17: (ProgramPart p) /. kk = (ProgramPart p) . (IC (Comput ((ProgramPart s),s,i))) by A11, PARTFUN1:def 8
.= (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by A11, A10, GRFUNC_1:8 ;
reconsider kk = IC (Comput ((ProgramPart s),s,i)) as Element of NAT ;
(IC (Comput ((ProgramPart s),s,i))) + k in dom (Reloc ((ProgramPart p),k)) by A11, COMPOS_1:158;
then A18: CurInstr ((ProgramPart (s +* (Relocated (p,k)))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) = (Reloc ((ProgramPart p),k)) . ((IC (Comput ((ProgramPart s),s,i))) + k) by A7, A9, A14, FUNCT_4:14
.= (Shift ((IncAddr ((ProgramPart p),k)),k)) . ((IC (Comput ((ProgramPart s),s,i))) + k) by COMPOS_1:159
.= (IncAddr ((ProgramPart p),k)) . kk by A12, VALUED_1:def 12
.= IncAddr ((CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,i)))),k) by A11, A17, A16, COMPOS_1:def 40 ;
A19: ( Comput ((ProgramPart s),s,(i + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,i))) & Exec ((IncAddr ((CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,i)))),k)),(IncIC ((Comput ((ProgramPart s),s,i)),k))) = IncIC ((Following ((ProgramPart s),(Comput ((ProgramPart s),s,i)))),k) ) by Th4, EXTPRO_1:4;
thus Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),(i + 1)) = Following ((ProgramPart (s +* (Relocated (p,k)))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) by EXTPRO_1:4
.= (IncIC ((Comput ((ProgramPart s),s,(i + 1))),k)) +* (Reloc ((ProgramPart p),k)) by A7, A18, A19, AMI_1:127 ; :: thesis: verum
end;
A20: Comput ((ProgramPart s),s,0) = s by EXTPRO_1:3;
A21: IC p = IC s by A2, A4, GRFUNC_1:8;
DataPart p c= p by RELAT_1:88;
then A22: DataPart p c= s by A4, XBOOLE_1:1;
Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0) = s +* ((IncIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k))) by EXTPRO_1:3
.= s +* (((DataPart p) +* (Start-At (((IC p) + k),S))) +* (Reloc ((ProgramPart p),k))) by A2, COMPOS_1:75
.= s +* ((DataPart p) +* ((Start-At (((IC p) + k),S)) +* (Reloc ((ProgramPart p),k)))) by FUNCT_4:15
.= (s +* (DataPart p)) +* ((Start-At (((IC p) + k),S)) +* (Reloc ((ProgramPart p),k))) by FUNCT_4:15
.= ((s +* (DataPart p)) +* (Start-At (((IC p) + k),S))) +* (Reloc ((ProgramPart p),k)) by FUNCT_4:15
.= ((Comput ((ProgramPart s),s,0)) +* (Start-At (((IC (Comput ((ProgramPart s),s,0))) + k),S))) +* (Reloc ((ProgramPart p),k)) by A21, A22, A20, FUNCT_4:79 ;
then A23: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A23, A6); :: thesis: verum