let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS
for J being shiftable Program of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )
let I be Program of SCMPDS; :: thesis: for J being shiftable Program of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )
let J be shiftable Program of SCMPDS; :: thesis: ( I is_closed_on s & I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) implies ( I ';' J is_closed_on s & I ';' J is_halting_on s ) )
set sE = IExec (I,s);
assume that
A1: I is_closed_on s and
A2: I is_halting_on s and
A3: J is_closed_on IExec (I,s) and
A4: J is_halting_on IExec (I,s) ; :: thesis: ( I ';' J is_closed_on s & I ';' J is_halting_on s )
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set spI = stop I;
set ss = (Initialize s) +* (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 sm = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(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)));
A5: (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (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 COMPOS_1:125;
A6: dom (DataPart (Initialize (stop J))) = (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by A2, A3, A4, Th42;
then A7: 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 SCMPDS_6:def 3;
A8: J is_closed_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by A2, A3, A4, Th42;
then A9: J is_closed_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 SCMPDS_6:38;

A10: 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 A11: x in (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A12: x in dom (Initialize (stop J)) by XBOOLE_0:def 4;
A13: x in SCM-Data-Loc by A11, XBOOLE_0:def 4;

per cases ( x in dom (stop J) or x = IC ) by A12, COMPOS_1:77;

suppose A14: 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₁

reconsider l = x as Element of NAT by A14;
l = x ;
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 A13, SCMPDS_4:22; :: thesis: verum

end;

suppose x = IC ; :: 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 A11, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
A15: 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 A5, FUNCT_4:75;
A16: 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 A5, FUNCT_4:26;
then 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 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 A6, 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 A10, GRFUNC_1:8;
then A17: 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 A15, LATTICE2:8;
(Initialize s) +* (stop (I ';' J)) = (Initialize s) +* (I ';' (J ';' (Stop SCMPDS))) by AFINSQ_1:30;
then Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) = Comput ((ProgramPart ((Initialize s) +* (I ';' (J ';' (Stop SCMPDS))))),((Initialize s) +* (I ';' (J ';' (Stop SCMPDS)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) ;
then Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))), Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) equal_outside NAT by A1, A2, Th38;
then A18: DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(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 A17, COMPOS_1:138;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30
.= I +* (Shift ((stop J),(card I))) ;
then A19: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:26;
stop (I ';' J) c= (Initialize s) +* (stop (I ';' J)) by FUNCT_4:26;
then Shift ((stop J),(card I)) c= (Initialize s) +* (stop (I ';' J)) by A19, XBOOLE_1:1;
then A20: Shift ((stop J),(card I)) c= Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by AMI_1:81;
A21: dom (stop I) c= dom (stop (I ';' J)) by SCMPDS_5:16;

now

let k be Element of NAT ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),b₁)) in dom (stop (I ';' J))
A22: ProgramPart ((Initialize s) +* (stop (I ';' J))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by AMI_1:123;

per cases ( k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) or k > LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ) ;

suppose k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),b₁)) in dom (stop (I ';' J))

then IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) in dom (stop I) by A1, A2, Th17, Th40;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) in dom (stop (I ';' J)) by A21; :: thesis: verum

end;

suppose A23: k > LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),b₁)) in dom (stop (I ';' J))

A24: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom (stop I) by A1, A2, Th17, Th40;

hereby :: thesis: verum

per cases ( IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I or CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS ) by A1, A2, Th17, Th41;

suppose A25: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) in dom (stop (I ';' J))

consider ii being Nat such that
A26: k = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + ii by A23, NAT_1:10;
reconsider ii = ii as Element of NAT by ORDINAL1:def 13;
reconsider nn = IC (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)),ii)) as Element of NAT ;
(IC (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)),ii))) + (card I) = IC (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))),ii)) by A16, A18, A9, A20, A25, SCMPDS_6:45;
then A27: IC (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),((Initialize s) +* (stop (I ';' J))),k)) = nn + (card I) by A26, A22, EXTPRO_1:5
.= nn + (card I) ;
nn in dom (stop J) by A8, SCMPDS_6:def 2;
then nn < card (stop J) by AFINSQ_1:70;
then nn < (card J) + 1 by SCMPDS_5:7;
then A28: (card I) + nn < (card I) + ((card J) + 1) by XREAL_1:8;
card (stop (I ';' J)) = (card (I ';' J)) + 1 by SCMPDS_5:7
.= ((card I) + (card J)) + 1 by AFINSQ_1:20 ;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) in dom (stop (I ';' J)) by A28, A27, A22, AFINSQ_1:70; :: thesis: verum

end;

suppose CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) in dom (stop (I ';' J))

then IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) = IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by A23, A22, EXTPRO_1:6;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) in dom (stop (I ';' J)) by A21, A24; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence I ';' J is_closed_on s by SCMPDS_6:def 2; :: thesis: I ';' J is_halting_on s
A29: ProgramPart ((Initialize s) +* (stop (I ';' J))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by AMI_1:123;
A30: 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;
A31: ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(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:123;
A32: Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((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 ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(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 EXTPRO_1:5;

per cases ( CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS or IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ) by A1, A2, Th17, Th41;

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

then ProgramPart ((Initialize s) +* (stop (I ';' J))) halts_on (Initialize s) +* (stop (I ';' J)) by A29, EXTPRO_1:30;
hence I ';' J is_halting_on s by SCMPDS_6:def 3; :: thesis: verum

end;

suppose IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ; :: thesis: I ';' J is_halting_on s

then 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))))))) = CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(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 A16, A18, A9, A20, A30, A31, SCMPDS_6:45;
then CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((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)))))))) = 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))))))) by A32, A29
.= halt SCMPDS by A7, EXTPRO_1:def 14 ;
then ProgramPart ((Initialize s) +* (stop (I ';' J))) halts_on (Initialize s) +* (stop (I ';' J)) by EXTPRO_1:30;
hence I ';' J is_halting_on s by SCMPDS_6:def 3; :: thesis: verum

end;

end;