let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free 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,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
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,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 ; :: 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,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 ; :: 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
A1: I is_closed_on s,P and
A2: I is_halting_on s,P and
A3: J is_closed_on IExec (I,P,s),P and
A4: 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))
A5: 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 A1, A2, A3, A4, Lm1;
J is_closed_on Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))),P +* (stop I) by A2, A3, A4, Th21, A5;
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 A1, A2, A3, A4, Lm1;
A10: IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A1, A2, A3, A4, 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));
A13: stop J c= P +* (stop J) by FUNCT_4:25;
A14: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
A15: P +* (stop I) halts_on s by A2, A5, SCMPDS_6:def 3;
then A16: Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (Result ((P +* (stop I)),s)) by EXTPRO_1:23;
A17: DataPart (IExec (I,P,s)) = DataPart (Initialize (IExec (I,P,s))) by MEMSTR_0:45;
then A18: J is_closed_on Initialize (IExec (I,P,s)),P +* (stop J) by A3, A4, SCMPDS_6:23;
A19: J is_halting_on Initialize (IExec (I,P,s)),P +* (stop J) by A3, A4, A17, SCMPDS_6:23;
I ';' J is_halting_on s,P by A1, A2, A3, A4, Th22, A5;
then A20: P +* (stop (I ';' J)) halts_on s by A5, SCMPDS_6:def 3;
J is_halting_on Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))),P +* (stop I) by A2, A3, A4, Th21, A5;
then A21: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by SCMPDS_6:def 3;
A22: IExec (I,P,s) = Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) by A15, 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 A13, A14, A18, A19, Th8, A22;
then A23: 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 A21, EXTPRO_1:23;
A24: IC (IExec ((I ';' J),P,s)) = IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s)))) by A20, 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 A1, A2, A3, A4, A16, 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 A21, EXTPRO_1:23
.= (IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))) + (card I) by A15, EXTPRO_1:23
.= (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) by A13, A14, A18, A19, Th8 ;
IExec ((I ';' J),P,s) = Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s))) by A20, 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 A1, A2, A3, A4, A16, Lm1 ;
then A25: DataPart (IExec ((I ';' J),P,s)) = DataPart (IExec (J,P,(Initialize (IExec (I,P,s))))) by A23, A12, EXTPRO_1:4;

hereby :: thesis: verum

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

A27: now :: thesis: for x being object st x in dom (IExec ((I ';' J),P,s)) holds
(IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x

let x be object ; :: 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 A28: 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 A28, SCMPDS_4:6;

suppose A29: 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 A30: not x in dom (Start-At (l,SCMPDS)) by A26, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(Initialize (IExec (I,P,s))))) . x by A25, A29, SCMPDS_4:8;
hence (IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A30, FUNCT_4:11; :: thesis: verum

end;

suppose A31: 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 A32: x in dom (Start-At (l,SCMPDS)) by FUNCOP_1:13;
thus (IExec ((I ';' J),P,s)) . x = (Start-At (l,SCMPDS)) . (IC ) by A24, A31, FUNCOP_1:72
.= (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A31, A32, 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 A27, FUNCT_1:2; :: thesis: verum

end;