let k be natural number ; :: thesis:
let R be good Ring; :: thesis:
let p be FinPartState of (SCM R); :: thesis:
let s be State of (SCM R); :: thesis:
assume that
A1: not R is trivial and
A2: IC (SCM R) in dom p and
A3: p c= s and
A4: Relocated p,k is autonomic ; :: thesis:
set IS = Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k);
set IP = Start-At ((IC p) + k);
set PR = [(ProgramPart (Relocated p,k))];
set SD = s | (dom [(ProgramPart (Relocated p,k))]);
set PP = ProgramPart p;
set DP = DataPart p;
A5: dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) = {(IC (SCM R))} by FUNCOP_1:19;
A6: dom (Start-At ((IC p) + k)) = {(IC (SCM R))} by FUNCOP_1:19;
ProgramPart p c= p by RELAT_1:88;
then A7: ProgramPart p c= s by A3, XBOOLE_1:1;
Start-At (IC p) c= p by A2, AMI_1:110;
then A8: Start-At (IC p) c= s by A3, XBOOLE_1:1;
dom [(ProgramPart (Relocated p,k))] c= the carrier of (SCM R) by AMI_1:80;
then A9: dom [(ProgramPart (Relocated p,k))] c= dom s by AMI_1:79;
A10: IC (SCM R) in dom (Relocated p,k) by AMISTD_2:72;
A11: IC (Computation (s +* (Relocated p,k)),0 ) = (s +* (Relocated p,k)) . (IC (SCM R)) by AMI_1:13
.= (Relocated p,k) . (IC (SCM R)) by A10, FUNCT_4:14
.= IC (Relocated p,k) by A10, AMI_1:def 43 ;
DataPart p c= p by RELAT_1:88;
then A12: DataPart p c= s by A3, XBOOLE_1:1;
A13: dom (DataPart p) misses dom [(ProgramPart (Relocated p,k))] by AMI_1:104;
A14: dom (Start-At ((IC p) + k)) = dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) by A5, FUNCOP_1:19;
A15: {(IC (SCM R))} misses dom (DataPart p) by AMI_1:102;
A16: {(IC (SCM R))} misses dom [(ProgramPart (Relocated p,k))] by AMI_1:103;
A17: dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) misses dom (s | (dom [(ProgramPart (Relocated p,k))]))

proof

thus (dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) /\ (dom (s | (dom [(ProgramPart (Relocated p,k))]))) = (dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) /\ ((dom s) /\ (dom [(ProgramPart (Relocated p,k))])) by RELAT_1:90
.= {(IC (SCM R))} /\ ((dom s) /\ (dom [(ProgramPart (Relocated p,k))])) by FUNCOP_1:19
.= ({(IC (SCM R))} /\ (dom [(ProgramPart (Relocated p,k))])) /\ (dom s) by XBOOLE_1:16
.= {} /\ (dom s) by A16, XBOOLE_0:def 7
.= {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

A18: dom [(ProgramPart (Relocated p,k))] = dom (s | (dom [(ProgramPart (Relocated p,k))])) by A9, RELAT_1:91;
defpred S₁[ Element of NAT ] means Computation s,$1 = (((Computation (s +* (Relocated p,k)),$1) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),$1)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p);
Computation s,0 = s by AMI_1:13
.= s +* (ProgramPart p) by A7, FUNCT_4:79
.= (s +* (Start-At (IC p))) +* (ProgramPart p) by A8, FUNCT_4:79
.= (s +* (Start-At (((IC p) + k) -' k))) +* (ProgramPart p) by AMISTD_1:61
.= (s +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (ProgramPart p) by A11, AMISTD_2:73
.= ((s +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (ProgramPart p) by FUNCT_4:80
.= (((s +* [(ProgramPart (Relocated p,k))]) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (ProgramPart p) by A18, FUNCT_4:78
.= ((s +* [(ProgramPart (Relocated p,k))]) +* ((s | (dom [(ProgramPart (Relocated p,k))])) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)))) +* (ProgramPart p) by FUNCT_4:15
.= ((s +* [(ProgramPart (Relocated p,k))]) +* ((Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) +* (s | (dom [(ProgramPart (Relocated p,k))])))) +* (ProgramPart p) by A17, FUNCT_4:36
.= (((s +* [(ProgramPart (Relocated p,k))]) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= ((((s +* (DataPart p)) +* [(ProgramPart (Relocated p,k))]) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by A12, FUNCT_4:79
.= (((s +* ((DataPart p) +* [(ProgramPart (Relocated p,k))])) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ([(ProgramPart (Relocated p,k))] +* (DataPart p))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by A13, FUNCT_4:36
.= ((((s +* [(ProgramPart (Relocated p,k))]) +* (DataPart p)) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= (((((s +* [(ProgramPart (Relocated p,k))]) +* (DataPart p)) +* (Start-At ((IC p) + k))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by A14, FUNCT_4:78
.= ((((s +* ([(ProgramPart (Relocated p,k))] +* (DataPart p))) +* (Start-At ((IC p) + k))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* (([(ProgramPart (Relocated p,k))] +* (DataPart p)) +* (Start-At ((IC p) + k)))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ([(ProgramPart (Relocated p,k))] +* ((DataPart p) +* (Start-At ((IC p) + k))))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* ([(ProgramPart (Relocated p,k))] +* ((Start-At ((IC p) + k)) +* (DataPart p)))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by A6, A15, FUNCT_4:36
.= (((s +* (([(ProgramPart (Relocated p,k))] +* (Start-At ((IC p) + k))) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by FUNCT_4:15
.= (((s +* (((Start-At ((IC p) + k)) +* [(ProgramPart (Relocated p,k))]) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by A6, AMI_1:103, FUNCT_4:36
.= (((s +* (Relocated p,k)) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom [(ProgramPart (Relocated p,k))]))) +* (ProgramPart p) by AMISTD_2:69
.= (((Computation (s +* (Relocated p,k)),0 ) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by AMI_1:13 ;
then A19: S₁[ 0 ] ;
A20: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis:
assume A21: S₁[i] ; :: thesis:
reconsider sdom = s | (dom (ProgramPart (Relocated p,k))) as Element of sproduct the Object-Kind of (SCM R) ;
dom [(ProgramPart (Relocated p,k))] c= the carrier of (SCM R) by AMI_1:80;
then dom (ProgramPart (Relocated p,k)) c= dom s by AMI_1:79;
then A22: dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k)))) by RELAT_1:91;
then reconsider sdom = sdom as FinPartState of (SCM R) by FINSET_1:29;
dom (s | (dom (ProgramPart (Relocated p,k)))) c= NAT by A22, RELAT_1:87;
then reconsider sdom = sdom as NAT -defined FinPartState of (SCM R) by RELAT_1:def 18;
A23: Computation (s +* (Relocated p,k)),(i + 1) = Following (Computation (s +* (Relocated p,k)),i) by AMI_1:14;
dom (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k)) = {(IC (SCM R))} by FUNCOP_1:19;
then A24: IC (SCM R) in dom (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k)) by TARSKI:def 1;
A25: not IC (SCM R) in dom (ProgramPart p) by AMI_1:101;
A26: dom sdom = (dom s) /\ (dom (ProgramPart (Relocated p,k))) by RELAT_1:90;
not IC (SCM R) in dom (ProgramPart (Relocated p,k)) by AMI_1:101;
then A27: not IC (SCM R) in dom sdom by A26, XBOOLE_0:def 4;
A28: IC ((((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* sdom) +* [(ProgramPart p)]) = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* sdom) . (IC (SCM R)) by A25, FUNCT_4:12
.= ((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) . (IC (SCM R)) by A27, FUNCT_4:12
.= (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k)) . (IC (SCM R)) by A24, FUNCT_4:14
.= (IC (Computation (s +* (Relocated p,k)),i)) -' k by FUNCOP_1:87 ;
IC (SCM R) in dom (Relocated p,k) by AMISTD_2:72;
then not Relocated p,k is NAT -defined by AMI_1:109;
then A29: IC (Computation (s +* (Relocated p,k)),i) in dom (ProgramPart (Relocated p,k)) by A1, A4, Th40, FUNCT_4:26;
A30: ProgramPart (Relocated p,k) c= Computation (s +* (Relocated p,k)),i by AMI_1:99, FUNCT_4:26;
consider jk being natural number such that
A31: IC (Computation (s +* (Relocated p,k)),i) = il. (SCM R),jk by AMISTD_1:26;
il. (SCM R),jk in { (il. (SCM R),(j + k)) where j is Element of NAT : il. (SCM R),j in dom [(ProgramPart p)] } by A29, A31, AMISTD_2:70;
then consider j being Element of NAT such that
A32: ( il. (SCM R),jk = il. (SCM R),(j + k) & il. (SCM R),j in dom [(ProgramPart p)] ) ;
A33: ((il. (SCM R),(j + k)) -' k) + k = (((il. (SCM R),j) + k) -' k) + k by AMISTD_1:def 13
.= (il. (SCM R),j) + k by AMISTD_1:61
.= il. (SCM R),(j + k) by AMISTD_1:def 13 ;
A34: (il. (SCM R),(j + k)) -' k = ((il. (SCM R),j) + k) -' k by AMISTD_1:def 13
.= il. (SCM R),j by AMISTD_1:61 ;
reconsider pp = [(ProgramPart p)] as NAT -defined FinPartState of (SCM R) ;
dom (Shift pp,k) = { (il. (SCM R),(m + k)) where m is Element of NAT : il. (SCM R),m in dom pp } by AMISTD_2:def 16;
then A35: il. (SCM R),(j + k) in dom (Shift [(ProgramPart p)],k) by A32;
reconsider ii = IC (Computation (s +* (Relocated p,k)),i) as Element of NAT by ORDINAL1:def 13;
A36: CurInstr (Computation s,i) = (ProgramPart p) . ((IC (Computation (s +* (Relocated p,k)),i)) -' k) by A21, A28, A31, A32, A34, FUNCT_4:14
.= (Shift [(ProgramPart p)],k) . (IC (Computation (s +* (Relocated p,k)),i)) by A31, A32, A33, A34, AMISTD_2:65
.= pi (Shift [(ProgramPart p)],k),ii by A31, A32, A35, AMI_1:def 47 ;
IncAddr (pi (Shift [(ProgramPart p)],k),ii),k = (IncAddr (Shift [(ProgramPart p)],k),k) . (IC (Computation (s +* (Relocated p,k)),i)) by A31, A32, A35, AMISTD_2:74
.= (ProgramPart (Relocated p,k)) . (IC (Computation (s +* (Relocated p,k)),i)) by AMISTD_2:69
.= CurInstr (Computation (s +* (Relocated p,k)),i) by A29, A30, GRFUNC_1:8 ;
then A37: Exec (CurInstr (Computation s,i)),((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) = (Following (Computation (s +* (Relocated p,k)),i)) +* (Start-At ((IC (Following (Computation (s +* (Relocated p,k)),i))) -' k)) by A31, A32, A36, Th36;
thus Computation s,(i + 1) = Following (Computation s,i) by AMI_1:14
.= (Exec (CurInstr (Computation s,i)),(((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* sdom)) +* (ProgramPart p) by A21, AMISTD_2:67
.= (((Computation (s +* (Relocated p,k)),(i + 1)) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),(i + 1))) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) by A23, A37, AMISTD_2:67 ; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A19, A20);
hence for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) ; :: thesis: