set D = Int-Locations \/ FinSeq-Locations ;
set JAt = Initialized J;
let s be State of ; :: according to AMI_1:def 26,SCM_HALT:def 2 :: thesis: ( not Initialized (I ';' J) c= s or ProgramPart s halts_on s )
A1: Initialized (I ';' J) = (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15;
set s1 = s +* I;
set s3 = (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J);
set m1 = LifeSpan (s +* I);
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A2: ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
A3: dom I misses dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by Th2;
set m3 = LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J));
A4: dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) as Element of NAT ;
A5: dom (Directed I) = dom I by FUNCT_4:105;
assume A6: Initialized (I ';' J) c= s ; :: thesis: ProgramPart s halts_on s
then A7: s = s +* (Initialized (I ';' J)) by FUNCT_4:79;
dom (I ';' J) misses dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by Th2;
then A8: I ';' J c= Initialized (I ';' J) by A1, FUNCT_4:33;
then I ';' J c= s by A6, XBOOLE_1:1;
then ProgramPart (Relocated J,(card I)) c= s by A2, XBOOLE_1:1;
then A9: ( Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) & [(ProgramPart (Relocated J,(card I)))] c= Computation s,((LifeSpan (s +* I)) + 1) ) by AMI_1:81, FUNCT_4:26;
((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A10: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s by A6, A1, XBOOLE_1:1;
then s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) = s by FUNCT_4:79;
then A11: 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 A3, FUNCT_4:36
.= s +* (Initialized I) by FUNCT_4:15 ;
then A12: ProgramPart (s +* I) halts_on s +* I by Th5, FUNCT_4:26;
A13: Initialized I c= s +* I by A11, FUNCT_4:26;

A14: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized J)) implies (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁ )
assume x in dom (DataPart (Initialized J)) ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁
then A15: x in (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A16: x in dom (Initialized J) by XBOOLE_0:def 4;
A17: x in Int-Locations \/ FinSeq-Locations by A15, XBOOLE_0:def 4;

per cases ( x in dom J or x = intloc 0 or x = IC SCM+FSA ) by A16, SCMFSA6A:44;

suppose A18: x in dom J ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁

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

end;

suppose A19: x = intloc 0 ; :: thesis: (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁ = (DataPart (Initialized J)) . b₁

then x in Int-Locations by SCMFSA_2:9;
then A20: 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 A13, A19, Def3
.= (Initialized J) . x by A19, SCMFSA6A:46
.= (DataPart (Initialized J)) . x by A20, FUNCT_1:72, SCMFSA_2:127 ;
:: thesis: verum

end;

suppose x = IC SCM+FSA ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁

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

end;

end;

end;

take m ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,m) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,m)) = halt SCM+FSA )
IC (Computation s,m) in NAT by AMI_1:def 4;
hence IC (Computation s,m) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) . (IC (Computation s,m)) = halt SCM+FSA
A21: Directed I c= I ';' J by SCMFSA6A:55;
A22: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A5, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A6, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A21, A8, LATTICE2:8, XBOOLE_1:1
.= s by A6, LATTICE2:8 ;
then A23: Directed I c= s by FUNCT_4:26;
A24: 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 dom (Initialized J) c= the carrier of SCM+FSA by AMI_1:79;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations ) by A4, 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 ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Computation (s +* I),(LifeSpan (s +* I))) ) by A14, FUNCT_4:75, GRFUNC_1:8;
then DataPart (Computation (s +* I),(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by LATTICE2:8;
then X: DataPart (Computation s,(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A7, A11, A12, Th24, SCMFSA6A:39;
then ProgramPart (s +* I) halts_on s +* I by A11, A13, A23, Th5;
then A25: DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A10, A13, A23, Th5, Th22, X;
IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A10, A12, A22, Th21, FUNCT_4:26;
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 (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) by A25, A9, Th12;
then A26: 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;
ProgramPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) halts_on (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by A24, AMI_1:def 26;
then CurInstr (Computation s,m) = IncAddr (halt SCM+FSA ),(card I) by A26, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
hence (ProgramPart s) . (IC (Computation s,m)) = halt SCM+FSA by AMI_1:145; :: thesis: verum