let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1 & I +* (Start-At 0 ,SCM+FSA ) c= s1 holds
for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
let J be Program of SCM+FSA ; :: thesis: ( J is_closed_on s1 & J +* (Start-At 0 ,SCM+FSA ) c= s1 implies for n being Element of NAT st ProgramPart (Relocated J,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
set JAt = J +* (Start-At 0 ,SCM+FSA );
assume A1: J is_closed_on s1 ; :: thesis: ( not J +* (Start-At 0 ,SCM+FSA ) c= s1 or for n being Element of NAT st ProgramPart (Relocated J,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
then A2: 0 in dom J by Th39;
dom J misses dom (Start-At 0 ,SCM+FSA ) by SF_MASTR:64;
then A3: J c= J +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:33;
then A4: dom J c= dom (J +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
assume A5: J +* (Start-At 0 ,SCM+FSA ) c= s1 ; :: thesis: for n being Element of NAT st ProgramPart (Relocated J,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
A6: IC SCM+FSA in dom (J +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
then A7: s1 . (IC s1) = s1 . ((J +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA )) by A5, GRFUNC_1:8
.= s1 . 0 by SF_MASTR:66
.= (J +* (Start-At 0 ,SCM+FSA )) . 0 by A5, A4, A2, GRFUNC_1:8
.= J . 0 by A3, A2, GRFUNC_1:8 ;
A8: IC (Comput (ProgramPart s1),s1,0 ) = s1 . (IC SCM+FSA ) by AMI_1:13
.= (J +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A5, A6, GRFUNC_1:8
.= 0 by SF_MASTR:66 ;
ProgramPart J = J by RELAT_1:209;
then A9: 0 in dom (ProgramPart J) by A1, Th39;
let n be Element of NAT ; :: thesis: ( ProgramPart (Relocated J,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) ) )
defpred S₁[ Nat] means ( (IC (Comput (ProgramPart s1),s1,$1)) + n = IC (Comput (ProgramPart s2),s2,$1) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,$1)),(Comput (ProgramPart s1),s1,$1)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,$1)),(Comput (ProgramPart s2),s2,$1) & DataPart (Comput (ProgramPart s1),s1,$1) = DataPart (Comput (ProgramPart s2),s2,$1) );
assume that
A10: ProgramPart (Relocated J,n) c= s2 and
A11: IC s2 = n and
A12: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
let i be Element of NAT ; :: thesis: ( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
A13: DataPart (Comput (ProgramPart s1),s1,0 ) = DataPart s2 by A12, AMI_1:13
.= DataPart (Comput (ProgramPart s2),s2,0 ) by AMI_1:13 ;
A14: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

dom J misses dom (Start-At 0 ,SCM+FSA ) by SF_MASTR:64;
then A15: J c= J +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:33;
then A16: dom J c= dom (J +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,k) by AMI_1:123;
A17: Comput (ProgramPart s1),s1,(k + 1) = Following (ProgramPart s1),(Comput (ProgramPart s1),s1,k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) by T ;
reconsider l = IC (Comput (ProgramPart s1),s1,(k + 1)) as Element of NAT ;
reconsider j = CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + 1))),(Comput (ProgramPart s1),s1,(k + 1)) as Instruction of SCM+FSA ;
Y: (ProgramPart (Comput (ProgramPart s1),s1,(k + 1))) /. (IC (Comput (ProgramPart s1),s1,(k + 1))) = (Comput (ProgramPart s1),s1,(k + 1)) . (IC (Comput (ProgramPart s1),s1,(k + 1))) by COMPOS_1:38;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,k) by AMI_1:123;
A18: Comput (ProgramPart s2),s2,(k + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) by T ;
s1 +* (J +* (Start-At 0 ,SCM+FSA )) = s1 by A5, FUNCT_4:79;
then A20: IC (Comput (ProgramPart s1),s1,(k + 1)) in dom J by A1, SCMFSA7B:def 7;
assume A21: S₁[k] ; :: thesis: S₁[k + 1]
hence A22: (IC (Comput (ProgramPart s1),s1,(k + 1))) + n = IC (Comput (ProgramPart s2),s2,(k + 1)) by A17, A18, SCMFSA6A:41; :: thesis: ( IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + 1))),(Comput (ProgramPart s1),s1,(k + 1))),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(k + 1))),(Comput (ProgramPart s2),s2,(k + 1)) & DataPart (Comput (ProgramPart s1),s1,(k + 1)) = DataPart (Comput (ProgramPart s2),s2,(k + 1)) )
then IC (Comput (ProgramPart s2),s2,(k + 1)) in dom (Relocated J,n) by A20, AMISTD_2:71;
then IC (Comput (ProgramPart s2),s2,(k + 1)) in (dom (Relocated J,n)) /\ NAT by XBOOLE_0:def 4;
then A23: IC (Comput (ProgramPart s2),s2,(k + 1)) in dom (ProgramPart (Relocated J,n)) by RELAT_1:90;
dom (ProgramPart J) = (dom J) /\ NAT by RELAT_1:90;
then A24: l in dom (ProgramPart J) by A20, XBOOLE_0:def 4;
U: (ProgramPart (Comput (ProgramPart s2),s2,(k + 1))) /. (IC (Comput (ProgramPart s2),s2,(k + 1))) = (Comput (ProgramPart s2),s2,(k + 1)) . (IC (Comput (ProgramPart s2),s2,(k + 1))) by COMPOS_1:38;
j = s1 . (IC (Comput (ProgramPart s1),s1,(k + 1))) by Y, AMI_1:54
.= (J +* (Start-At 0 ,SCM+FSA )) . (IC (Comput (ProgramPart s1),s1,(k + 1))) by A5, A16, A20, GRFUNC_1:8
.= J . l by A15, A20, GRFUNC_1:8 ;
hence IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + 1))),(Comput (ProgramPart s1),s1,(k + 1))),n = (Relocated J,n) . (l + n) by A24, AMISTD_2:76
.= (ProgramPart (Relocated J,n)) . (IC (Comput (ProgramPart s2),s2,(k + 1))) by A22, FUNCT_1:72
.= s2 . (IC (Comput (ProgramPart s2),s2,(k + 1))) by A10, A23, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(k + 1))),(Comput (ProgramPart s2),s2,(k + 1)) by U, AMI_1:54 ;
:: thesis: DataPart (Comput (ProgramPart s1),s1,(k + 1)) = DataPart (Comput (ProgramPart s2),s2,(k + 1))
thus DataPart (Comput (ProgramPart s1),s1,(k + 1)) = DataPart (Comput (ProgramPart s2),s2,(k + 1)) by A21, A17, A18, SCMFSA6A:41; :: thesis: verum

end;

0 in dom J by A1, Th39;
then 0 + n in dom (Relocated J,n) by AMISTD_2:71;
then A25: 0 + n in dom (ProgramPart (Relocated J,n)) by COMPOS_1:16;
V: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
U: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
u: Comput (ProgramPart s1),s1,0 = s1 by AMI_1:13;
v: Comput (ProgramPart s2),s2,0 = s2 by AMI_1:13;
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,0 )),(Comput (ProgramPart s1),s1,0 )),n = IncAddr (CurInstr (ProgramPart s1),s1),n by u
.= (Relocated J,n) . (0 + n) by A7, A9, V, AMISTD_2:76
.= (ProgramPart (Relocated J,n)) . n by FUNCT_1:72
.= CurInstr (ProgramPart s2),s2 by A10, A11, A25, U, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart s2),s2,0 )),(Comput (ProgramPart s2),s2,0 ) by v ;
then A26: S₁[ 0 ] by A11, A8, A13, AMI_1:13;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A26, A14);
hence ( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) ) ; :: thesis: verum