let s be State of SCMPDS ; :: 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 = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J));
set m3 = LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)));
set D = SCM-Data-Loc ;
A1: DataPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) = (DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(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 (Comput (ProgramPart (s +* (Initialized (stop I)))),(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 (Comput (ProgramPart (s +* (Initialized (stop I)))),(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 (Comput (ProgramPart (s +* (Initialized (stop I)))),(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 Element of NAT by A6;
(DataPart (Initialized (stop J))) . l = (DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . l by A5, SCMPDS_4:22;
hence (DataPart (Initialized (stop J))) . x = (DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) . x ; :: thesis: verum

end;

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

hence (DataPart (Initialized (stop J))) . x = (DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(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= (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) by FUNCT_4:26;
then A9: ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) halts_on (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) by AMI_1:def 26;
dom (Initialized (stop J)) c= dom ((Comput (ProgramPart (s +* (Initialized (stop I)))),(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 PARTFUN1:def 4;
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 (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) /\ SCM-Data-Loc by PARTFUN1:def 4;
then dom (DataPart (Initialized (stop J))) c= dom (DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialized (stop J)) c= DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by A2, GRFUNC_1:8;
then A10: DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(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 = Comput (ProgramPart s),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 0 ,SCMPDS )) by SCMPDS_4:46 ;
then A14: DataPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) by A10, Th33, SCMPDS_4:24;

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

suppose A15: CurInstr (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart s),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 (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) in proj1 (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))) = halt SCMPDS )
IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) in NAT ;
hence IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))) = halt SCMPDS
CurInstr (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS by A15;
hence (ProgramPart s) /. (IC (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))) = halt SCMPDS by AMI_1:145; :: thesis: verum

end;

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

reconsider m = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(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 (Comput (ProgramPart s),s,m) in proj1 (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,m)) = halt SCMPDS )
IC (Comput (ProgramPart s),s,m) in NAT ;
hence IC (Comput (ProgramPart s),s,m) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,m)) = halt SCMPDS
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))) by AMI_1:144;
x: Comput (ProgramPart s),s,((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))) by AMI_1:51;
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= Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:81;
then CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))),(Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))),(Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) by A8, A14, A16, SCMPDS_4:84;
then Y: CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))),(Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = CurInstr (ProgramPart (Comput (ProgramPart s),s,((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))))),(Comput (ProgramPart s),s,((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) by x, T;
CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))),(Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = halt SCMPDS by A9, AMI_1:def 46;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,m)),(Comput (ProgramPart s),s,m) = halt SCMPDS by Y;
hence (ProgramPart s) /. (IC (Comput (ProgramPart s),s,m)) = halt SCMPDS by AMI_1:145; :: thesis: verum

end;

end;