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;

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;

.= 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;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

dom (IExec ((I ';' J),P,s)) =
the carrier of SCMPDS
by PARTFUN1:def 2
(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_{1} = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b_{1} )

assume A28: x in dom (IExec ((I ';' J),P,s)) ; :: thesis: (IExec ((I ';' J),P,s)) . b_{1} = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b_{1}

end;assume A28: x in dom (IExec ((I ';' J),P,s)) ; :: thesis: (IExec ((I ';' J),P,s)) . b

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

end;

suppose A29:
x is Int_position
; :: thesis: (IExec ((I ';' J),P,s)) . b_{1} = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b_{1}

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;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

suppose A31:
x = IC
; :: thesis: (IExec ((I ';' J),P,s)) . b_{1} = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b_{1}

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;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

.= 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