let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I being Program of
for J being shiftable Program of 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
for J being shiftable Program of 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 ; :: thesis: for J being shiftable Program of 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 ; :: 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, Th21;
then A5: (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;
A6: J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) by A2, A3, A4, Th21;
then A7: 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));
A8: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
A9: 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;
A10: I ';' (J ';' (Stop SCMPDS)) = stop (I ';' J) by AFINSQ_1:27;
A11: 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, Th17, A10;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27
.= I +* (Shift ((stop J),(card I))) ;
then A12: 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 A13: Shift ((stop J),(card I)) c= P +* (stop (I ';' J)) by A12, XBOOLE_1:1;
A14: dom (stop I) c= dom (stop (I ';' J)) by SCMPDS_5:13;

now :: thesis: for k being Nat holds IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J))

let k be 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, Th4, Th19;
hence IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J)) by A14; :: thesis: verum

end;

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

A16: IC (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom (stop I) by A1, A2, Th4, Th19;

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, Th4, Th20;

suppose A17: 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
A18: k = (LifeSpan ((P +* (stop I)),(Initialize s))) + ii by A15, NAT_1:10;
reconsider ii = ii as Nat ;
reconsider nn = IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),ii)) as 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 A8, A11, A9, A7, A13, A17, SCMPDS_6:31;
then A19: IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) = nn + (card I) by A18, EXTPRO_1:4;
nn in dom (stop J) by A6, SCMPDS_6:def 2;
then nn < card (stop J) by AFINSQ_1:66;
then nn < (card J) + 1 by COMPOS_1:55;
then A20: (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 A20, A19, 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 A15, EXTPRO_1:5;
hence IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J)) by A14, A16; :: 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
A21: 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, Th4, Th20;

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 A21, A8, A11, A9, A7, A13, SCMPDS_6:31
.= halt SCMPDS by A5, 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;