let s be State of SCM+FSA ; :: according to AMI_1:def 26,SCM_HALT:def 2 :: thesis:
assume A1: Initialized (I ';' J) c= s ; :: thesis:
A2: Initialized (I ';' J) = (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15;
A3: s = s +* (Initialized (I ';' J)) by A1, FUNCT_4:79;
A4: dom I misses dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by Th2;
((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A5: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s by A1, A2, XBOOLE_1:1;
then s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) = s by FUNCT_4:79;
then A6: s +* I = s +* ((((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) +* I) by FUNCT_4:15
.= s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by A4, FUNCT_4:36
.= s +* (Initialized I) by FUNCT_4:15 ;
then A7: Initialized I c= s +* I by FUNCT_4:26;
A8: s +* I is halting by A6, Th5, FUNCT_4:26;
set JAt = Initialized J;
set s1 = s +* I;
set s3 = (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J);
set m1 = LifeSpan (s +* I);
set m3 = LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J));
set D = Int-Locations \/ FinSeq-Locations ;
A9: DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) +* (DataPart (Initialized J)) by FUNCT_4:75;

A10: now

let x be set ; :: thesis:
assume x in dom (DataPart (Initialized J)) ; :: thesis:
then A11: x in (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A12: ( x in dom (Initialized J) & x in Int-Locations \/ FinSeq-Locations ) by XBOOLE_0:def 4;

per cases by A12, SCMFSA6A:44;

suppose A13: x in dom J ; :: thesis:

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM+FSA by A13, AMI_1:def 4;
(DataPart (Initialized J)) . l = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . l by A12, SCMFSA6A:37;
hence (DataPart (Initialized J)) . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x ; :: thesis:

end;

suppose A14: x = intloc 0 ; :: thesis:

then x in Int-Locations by SCMFSA_2:9;
then A15: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x = (Computation (s +* I),(LifeSpan (s +* I))) . x by FUNCT_1:72, SCMFSA_2:127
.= 1 by A7, A14, Def3
.= (Initialized J) . x by A14, SCMFSA6A:46
.= (DataPart (Initialized J)) . x by A15, FUNCT_1:72, SCMFSA_2:127 ;
:: thesis:

end;

suppose x = IC SCM+FSA ; :: thesis:

hence (DataPart (Initialized J)) . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x by A11, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis:

end;

A16: Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by GRFUNC_1:8;
then A17: dom (Initialized J) c= the carrier of SCM+FSA by AMI_1:79;
dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations ) by A17, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Computation (s +* I),(LifeSpan (s +* I)))) /\ (Int-Locations \/ FinSeq-Locations ) by AMI_1:79;
then dom (DataPart (Initialized J)) c= dom (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) by RELAT_1:90, SCMFSA_2:127;
then DataPart (Initialized J) c= DataPart (Computation (s +* I),(LifeSpan (s +* I))) by A10, GRFUNC_1:8;
then DataPart (Computation (s +* I),(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A9, LATTICE2:8;
then A18: DataPart (Computation s,(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A3, A6, A8, Th24, SCMFSA6A:39;
A19: (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) is halting by A16, AMI_1:def 26;
A20: dom (Directed I) = dom I by FUNCT_4:105;
A21: Directed I c= I ';' J by SCMFSA6A:55;
dom (I ';' J) misses dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by Th2;
then A22: I ';' J c= Initialized (I ';' J) by A2, FUNCT_4:33;
A23: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A20, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A1, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A21, A22, LATTICE2:8, XBOOLE_1:1
.= s by A1, LATTICE2:8 ;
then A24: Directed I c= s by FUNCT_4:26;
A25: IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A5, A8, A23, Th21, FUNCT_4:26;
A26: DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A5, A7, A18, A24, Th5, Th22;
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) as Element of NAT ;
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A27: Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
A28: I ';' J c= s by A1, A22, XBOOLE_1:1;
ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
then ProgramPart (Relocated J,(card I)) c= s by A28, XBOOLE_1:1;
then A29: [(ProgramPart (Relocated J,(card I)))] c= Computation s,((LifeSpan (s +* I)) + 1) by AMI_1:81;
take m ; :: according to AMI_1:def 20 :: thesis:
IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))),(card I) = CurInstr (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) by A25, A26, A27, A29, Th12;
then IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))),(card I) = CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))) by AMI_1:51;
hence CurInstr (Computation s,m) = IncAddr (halt SCM+FSA ),(card I) by A19, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
:: thesis: