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

A2: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialize (stop J))) implies (DataPart (Initialize (stop J))) . b₁ = (DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) . b₁ )
assume x in dom (DataPart (Initialize (stop J))) ; :: thesis: (DataPart (Initialize (stop J))) . b₁ = (DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) . b₁
then A3: x in (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A4: x in dom (Initialize (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, COMPOS_1:77;

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

dom (stop J) c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A6;
(DataPart (Initialize (stop J))) . l = (DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) . l by A5, SCMPDS_4:22;
hence (DataPart (Initialize (stop J))) . x = (DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) . x ; :: thesis: verum

end;

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

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

end;

end;

end;

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

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

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

take LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) in proj1 (ProgramPart s) & CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = halt SCMPDS )
IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) in NAT ;
hence IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = halt SCMPDS
ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by AMI_1:123;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = halt SCMPDS by A15;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = halt SCMPDS ; :: thesis: verum

end;

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

reconsider m = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (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) & CurInstr (ProgramPart s),(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 COMPOS_1:34; :: thesis: CurInstr (ProgramPart s),(Comput (ProgramPart s),s,m) = halt SCMPDS
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by AMI_1:123;
x: Comput (ProgramPart s),s,((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (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 (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by AMI_1:81;
then CurInstr (ProgramPart (Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))))),(Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) = CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))))),(Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) by A8, A14, A16, SCMPDS_4:84;
then Y: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))))),(Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) = CurInstr (ProgramPart (Comput (ProgramPart s),s,((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))))),(Comput (ProgramPart s),s,((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))))) by x, T;
TX3: ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)) = ProgramPart (Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) by AMI_1:123;
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,m) by AMI_1:123;
CurInstr (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),(Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) = halt SCMPDS by A9, AMI_1:def 46;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,m) = halt SCMPDS by Y, TX, TX3;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,m) = halt SCMPDS ; :: thesis: verum

end;

end;