let k be Element of NAT ; :: thesis: for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
let p be FinPartState of SCM+FSA ; :: thesis: ( IC SCM+FSA in dom p implies for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) )
assume Z: IC SCM+FSA in dom p ; :: thesis: for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
then A1: Start-At (IC p),SCM+FSA c= p by FUNCOP_1:99;
let s be State of SCM+FSA ; :: thesis: ( p c= s & Relocated p,k is autonomic implies for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) )
assume that
A2: p c= s and
A3: Relocated p,k is autonomic ; :: thesis: for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
A4: Start-At (IC p),SCM+FSA c= s by A2, A1, XBOOLE_1:1;
defpred S1[ Nat] means Comput (ProgramPart s),s,$1 = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),$1) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),$1)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p);
A5: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp = ProgramPart p as preProgram of SCM+FSA ;
set sdom = s | (dom (ProgramPart (Relocated p,k)));
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A6: Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) ; :: thesis: S1[i + 1]
dom (ProgramPart (Relocated p,k)) c= the carrier of SCM+FSA by RELAT_1:def 18;
then dom (ProgramPart (Relocated p,k)) c= dom s by PARTFUN1:def 4;
then A7: dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k)))) by RELAT_1:91;
reconsider sdom = s | (dom (ProgramPart (Relocated p,k))) as FinPartState of SCM+FSA ;
X: rng (ProgramPart s) c= the Instructions of SCM+FSA by RELAT_1:def 19;
dom (ProgramPart (Relocated p,k)) c= NAT by RELAT_1:def 18;
then s | (dom (ProgramPart (Relocated p,k))) c= ProgramPart s by RELAT_1:104;
then rng (s | (dom (ProgramPart (Relocated p,k)))) c= rng (ProgramPart s) by RELAT_1:25;
then B: rng (s | (dom (ProgramPart (Relocated p,k)))) c= the Instructions of SCM+FSA by X, XBOOLE_1:1;
dom (s | (dom (ProgramPart (Relocated p,k)))) c= NAT by A7, RELAT_1:def 18;
then reconsider sdom = sdom as preProgram of SCM+FSA by B, RELAT_1:def 18, RELAT_1:def 19;
reconsider ii = IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) as Element of NAT ;
reconsider jk = IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) as Element of NAT ;
A8: ProgramPart (Relocated p,k) c= Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i by AMI_1:99, FUNCT_4:26;
IC SCM+FSA in dom (Relocated p,k) by AMISTD_2:72;
then not Relocated p,k is NAT -defined by COMPOS_1:19;
then A9: IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) in dom (ProgramPart (Relocated p,k)) by A3, FUNCT_4:26, SCMFSA_3:17;
then IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) in dom (Reloc (ProgramPart p),k) by AMISTD_2:69;
then A10: jk in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by AMISTD_2:70;
A11: not IC SCM+FSA in dom (ProgramPart (Relocated p,k)) by COMPOS_1:12;
dom sdom = (dom s) /\ (dom (ProgramPart (Relocated p,k))) by RELAT_1:90;
then A12: not IC SCM+FSA in dom sdom by A11, XBOOLE_0:def 4;
dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A13: IC SCM+FSA in dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA ) by TARSKI:def 1;
not IC SCM+FSA in dom (ProgramPart p) by COMPOS_1:12;
then A14: IC ((((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* sdom) +* (ProgramPart p)) = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* sdom) . (IC SCM+FSA ) by FUNCT_4:12
.= ((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) . (IC SCM+FSA ) by A12, FUNCT_4:12
.= (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA ) . (IC SCM+FSA ) by A13, FUNCT_4:14
.= (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k by FUNCOP_1:87 ;
consider j being Element of NAT such that
A15: jk = j + k and
A16: j in dom (ProgramPart p) by A10;
Y: (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) /. (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 COMPOS_1:38;
dom (Shift pp,k) = { (m + k) where m is Element of NAT : m in dom pp } by VALUED_1:def 12;
then A17: j + k in dom (Shift (ProgramPart p),k) by A16;
then A18: IncAddr ((Shift (ProgramPart p),k) /. ii),k = (Reloc (ProgramPart p),k) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) by A15, SCMFSA_4:24
.= (ProgramPart (Relocated p,k)) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) by AMISTD_2:69
.= CurInstr (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) by A9, A8, Y, GRFUNC_1:8 ;
Y: (ProgramPart (Comput (ProgramPart s),s,i)) /. (IC (Comput (ProgramPart s),s,i)) = (Comput (ProgramPart s),s,i) . (IC (Comput (ProgramPart s),s,i)) by COMPOS_1:38;
A19: ((j + k) -' k) + k = j + k by NAT_D:34;
(j + k) -' k = j by NAT_D:34;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i) = (ProgramPart p) . ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k) by A6, A14, A15, A16, Y, FUNCT_4:14
.= (Shift (ProgramPart p),k) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) by A15, A16, A19, VALUED_1:def 12
.= (Shift (ProgramPart p),k) /. ii by A15, A17, PARTFUN1:def 8 ;
then A20: Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) = (Following (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i))) -' k),SCM+FSA ) by A15, A18, SCMFSA_4:29;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,i) by AMI_1:123;
S: ProgramPart (s +* (Relocated p,k)) = ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) by AMI_1:123;
A21: 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 AMI_1:14;
Comput (ProgramPart s),s,(i + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,i) by AMI_1:14
.= (Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),(((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* sdom)) +* (ProgramPart p) by A6, T, SCMFSA_3:10
.= (((Following (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i))) -' k),SCM+FSA )) +* sdom) +* (ProgramPart p) by A20, SCMFSA_3:10 ;
hence S1[i + 1] by A21, S; :: thesis: verum
end;
A22: IC SCM+FSA in dom (Relocated p,k) by AMISTD_2:72;
A23: IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 ) = (s +* (Relocated p,k)) . (IC SCM+FSA ) by AMI_1:13
.= IC (Relocated p,k) by A22, FUNCT_4:14 ;
DataPart p c= p by RELAT_1:88;
then A24: DataPart p c= s by A2, XBOOLE_1:1;
ProgramPart p c= p by RELAT_1:88;
then A25: ProgramPart p c= s by A2, XBOOLE_1:1;
set DP = DataPart p;
set IP = Start-At ((IC p) + k),SCM+FSA ;
set PP = ProgramPart p;
set IS = Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA ;
A27: dom (Start-At ((IC p) + k),SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
set PR = ProgramPart (Relocated p,k);
set SD = s | (dom (ProgramPart (Relocated p,k)));
dom (ProgramPart (Relocated p,k)) c= the carrier of SCM+FSA by RELAT_1:def 18;
then dom (ProgramPart (Relocated p,k)) c= dom s by PARTFUN1:def 4;
then A29: dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k)))) by RELAT_1:91;
{(IC SCM+FSA )} misses dom (ProgramPart (Relocated p,k)) by COMPOS_1:14;
then A30: {(IC SCM+FSA )} /\ (dom (ProgramPart (Relocated p,k))) = {} by XBOOLE_0:def 7;
A31: dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
then (dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) /\ (dom (s | (dom (ProgramPart (Relocated p,k))))) = {(IC SCM+FSA )} /\ ((dom s) /\ (dom (ProgramPart (Relocated p,k)))) by RELAT_1:90
.= ({(IC SCM+FSA )} /\ (dom (ProgramPart (Relocated p,k)))) /\ (dom s) by XBOOLE_1:16
.= {} by A30 ;
then A32: dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA ) misses dom (s | (dom (ProgramPart (Relocated p,k)))) by XBOOLE_0:def 7;
reconsider k = k as Element of NAT ;
Comput (ProgramPart s),s,0 = s by AMI_1:13
.= s +* (ProgramPart p) by A25, FUNCT_4:79
.= (s +* (Start-At (IC p),SCM+FSA )) +* (ProgramPart p) by A4, FUNCT_4:79
.= (s +* (Start-At (((IC p) + k) -' k),SCM+FSA )) +* (ProgramPart p) by NAT_D:34
.= (s +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (ProgramPart p) by A23, Z, AMISTD_2:73
.= ((s +* (s | (dom (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (ProgramPart p) by FUNCT_4:80
.= (((s +* (ProgramPart (Relocated p,k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (ProgramPart p) by A29, FUNCT_4:78
.= ((s +* (ProgramPart (Relocated p,k))) +* ((s | (dom (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA ))) +* (ProgramPart p) by FUNCT_4:15
.= ((s +* (ProgramPart (Relocated p,k))) +* ((Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA ) +* (s | (dom (ProgramPart (Relocated p,k)))))) +* (ProgramPart p) by A32, FUNCT_4:36
.= (((s +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by FUNCT_4:15
.= ((((s +* (DataPart p)) +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by A24, FUNCT_4:79
.= (((((s +* (DataPart p)) +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC p) + k),SCM+FSA )) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by A31, A27, FUNCT_4:78
.= ((((s +* ((DataPart p) +* (ProgramPart (Relocated p,k)))) +* (Start-At ((IC p) + k),SCM+FSA )) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* (((DataPart p) +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC p) + k),SCM+FSA ))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ((DataPart p) +* ((ProgramPart (Relocated p,k)) +* (Start-At ((IC p) + k),SCM+FSA )))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ((DataPart p) +* ((Start-At ((IC p) + k),SCM+FSA ) +* (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by A27, COMPOS_1:14, FUNCT_4:36
.= (((s +* (((DataPart p) +* (Start-At ((IC p) + k),SCM+FSA )) +* (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ((IncrIC (NPP p),k) +* (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by Z, COMPOS_1:75
.= (((s +* (Relocated p,k)) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by AMISTD_2:69
.= (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 ) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by AMI_1:13 ;
then A33: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A33, A5); :: thesis: verum