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 FinPartState of S st IC in dom p holds
for s being State of S st NPP p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of b1 -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),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 FinPartState of S st IC in dom p holds
for s being State of S st NPP p c= s & Relocated (p,k) is autonomic 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) )
assume A1: S is CurIns-recognized ; :: thesis: for k being Element of NAT
for p being FinPartState of S st IC in dom p holds
for s being State of S st NPP p c= s & Relocated (p,k) is autonomic 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k))
let k be Element of NAT ; :: thesis: for p being FinPartState of S st IC in dom p holds
for s being State of S st NPP p c= s & Relocated (p,k) is autonomic 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k))
let p be FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st NPP p c= s & Relocated (p,k) is autonomic 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) )
RE: Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;
assume A3: IC in dom p ; :: thesis: for s being State of S st NPP p c= s & Relocated (p,k) is autonomic 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k))
then B4: Start-At ((IC p),S) c= NPP p by COMPOS_1:216, FUNCOP_1:99;
let s be State of S; :: thesis: ( NPP p c= s & Relocated (p,k) is autonomic 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) )
assume that
A5: NPP p c= s and
A6: Relocated (p,k) is autonomic ; :: 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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),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,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) )
assume A7: ProgramPart p c= P ; :: thesis: for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k))
A8: Start-At ((IC p),S) c= s by A5, B4, XBOOLE_1:1;
defpred S1[ Element of NAT ] means NPP (Comput (P,s,$1)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),$1)),k));
A9: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp = ProgramPart p as preProgram of S ;
set sdom = s | (dom (Reloc ((ProgramPart p),k)));
dom (Reloc ((ProgramPart p),k)) c= the carrier of S by RELAT_1:def 18;
then dom (Reloc ((ProgramPart p),k)) c= dom s by PARTFUN1:def 4;
then dom (Reloc ((ProgramPart p),k)) = dom (s | (dom (Reloc ((ProgramPart p),k)))) by RELAT_1:91;
then ( rng (s | (dom (Reloc ((ProgramPart p),k)))) c= the Instructions of S & dom (s | (dom (Reloc ((ProgramPart p),k)))) c= NAT ) by RE, COMPOS_1:32, RELAT_1:87;
then reconsider sdom = s | (dom (Reloc ((ProgramPart p),k))) as NAT -defined FinPartState of by RELSET_1:11;
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A10: NPP (Comput (P,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) ; :: thesis: S1[i + 1]
reconsider kk = IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) as Element of NAT ;
reconsider jk = IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) as Element of NAT ;
A11: NPP (Relocated (p,k)) c= s +* (NPP (Relocated (p,k))) by FUNCT_4:26;
A12: Reloc ((ProgramPart p),k) c= P +* (Reloc ((ProgramPart p),k)) by FUNCT_4:26;
IC in dom (Relocated (p,k)) by COMPOS_1:119;
then not Relocated (p,k) is NAT -defined by COMPOS_1:19;
then A13: IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) in dom (Reloc ((ProgramPart p),k)) by A6, A1, Def4, A11, A12, RE;
then A14: jk in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by COMPOS_1:117;
dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) -' k),S)) = {(IC )} by FUNCOP_1:19;
then A16: IC in dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) -' k),S)) by TARSKI:def 1;
consider j being Element of NAT such that
A17: jk = j + k and
A18: j in dom (ProgramPart p) by A14;
A19: dom (P +* (Reloc ((ProgramPart p),k))) = NAT by PARTFUN1:def 4;
A20: Reloc ((ProgramPart p),k) c= P +* (Reloc ((ProgramPart p),k)) by FUNCT_4:26;
dom (Shift (pp,k)) = { (m + k) where m is Element of NAT : m in dom pp } by VALUED_1:def 12;
then A21: j + k in dom (Shift ((ProgramPart p),k)) by A18;
then A22: IncAddr (((Shift ((ProgramPart p),k)) /. kk),k) = (Reloc ((ProgramPart p),k)) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) by A17, COMPOS_1:def 40
.= (P +* (Reloc ((ProgramPart p),k))) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) by A13, A20, GRFUNC_1:8
.= CurInstr ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) by A19, PARTFUN1:def 8 ;
A23: (j + k) -' k = j by NAT_D:34;
A24: dom P = NAT by PARTFUN1:def 4;
X1: IC (NPP (Comput (P,s,i))) = IC (Comput (P,s,i)) by COMPOS_1:240;
X2: IC (NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k))) = IC (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) by COMPOS_1:240;
A25: IC (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)) = (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) -' k),S)) . (IC ) by A16, FUNCT_4:14
.= (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) -' k by FUNCOP_1:87 ;
CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by A24, PARTFUN1:def 8
.= (ProgramPart p) . (IC (Comput (P,s,i))) by A10, A17, A18, A23, A7, A25, GRFUNC_1:8, X1, X2
.= (Shift ((ProgramPart p),k)) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) by A17, A18, A23, A10, A25, VALUED_1:def 12, X1, X2
.= (Shift ((ProgramPart p),k)) /. kk by A17, A21, PARTFUN1:def 8 ;
then A26: ( Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),(i + 1)) = Following ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i))) & NPP (Exec ((CurInstr (P,(Comput (P,s,i)))),(DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k)))) = NPP (DecIC ((Following ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)))),k)) ) by A17, A22, Th5, EXTPRO_1:4;
thus NPP (Comput (P,s,(i + 1))) = NPP (Following (P,(Comput (P,s,i)))) by EXTPRO_1:4
.= NPP (DecIC ((Following ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)))),k)) by A10, A26, AMISTD_2:def 20
.= NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),(i + 1))),k)) by A26 ; :: thesis: verum
end;
A27: IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B27: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;
A28: IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0)) = (s +* (NPP (Relocated (p,k)))) . (IC ) by EXTPRO_1:3
.= IC (NPP (Relocated (p,k))) by B27, FUNCT_4:14
.= IC (Relocated (p,k)) by A27, COMPOS_1:72 ;
DataPart p c= NPP p by COMPOS_1:217, RELAT_1:88;
then A29: DataPart p c= s by A5, XBOOLE_1:1;
set DP = DataPart p;
set IP = Start-At (((IC p) + k),S);
set PP = ProgramPart p;
set IS = Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S);
A32: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:19;
set PR = Reloc ((ProgramPart p),k);
set SD = s | (dom (Reloc ((ProgramPart p),k)));
A33: {(IC )} misses dom (DataPart p) by COMPOS_1:13;
A36: dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S)) = {(IC )} by FUNCOP_1:19;
A41: dom (Start-At (((IC p) + k),S)) misses dom (DataPart p) by A33, FUNCOP_1:19;
A42: (Start-At (((IC p) + k),S)) +* (DataPart p) = (DataPart p) +* (Start-At (((IC p) + k),S)) by A41, FUNCT_4:36
.= IncIC ((NPP p),k) by A3, COMPOS_1:75
.= NPP (Relocated (p,k)) by A3, COMPOS_1:205 ;
Comput (P,s,0) = s by EXTPRO_1:3
.= s +* (Start-At ((IC p),S)) by A8, FUNCT_4:104
.= s +* (Start-At ((((IC p) + k) -' k),S)) by NAT_D:34
.= s +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S)) by A28, A3, COMPOS_1:120
.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S)) by A29, FUNCT_4:104
.= ((s +* (DataPart p)) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S)) by A36, A32, FUNCT_4:78
.= (s +* ((DataPart p) +* (Start-At (((IC p) + k),S)))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S)) by FUNCT_4:15
.= (s +* ((Start-At (((IC p) + k),S)) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0))) -' k),S)) by A32, A33, FUNCT_4:36
.= DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),0)),k) by A42, EXTPRO_1:3 ;
then A43: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A43, A9); :: thesis: verum