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 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 NPP p c= s holds
for P being the Instructions of b₁ -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving 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 NPP p c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),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 NPP p c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),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 NPP p c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k))
let p be autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st NPP p c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k)) )
assume A2: IC in dom p ; :: thesis: for s being State of S st NPP p c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k))
B2: IC in dom (NPP p) by A2, COMPOS_1:179;
let s be State of S; :: thesis: ( NPP p c= s implies for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k)) )
assume A4: NPP p c= s ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k))
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart p c= P implies for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k)) )
assume A5: ProgramPart p c= P ; :: thesis: for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k))
defpred S₁[ Element of NAT ] means NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),$1)) = NPP (IncIC ((Comput (P,s,$1)),k));
A6: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k)) ; :: thesis: S₁[i + 1]
reconsider kk = IC (Comput (P,s,i)) as Element of NAT ;
dom (Start-At (((IC (Comput (P,s,i))) + k),S)) = {(IC )} by FUNCOP_1:19;
then A8: IC in dom (Start-At (((IC (Comput (P,s,i))) + k),S)) by TARSKI:def 1;
A9: IC (IncIC ((Comput (P,s,i)),k)) = IC (Start-At (((IC (Comput (P,s,i))) + k),S)) by A8, FUNCT_4:14
.= (IC (Comput (P,s,i))) + k by FUNCOP_1:87 ;
not p is NAT -defined by A2, COMPOS_1:19;
then A11: IC (Comput (P,s,i)) in dom (ProgramPart p) by A5, Def4, A1, A4;
then A12: IC (Comput (P,s,i)) in dom (IncAddr ((ProgramPart p),k)) by COMPOS_1:def 40;
A17: (ProgramPart p) /. kk = (ProgramPart p) . (IC (Comput (P,s,i))) by A11, PARTFUN1:def 8
.= P . (IC (Comput (P,s,i))) by A11, A5, GRFUNC_1:8 ;
reconsider kk = IC (Comput (P,s,i)) as Element of NAT ;
XX: (IC (Comput (P,s,i))) + k in dom (Reloc ((ProgramPart p),k)) by A11, COMPOS_1:158;
X1: IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = IC (NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) by COMPOS_1:240;
X3: IC (IncIC ((Comput (P,s,i)),k)) = IC (NPP (IncIC ((Comput (P,s,i)),k))) by COMPOS_1:240;
A18: CurInstr ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) = (P +* (Reloc ((ProgramPart p),k))) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) by PBOOLE:158
.= (Reloc ((ProgramPart p),k)) . ((IC (Comput (P,s,i))) + k) by A7, A9, XX, FUNCT_4:14, X1, X3
.= (Shift ((IncAddr ((ProgramPart p),k)),k)) . ((IC (Comput (P,s,i))) + k) by COMPOS_1:159
.= (IncAddr ((ProgramPart p),k)) . kk by A12, VALUED_1:def 12
.= IncAddr (((ProgramPart p) /. kk),k) by A11, COMPOS_1:def 40
.= IncAddr ((CurInstr (P,(Comput (P,s,i)))),k) by A17, PBOOLE:158 ;
A19: ( Comput (P,s,(i + 1)) = Following (P,(Comput (P,s,i))) & NPP (Exec ((IncAddr ((CurInstr (P,(Comput (P,s,i)))),k)),(IncIC ((Comput (P,s,i)),k)))) = NPP (IncIC ((Following (P,(Comput (P,s,i)))),k)) ) by Th4, EXTPRO_1:4;
thus NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),(i + 1))) = NPP (Following ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)))) by EXTPRO_1:4
.= NPP (Exec ((IncAddr ((CurInstr (P,(Comput (P,s,i)))),k)),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)))) by A18
.= NPP (Exec ((IncAddr ((CurInstr (P,(Comput (P,s,i)))),k)),(IncIC ((Comput (P,s,i)),k)))) by A7, AMISTD_2:def 20
.= NPP (IncIC ((Following (P,(Comput (P,s,i)))),k)) by A19
.= NPP (IncIC ((Comput (P,s,(i + 1))),k)) by A19 ; :: thesis: verum

end;

A20: Comput (P,s,0) = s by EXTPRO_1:3;
A21: IC p = IC (NPP p) by A2, COMPOS_1:72
.= IC s by A4, B2, GRFUNC_1:8 ;
DataPart p c= NPP p by COMPOS_1:169;
then A22: DataPart p c= s by A4, XBOOLE_1:1;
Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0) = s +* (NPP (Relocated (p,k))) by EXTPRO_1:3
.= s +* (IncIC ((NPP p),k)) by A2, COMPOS_1:205
.= s +* ((DataPart p) +* (Start-At (((IC p) + k),S))) by A2, COMPOS_1:75
.= (s +* (DataPart p)) +* (Start-At (((IC p) + k),S)) by FUNCT_4:15
.= IncIC ((Comput (P,s,0)),k) by A21, A22, A20, FUNCT_4:104 ;
then A23: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A23, A6); :: thesis: verum