let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free 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,s),P & J is_halting_on IExec (I,P,s),P holds
IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free 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,s),P & J is_halting_on IExec (I,P,s),P holds
IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
let I be halt-free 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,s),P & J is_halting_on IExec (I,P,s),P holds
IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
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,s),P & J is_halting_on IExec (I,P,s),P implies IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) )
set IJ = I ';' J;
set s1 = s;
set P1 = P +* (stop I);
set m1 = LifeSpan ((P +* (stop I)),s);
set P2 = P +* (stop (I ';' J));
set s3 = Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))));
set sE = IExec (I,P,s);
assume that
A2: I is_closed_on s,P and
A3: I is_halting_on s,P and
A4: J is_closed_on IExec (I,P,s),P and
A5: J is_halting_on IExec (I,P,s),P ; :: thesis: IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
I: Initialize s = s by MEMSTR_0:44;
A6: DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A2, A3, A4, A5, Lm1;
J is_closed_on Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))),P +* (stop I) by A3, A4, A5, Th42, I;
then A7: J is_closed_on Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))),(P +* (stop I)) +* (stop J) by SCMPDS_6:24;
A8: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
A9: Shift ((stop J),(card I)) c= P +* (stop (I ';' J)) by A2, A3, A4, A5, Lm1;
A10: IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A2, A3, A4, A5, Lm1;
then A11: IC (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) + (card I) by A8, A6, A9, A7, SCMPDS_6:31;
A12: DataPart (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) = DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A8, A10, A6, A9, A7, SCMPDS_6:31;
set R1 = Initialize (IExec (I,P,s));
set R2 = Initialize (Result ((P +* (stop I)),s));
B18: stop J c= P +* (stop J) by FUNCT_4:25;
B19: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
A22: P +* (stop I) halts_on s by A3, SCMPDS_6:def 3, I;
then A23: Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (Result ((P +* (stop I)),s)) by EXTPRO_1:23;
A24: DataPart (IExec (I,P,s)) = DataPart (Initialize (IExec (I,P,s))) by MEMSTR_0:45;
then A25: J is_closed_on Initialize (IExec (I,P,s)),P +* (stop J) by A4, A5, SCMPDS_6:23;
A26: J is_halting_on Initialize (IExec (I,P,s)),P +* (stop J) by A4, A5, A24, SCMPDS_6:23;
I ';' J is_halting_on s,P by A2, A3, A4, A5, Th43, I;
then A30: P +* (stop (I ';' J)) halts_on s by SCMPDS_6:def 3, I;
J is_halting_on Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))),P +* (stop I) by A3, A4, A5, Th42, I;
then A31: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by SCMPDS_6:def 3;
TT: IExec (I,P,s) = Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) by A22, EXTPRO_1:23;
Result ((P +* (stop J)),(Initialize (IExec (I,P,s)))) = Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))) by B18, B19, A25, A26, Th28, TT;
then A32: IExec (J,P,(Initialize (IExec (I,P,s)))) = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))) by A31, EXTPRO_1:23;
A35: IC (IExec ((I ';' J),P,s)) = IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s)))) by A30, EXTPRO_1:23
.= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) by A2, A3, A4, A5, A23, Lm1
.= (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) + (card I) by A11, EXTPRO_1:4
.= (IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))) + (card I) by A31, EXTPRO_1:23
.= (IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))) + (card I) by A22, EXTPRO_1:23
.= (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) by B18, B19, A25, A26, Th28 ;
IExec ((I ';' J),P,s) = Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s))) by A30, EXTPRO_1:23
.= Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A2, A3, A4, A5, A23, Lm1 ;
then A36: DataPart (IExec ((I ';' J),P,s)) = DataPart (IExec (J,P,(Initialize (IExec (I,P,s))))) by A32, A12, EXTPRO_1:4;

hereby :: thesis: verum

reconsider l = (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) as Element of NAT ;
A37: dom (Start-At (l,SCMPDS)) = {(IC )} by FUNCOP_1:13;

A38: now

let x be set ; :: thesis: ( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁ )
assume A39: x in dom (IExec ((I ';' J),P,s)) ; :: thesis: (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁

per cases ( x is Int_position or x = IC ) by A39, SCMPDS_4:6;

suppose A40: x is Int_position ; :: thesis: (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁

then x <> IC by SCMPDS_2:43;
then A41: not x in dom (Start-At (l,SCMPDS)) by A37, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(Initialize (IExec (I,P,s))))) . x by A36, A40, SCMPDS_4:8;
hence (IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A41, FUNCT_4:11; :: thesis: verum

end;

suppose A42: x = IC ; :: thesis: (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁

then x in {(IC )} by TARSKI:def 1;
then A43: x in dom (Start-At (l,SCMPDS)) by FUNCOP_1:13;
thus (IExec ((I ';' J),P,s)) . x = (Start-At (l,SCMPDS)) . (IC ) by A35, A42, FUNCOP_1:72
.= (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A42, A43, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

dom (IExec ((I ';' J),P,s)) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) by PARTFUN1:def 2 ;
hence IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) by A38, FUNCT_1:2; :: thesis: verum

end;