let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I being Program of SCMPDS
for J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
let P be Instruction-Sequence of SCMPDS; :: thesis: for I being Program of SCMPDS
for J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
let I be Program of SCMPDS; :: thesis: for J being shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
let J be shiftable Program of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P implies ( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P ) )
set sE = IExec (I,P,(Initialize s));
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P and
A3: J is_closed_on IExec (I,P,(Initialize s)),P and
A4: J is_halting_on IExec (I,P,(Initialize s)),P ; :: thesis: ( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set spI = stop I;
set ss = Initialize s;
set PP = P +* (stop (I ';' J));
set spJ = stop J;
set s1 = Initialize s;
set P1 = P +* (stop I);
set m1 = LifeSpan ((P +* (stop I)),(Initialize s));
set sm = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set s3 = Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))));
J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) by A2, A3, A4, Th42;
then A7: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by SCMPDS_6:def 3;
A8: J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) by A2, A3, A4, Th42;
then A9: J is_closed_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),(P +* (stop I)) +* (stop J) by SCMPDS_6:24;
set s4 = Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P4 = P +* (stop (I ';' J));
A16: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
A17: DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by MEMSTR_0:45;
XX: I ';' (J ';' (Stop SCMPDS)) = stop (I ';' J) by AFINSQ_1:27;
B18: Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))) = Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))) by A1, A2, Th38, XX;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27
.= I +* (Shift ((stop J),(card I))) ;
then A19: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:25;
stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25;
then A20: Shift ((stop J),(card I)) c= P +* (stop (I ';' J)) by A19, XBOOLE_1:1;
A21: dom (stop I) c= dom (stop (I ';' J)) by SCMPDS_5:13;

now

let k be Element of NAT ; :: thesis: IC (Comput ((P +* (stop (I ';' J))),(Initialize s),b₁)) in dom (stop (I ';' J))

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

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

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

end;

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

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

hereby :: thesis: verum

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

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

consider ii being Nat such that
A26: k = (LifeSpan ((P +* (stop I)),(Initialize s))) + ii by A23, NAT_1:10;
reconsider ii = ii as Element of NAT by ORDINAL1:def 12;
reconsider nn = IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),ii)) as Element of NAT ;
(IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),ii))) + (card I) = IC (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),ii)) by A16, B18, A17, A9, A20, A25, SCMPDS_6:31;
then A27: IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) = nn + (card I) by A26, EXTPRO_1:4;
nn in dom (stop J) by A8, SCMPDS_6:def 2;
then nn < card (stop J) by AFINSQ_1:66;
then nn < (card J) + 1 by COMPOS_1:55;
then A28: (card I) + nn < (card I) + ((card J) + 1) by XREAL_1:6;
card (stop (I ';' J)) = (card (I ';' J)) + 1 by COMPOS_1:55
.= ((card I) + (card J)) + 1 by AFINSQ_1:17 ;
hence IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J)) by A28, A27, AFINSQ_1:66; :: thesis: verum

end;

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

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

end;

end;

end;

end;

end;

end;

hence I ';' J is_closed_on s,P by SCMPDS_6:def 2; :: thesis: I ';' J is_halting_on s,P
A32: Comput ((P +* (stop (I ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) = Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))) by EXTPRO_1:4;

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

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

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

end;

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

then CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))) = CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))) by A32, A16, B18, A17, A9, A20, SCMPDS_6:31
.= halt SCMPDS by A7, EXTPRO_1:def 15 ;
then P +* (stop (I ';' J)) halts_on Initialize s by EXTPRO_1:29;
hence I ';' J is_halting_on s,P by SCMPDS_6:def 3; :: thesis: verum

end;

end;