let k be Element of NAT ; :: thesis:
let p be FinPartState of SCM; :: thesis:
assume A0: IC SCM in dom p ; :: thesis:
then A1: Start-At ((IC p),SCM) c= p by FUNCOP_1:99;
let s be State of SCM; :: thesis:
assume that
A2: p c= s and
A3: Relocated (p,k) is autonomic ; :: thesis:
A4: Start-At ((IC p),SCM) c= s by A2, A1, XBOOLE_1:1;
defpred S₁[ Element of 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))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p);
A5: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

reconsider pp = ProgramPart p as preProgram of SCM ;
set sdom = s | (dom (ProgramPart (Relocated (p,k))));
dom (ProgramPart (Relocated (p,k))) c= the carrier of SCM by RELAT_1:def 18;
then dom (ProgramPart (Relocated (p,k))) c= dom s by PARTFUN1:def 4;
then dom (ProgramPart (Relocated (p,k))) = dom (s | (dom (ProgramPart (Relocated (p,k))))) by RELAT_1:91;
then ( rng (s | (dom (ProgramPart (Relocated (p,k))))) c= the Instructions of SCM & dom (s | (dom (ProgramPart (Relocated (p,k))))) c= NAT ) by COMPOS_1:32, RELAT_1:87;
then reconsider sdom = s | (dom (ProgramPart (Relocated (p,k)))) as NAT -defined finite FinPartState of by RELSET_1:11;
let i be Element of NAT ; :: thesis:
assume A7: 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))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) ; :: thesis:
reconsider kk = 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 in dom (Relocated (p,k)) by COMPOS_1:119;
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, AMI_5:86, FUNCT_4:26;
then IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) in dom (Reloc ((ProgramPart p),k)) by COMPOS_1:116;
then A10: jk in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by COMPOS_1:117;
( dom sdom = (dom s) /\ (dom (ProgramPart (Relocated (p,k)))) & not IC SCM in dom (ProgramPart (Relocated (p,k))) ) by COMPOS_1:12, RELAT_1:90;
then A11: not IC SCM in dom sdom by XBOOLE_0:def 4;
dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM)) = {(IC SCM)} by FUNCOP_1:19;
then A12: IC SCM in dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM)) by TARSKI:def 1;
consider j being Element of NAT such that
A13: jk = j + k and
A14: j in dom (ProgramPart p) by A10;
T: ProgramPart (s +* (Relocated (p,k))) = ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) by AMI_1:123;
Y: (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 T, 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 A15: j + k in dom (Shift ((ProgramPart p),k)) by A14;
then A16: IncAddr (((Shift ((ProgramPart p),k)) /. kk),k) = (Reloc ((ProgramPart p),k)) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) by A13, COMPOS_1:def 40
.= (ProgramPart (Relocated (p,k))) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) by COMPOS_1:116
.= CurInstr ((ProgramPart (s +* (Relocated (p,k)))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) by A9, A8, Y, GRFUNC_1:8 ;
U1: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i)) by AMI_1:123;
A17: (j + k) -' k = j by NAT_D:34;
Z: (ProgramPart s) /. (IC (Comput ((ProgramPart s),s,i))) = (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by U1, COMPOS_1:38;
not IC SCM in dom (ProgramPart p) by COMPOS_1:12;
then 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))) +* 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))) +* sdom) . (IC SCM) 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))) . (IC SCM) by A11, FUNCT_4:12
.= (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM)) . (IC SCM) by A12, FUNCT_4:14
.= (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k by FUNCOP_1:87 ;
then CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,i))) = (ProgramPart p) . ((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k) by A7, A13, A14, A17, Z, FUNCT_4:14
.= (Shift ((ProgramPart p),k)) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) by A13, A14, A17, VALUED_1:def 12
.= (Shift ((ProgramPart p),k)) /. kk by A13, A15, PARTFUN1:def 8 ;
then A18: ( 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))) & Exec ((CurInstr ((ProgramPart s),(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)))) = (Following ((ProgramPart (s +* (Relocated (p,k)))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))) +* (Start-At (((IC (Following ((ProgramPart (s +* (Relocated (p,k)))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))))) -' k),SCM)) ) by A13, A16, Th32, EXTPRO_1:4;
thus Comput ((ProgramPart s),s,(i + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,i))) by EXTPRO_1:4
.= (Exec ((CurInstr ((ProgramPart s),(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))) +* sdom))) +* (ProgramPart p) by A7, AMI_1:127
.= (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),(i + 1))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),(i + 1)))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by A18, AMI_1:127 ; :: thesis:

end;

A19: IC SCM in dom (Relocated (p,k)) by COMPOS_1:119;
A20: IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0)) = (s +* (Relocated (p,k))) . (IC SCM) by EXTPRO_1:3
.= (Relocated (p,k)) . (IC SCM) by A19, FUNCT_4:14
.= IC (Relocated (p,k)) ;
DataPart p c= p by RELAT_1:88;
then A21: DataPart p c= s by A2, XBOOLE_1:1;
ProgramPart p c= p by RELAT_1:88;
then A22: ProgramPart p c= s by A2, XBOOLE_1:1;
set DP = DataPart p;
set IP = Start-At (((IC p) + k),SCM);
A23: dom (DataPart p) misses dom (ProgramPart (Relocated (p,k))) by COMPOS_1:15;
set PP = ProgramPart p;
set IS = Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM);
A24: dom (Start-At (((IC p) + k),SCM)) = {(IC SCM)} by FUNCOP_1:19;
set PR = ProgramPart (Relocated (p,k));
set SD = s | (dom (ProgramPart (Relocated (p,k))));
A25: {(IC SCM)} misses dom (DataPart p) by COMPOS_1:13;
dom (ProgramPart (Relocated (p,k))) c= the carrier of SCM by RELAT_1:def 18;
then dom (ProgramPart (Relocated (p,k))) c= dom s by PARTFUN1:def 4;
then A26: dom (ProgramPart (Relocated (p,k))) = dom (s | (dom (ProgramPart (Relocated (p,k))))) by RELAT_1:91;
{(IC SCM)} misses dom (ProgramPart (Relocated (p,k))) by COMPOS_1:14;
then A27: {(IC SCM)} /\ (dom (ProgramPart (Relocated (p,k)))) = {} by XBOOLE_0:def 7;
A28: dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM)) = {(IC SCM)} by FUNCOP_1:19;
then (dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) /\ (dom (s | (dom (ProgramPart (Relocated (p,k)))))) = {(IC SCM)} /\ ((dom s) /\ (dom (ProgramPart (Relocated (p,k))))) by RELAT_1:90
.= ({(IC SCM)} /\ (dom (ProgramPart (Relocated (p,k))))) /\ (dom s) by XBOOLE_1:16
.= {} by A27 ;
then A29: dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM)) misses dom (s | (dom (ProgramPart (Relocated (p,k))))) by XBOOLE_0:def 7;
T2: dom ((Start-At (((IC p) + k),SCM)) +* (Reloc ((ProgramPart p),k))) = (dom (Start-At (((IC p) + k),SCM))) \/ (dom (Reloc ((ProgramPart p),k))) by FUNCT_4:def 1;
X: NAT misses Data-Locations SCM by AMI_2:29, AMI_3:72;
dom (Reloc ((ProgramPart p),k)) c= NAT by RELAT_1:def 18;
then T3: dom (Reloc ((ProgramPart p),k)) misses Data-Locations SCM by X, XBOOLE_1:63;
T1: dom (Start-At (((IC p) + k),SCM)) misses dom (DataPart p) by A25, FUNCOP_1:19;
dom (Reloc ((ProgramPart p),k)) misses dom (DataPart p) by T3, XBOOLE_1:63, RELAT_1:87;
then T: dom ((Start-At (((IC p) + k),SCM)) +* (Reloc ((ProgramPart p),k))) misses dom (DataPart p) by T1, T2, XBOOLE_1:70;
X: ((Start-At (((IC p) + k),SCM)) +* (ProgramPart (Relocated (p,k)))) +* (DataPart p) = ((Start-At (((IC p) + k),SCM)) +* (Reloc ((ProgramPart p),k))) +* (DataPart p) by COMPOS_1:116
.= (DataPart p) +* ((Start-At (((IC p) + k),SCM)) +* (Reloc ((ProgramPart p),k))) by T, FUNCT_4:36
.= ((DataPart p) +* (Start-At (((IC p) + k),SCM))) +* (Reloc ((ProgramPart p),k)) by FUNCT_4:15
.= Relocated (p,k) by A0, COMPOS_1:75 ;
Comput ((ProgramPart s),s,0) = s by EXTPRO_1:3
.= s +* (ProgramPart p) by A22, FUNCT_4:79
.= (s +* (Start-At ((IC p),SCM))) +* (ProgramPart p) by A4, FUNCT_4:79
.= (s +* (Start-At ((((IC p) + k) -' k),SCM))) +* (ProgramPart p) by NAT_D:34
.= (s +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (ProgramPart p) by A20, A0, Th26
.= ((s +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (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))) +* (ProgramPart p) by A26, 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)))) +* (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)) +* (s | (dom (ProgramPart (Relocated (p,k))))))) +* (ProgramPart p) by A29, FUNCT_4:36
.= (((s +* (ProgramPart (Relocated (p,k)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (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))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by A21, FUNCT_4:79
.= (((s +* ((DataPart p) +* (ProgramPart (Relocated (p,k))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ((ProgramPart (Relocated (p,k))) +* (DataPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by A23, FUNCT_4:36
.= ((((s +* (ProgramPart (Relocated (p,k)))) +* (DataPart p)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by FUNCT_4:15
.= (((((s +* (ProgramPart (Relocated (p,k)))) +* (DataPart p)) +* (Start-At (((IC p) + k),SCM))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by A28, A24, FUNCT_4:78
.= ((((s +* ((ProgramPart (Relocated (p,k))) +* (DataPart p))) +* (Start-At (((IC p) + k),SCM))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* (((ProgramPart (Relocated (p,k))) +* (DataPart p)) +* (Start-At (((IC p) + k),SCM)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ((ProgramPart (Relocated (p,k))) +* ((DataPart p) +* (Start-At (((IC p) + k),SCM))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ((ProgramPart (Relocated (p,k))) +* ((Start-At (((IC p) + k),SCM)) +* (DataPart p)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by A24, A25, FUNCT_4:36
.= (((s +* (((ProgramPart (Relocated (p,k))) +* (Start-At (((IC p) + k),SCM))) +* (DataPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* (((Start-At (((IC p) + k),SCM)) +* (ProgramPart (Relocated (p,k)))) +* (DataPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by A24, COMPOS_1:14, FUNCT_4:36
.= (((s +* (Relocated (p,k))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by X
.= (((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))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) by EXTPRO_1:3 ;
then A30: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A30, A5); :: thesis: