let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I +* (Start-At (insloc 0 )) c= s1 & I is_closed_on s1 holds
for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let I be Program of SCM+FSA ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s1 & I is_closed_on s1 implies for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A1: I +* (Start-At (insloc 0 )) c= s1 ; :: thesis: ( not I is_closed_on s1 or for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A2: I is_closed_on s1 ; :: thesis: for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let n be Element of NAT ; :: thesis: ( ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
A3: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A4: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A5: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
defpred S₁[ Element of NAT ] means ( (IC (Computation s1,$1)) + n = IC (Computation s2,$1) & IncAddr (CurInstr (Computation s1,$1)),n = CurInstr (Computation s2,$1) & DataPart (Computation s1,$1) = DataPart (Computation s2,$1) );
assume A6: ProgramPart (Relocated I,n) c= s2 ; :: thesis: ( not IC s2 = insloc n or not DataPart s1 = DataPart s2 or for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
A7: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A8: Computation s1,(k + 1) = Following (Computation s1,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s1,k) ;
reconsider l = IC (Computation s1,(k + 1)) as Element of NAT by ORDINAL1:def 13;
reconsider j = CurInstr (Computation s1,(k + 1)) as Instruction of SCM+FSA ;
A9: Computation s2,(k + 1) = Following (Computation s2,k) by AMI_1:14
.= Exec (CurInstr (Computation s2,k)),(Computation s2,k) ;
A10: IC (Computation s2,(k + 1)) in NAT by AMI_1:def 4;
s1 +* (I +* (Start-At (insloc 0 ))) = s1 by A1, FUNCT_4:79;
then A11: IC (Computation s1,(k + 1)) in dom I by A2, SCMFSA7B:def 7;
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
hence A13: (IC (Computation s1,(k + 1))) + n = IC (Computation s2,(k + 1)) by A8, A9, SCMFSA6A:41; :: thesis: ( IncAddr (CurInstr (Computation s1,(k + 1))),n = CurInstr (Computation s2,(k + 1)) & DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) )
then IC (Computation s2,(k + 1)) in dom (Relocated I,n) by A11, SCMFSA_5:4;
then IC (Computation s2,(k + 1)) in (dom (Relocated I,n)) /\ NAT by A10, XBOOLE_0:def 4;
then A14: IC (Computation s2,(k + 1)) in dom (ProgramPart (Relocated I,n)) by RELAT_1:90;
dom (ProgramPart I) = (dom I) /\ NAT by RELAT_1:90;
then A15: l in dom (ProgramPart I) by A11, XBOOLE_0:def 4;
A16: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A17: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
j = s1 . (IC (Computation s1,(k + 1))) by AMI_1:54
.= (I +* (Start-At (insloc 0 ))) . (IC (Computation s1,(k + 1))) by A1, A17, A11, GRFUNC_1:8
.= I . l by A16, A11, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation s1,(k + 1))),n = (Relocated I,n) . (l + n) by A15, SCMFSA_5:7
.= (ProgramPart (Relocated I,n)) . (IC (Computation s2,(k + 1))) by A13, FUNCT_1:72
.= s2 . (IC (Computation s2,(k + 1))) by A6, A14, GRFUNC_1:8
.= CurInstr (Computation s2,(k + 1)) by AMI_1:54 ;
:: thesis: DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1))
thus DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) by A12, A8, A9, SCMFSA6A:41; :: thesis: verum

end;

A18: IC (Computation s1,0 ) = s1 . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A1, A3, GRFUNC_1:8
.= insloc 0 by SF_MASTR:66 ;
assume A19: IC s2 = insloc n ; :: thesis: ( not DataPart s1 = DataPart s2 or for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
A20: insloc 0 in dom I by A2, Th3;
then (insloc 0 ) + n in dom (Relocated I,n) by SCMFSA_5:4;
then A21: insloc (0 + n) in dom (ProgramPart (Relocated I,n)) by AMI_1:106;
IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A22: s1 . (IC s1) = s1 . ((I +* (Start-At (insloc 0 ))) . (IC SCM+FSA )) by A1, GRFUNC_1:8
.= s1 . (insloc 0 ) by SF_MASTR:66
.= (I +* (Start-At (insloc 0 ))) . (insloc 0 ) by A1, A5, A20, GRFUNC_1:8
.= I . (insloc 0 ) by A4, A20, GRFUNC_1:8 ;
ProgramPart I = I by AMI_1:105;
then A23: insloc 0 in dom (ProgramPart I) by A2, Th3;
assume DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
then A24: DataPart (Computation s1,0 ) = DataPart s2 by AMI_1:13
.= DataPart (Computation s2,0 ) by AMI_1:13 ;
let i be Element of NAT ; :: thesis: ( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
IncAddr (CurInstr (Computation s1,0 )),n = IncAddr (CurInstr s1),n by AMI_1:13
.= (Relocated I,n) . ((insloc 0 ) + n) by A22, A23, SCMFSA_5:7
.= (ProgramPart (Relocated I,n)) . (insloc n) by FUNCT_1:72
.= CurInstr s2 by A6, A19, A21, GRFUNC_1:8
.= CurInstr (Computation s2,0 ) by AMI_1:13 ;
then A25: S₁[ 0 ] by A19, A18, A24, AMI_1:13;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A25, A7);
hence ( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) ; :: thesis: verum