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 (Relocated (p,k)) c= s holds
for P being the Instructions of b1 -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),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 (Relocated (p,k)) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),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 (Relocated (p,k)) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),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 (Relocated (p,k)) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k))
let p be autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st NPP (Relocated (p,k)) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k)) )
assume A2: IC in dom p ; :: thesis: for s being State of S st NPP (Relocated (p,k)) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k))
B2: IC in dom (NPP p) by A2, COMPOS_1:179;
let s be State of S; :: thesis: ( NPP (Relocated (p,k)) c= s implies for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k)) )
assume A4: NPP (Relocated (p,k)) c= s ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k))
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( Reloc ((ProgramPart p),k) c= P implies for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k)) )
assume A5: Reloc ((ProgramPart p),k) c= P ; :: thesis: for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k))
defpred S1[ Element of NAT ] means NPP (Comput (P,s,$1)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),$1)),k));
A6: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set sdom = s | (dom (ProgramPart p));
dom (ProgramPart p) c= the carrier of S by RELAT_1:def 18;
then dom (ProgramPart p) c= dom s by PARTFUN1:def 4;
then dom (ProgramPart p) = dom (s | (dom (ProgramPart p))) by RELAT_1:91;
then ( rng (s | (dom (ProgramPart p))) c= the Instructions of S & dom (s | (dom (ProgramPart p))) c= NAT ) by COMPOS_1:32, RELAT_1:87;
then reconsider sdom = s | (dom (ProgramPart p)) as NAT -defined FinPartState of by RELSET_1:11;
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A7: NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k)) ; :: thesis: S1[i + 1]
reconsider kk = IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)) as Element of NAT ;
dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) + k),S)) = {(IC )} by FUNCOP_1:19;
then A8: IC in dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) + k),S)) by TARSKI:def 1;
A10: NPP p c= s +* (NPP p) by FUNCT_4:26;
A11: ProgramPart p c= P +* (ProgramPart p) by FUNCT_4:26;
not p is NAT -defined by A2, COMPOS_1:19;
then A12: IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)) in dom (ProgramPart p) by A1, Def4, A10, A11;
then A13: IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)) in dom (IncAddr ((ProgramPart p),k)) by COMPOS_1:def 40;
A14: (IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) + k in dom (Reloc ((ProgramPart p),k)) by A12, COMPOS_1:158;
reconsider kk = IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)) as Element of NAT ;
A15: IC (Comput (P,s,i)) = IC (NPP (Comput (P,s,i))) by COMPOS_1:240
.= IC (NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k))) by A7
.= IC (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k)) by COMPOS_1:240
.= IC (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) + k),S)) by A8, FUNCT_4:14
.= (IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) + k by FUNCOP_1:87 ;
A16: ProgramPart p c= P +* (ProgramPart p) by FUNCT_4:26;
A17: (ProgramPart p) /. kk = (ProgramPart p) . kk by A12, PARTFUN1:def 8;
A18: dom (P +* (ProgramPart p)) = NAT by PARTFUN1:def 4;
dom P = NAT by PARTFUN1:def 4;
then A19: CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PARTFUN1:def 8
.= (Reloc ((ProgramPart p),k)) . (IC (Comput (P,s,i))) by A5, A14, A15, GRFUNC_1:8
.= (Shift ((IncAddr ((ProgramPart p),k)),k)) . ((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) + k) by A15, COMPOS_1:159
.= (IncAddr ((ProgramPart p),k)) . kk by A13, VALUED_1:def 12
.= IncAddr (((ProgramPart p) /. kk),k) by A12, COMPOS_1:def 40
.= IncAddr (((P +* (ProgramPart p)) . (IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),k) by A12, A17, A16, GRFUNC_1:8
.= IncAddr ((CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),k) by A18, PARTFUN1:def 8 ;
A20: Comput ((P +* (ProgramPart p)),(s +* (NPP p)),(i + 1)) = Following ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i))) by EXTPRO_1:4;
thus NPP (Comput (P,s,(i + 1))) = NPP (Following (P,(Comput (P,s,i)))) by EXTPRO_1:4
.= NPP (Exec ((IncAddr ((CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),k)),(Comput (P,s,i)))) by A19
.= NPP (Exec ((IncAddr ((CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),k)),(IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k)))) by A7, AMISTD_2:def 20
.= NPP (IncIC ((Exec ((CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),k)) by Th4
.= NPP (IncIC ((Following ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)))),k))
.= NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),(i + 1))),k)) by A20 ; :: thesis: verum
end;
set IP = Start-At ((IC p),S);
A21: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:19;
B22: Start-At (((IC p) + k),S) c= NPP (Relocated (p,k)) by A2, COMPOS_1:123, COMPOS_1:216;
IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0)) = (s +* (NPP p)) . (IC ) by EXTPRO_1:3
.= IC (NPP p) by B2, FUNCT_4:14
.= IC p by A2, COMPOS_1:72 ;
then A23: Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S) c= s by A4, B22, XBOOLE_1:1;
set DP = DataPart p;
DataPart (Relocated (p,k)) c= NPP (Relocated (p,k)) by COMPOS_1:217, RELAT_1:88;
then DataPart (Relocated (p,k)) c= s by A4, XBOOLE_1:1;
then A29: DataPart p c= s by COMPOS_1:115;
set PR = Reloc ((ProgramPart p),k);
set IS = Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S);
A30: dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S)) = {(IC )} by FUNCOP_1:19;
Comput (P,s,0) = s by EXTPRO_1:3
.= s +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S)) by A23, FUNCT_4:104
.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S)) by A29, FUNCT_4:104
.= ((s +* (DataPart p)) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S)) by A30, A21, FUNCT_4:78
.= (s +* ((DataPart p) +* (Start-At ((IC p),S)))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S)) by FUNCT_4:15
.= (s +* (NPP p)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0))) + k),S)) by A2, COMPOS_1:74
.= IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),0)),k) by EXTPRO_1:3 ;
then A31: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A31, A6); :: thesis: verum