let s be State of ; :: according to AMI_1:def 26,SCMPDS_4:def 10 :: thesis: ( not Initialized (stop (I ';' J)) c= s or ProgramPart s halts_on s )
set sIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set spJ = stop J;
set IsJ = Initialized (stop J);
set s1 = s +* (Initialized (stop I));
set m1 = LifeSpan (s +* (Initialized (stop I)));
set s3 = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J));
set m3 = LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)));
set D = SCM-Data-Loc ;
A1: DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) +* (DataPart (Initialized (stop J))) by FUNCT_4:75;

A2: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized (stop J))) implies (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . b₁ )
assume x in dom (DataPart (Initialized (stop J))) ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . b₁
then A3: x in (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A4: x in dom (Initialized (stop J)) by XBOOLE_0:def 4;
A5: x in SCM-Data-Loc by A3, XBOOLE_0:def 4;

per cases ( x in dom (stop J) or x = IC SCMPDS ) by A4, SCMPDS_4:28;

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

dom (stop J) c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCMPDS by A6, AMI_1:def 4;
(DataPart (Initialized (stop J))) . l = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . l by A5, SCMPDS_4:22;
hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . x ; :: thesis: verum

end;

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

hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . x by A3, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A7: dom (DataPart (Initialized (stop J))) = (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
A8: Initialized (stop J) c= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) by FUNCT_4:26;
then A9: ProgramPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) halts_on (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) by AMI_1:def 26;
dom (Initialized (stop J)) c= dom ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by A8, GRFUNC_1:8;
then dom (Initialized (stop J)) c= the carrier of SCMPDS by AMI_1:79;
then dom (DataPart (Initialized (stop J))) c= the carrier of SCMPDS /\ SCM-Data-Loc by A7, XBOOLE_1:26;
then dom (DataPart (Initialized (stop J))) c= (dom (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) /\ SCM-Data-Loc by AMI_1:79;
then dom (DataPart (Initialized (stop J))) c= dom (DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialized (stop J)) c= DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by A2, GRFUNC_1:8;
then A10: DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by A1, LATTICE2:8;
A11: Initialized I c= Initialized (stop (I ';' J)) by Th15;
set s4 = Computation s,(LifeSpan (s +* (Initialized (stop I))));
assume A12: Initialized (stop (I ';' J)) c= s ; :: thesis: ProgramPart s halts_on s
then A13: stop (I ';' J) c= s by SCMPDS_4:57;
s = s +* (Initialized (stop (I ';' J))) by A12, FUNCT_4:79
.= s +* ((I ';' (J ';' (Stop SCMPDS ))) +* (Start-At (inspos 0 ))) by SCMPDS_4:46 ;
then A14: DataPart (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by A10, Th33, SCMPDS_4:24;

per cases ( CurInstr (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS or IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ) by A12, A11, Th31, XBOOLE_1:1;

suppose A15: CurInstr (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS ; :: thesis: ProgramPart s halts_on s

take LifeSpan (s +* (Initialized (stop I))) ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,(LifeSpan (s +* (Initialized (stop I)))))) = halt SCMPDS )
IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) in NAT by AMI_1:def 4;
hence IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) . (IC (Computation s,(LifeSpan (s +* (Initialized (stop I)))))) = halt SCMPDS
then CurInstr (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS by A15, AMI_1:def 13;
hence (ProgramPart s) . (IC (Computation s,(LifeSpan (s +* (Initialized (stop I)))))) = halt SCMPDS by AMI_1:145; :: thesis: verum

end;

suppose A16: IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ; :: thesis: ProgramPart s halts_on s

reconsider m = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))) as Element of NAT ;
take m ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,m) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,m)) = halt SCMPDS )
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 SCMPDS
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46
.= I +* (Shift (stop J),(card I)) ;
then Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26;
then Shift (stop J),(card I) c= s by A13, XBOOLE_1:1;
then Shift (stop J),(card I) c= Computation s,(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:81;
then X: CurInstr (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = CurInstr (Computation (Computation s,(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) by A8, A14, A16, SCMPDS_4:84;
then Y: CurInstr (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = CurInstr (Computation s,((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) by AMI_1:51;
CurInstr (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = halt SCMPDS by A9, AMI_1:def 46;
then CurInstr (Computation s,m) = halt SCMPDS by A9, AMI_1:def 46, X, Y;
hence (ProgramPart s) . (IC (Computation s,m)) = halt SCMPDS by AMI_1:145; :: thesis: verum

end;

end;