let P, P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for I being halt-free Program of

for J being shiftable Program of

for s being 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

let I be halt-free Program of ; :: thesis: for J being shiftable Program of

for s being 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

let J be shiftable Program of ; :: thesis: for s being 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

let s be 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) implies ( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) )

set spJ = stop J;

set IJ = I ';' J;

set sIJ = stop (I ';' J);

set m1 = LifeSpan (P1,s);

set sm = Comput (P1,s,(LifeSpan (P1,s)));

set s3 = Initialize (Comput (P1,s,(LifeSpan (P1,s))));

set P3 = P1 +* (stop J);

set m3 = LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,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 and

A5: P2 = P +* (stop (I ';' J)) and

A6: P1 = P +* (stop I) ; :: thesis: ( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

set s4 = Comput (P2,s,(LifeSpan (P1,s)));

set P4 = P2;

A7: Initialize s = s by MEMSTR_0:44;

hence A8: IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I by A1, A2, Th4, Th23, A5, A6; :: thesis: ( DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

A9: stop J c= P1 +* (stop J) by FUNCT_4:25;

A10: DataPart (Comput (P1,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by MEMSTR_0:45;

I ';' (J ';' (Stop SCMPDS)) = stop (I ';' J) by AFINSQ_1:27;

hence A11: DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by A10, A1, A2, Th17, A6, A7, A5; :: thesis: ( Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

reconsider m = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))) as Nat ;

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= P2 by A5, FUNCT_4:25;

hence A13: Shift ((stop J),(card I)) c= P2 by A12, XBOOLE_1:1; :: thesis: LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s)))))

J is_halting_on Comput (P1,s,(LifeSpan (P1,s))),P1 by A2, A3, A4, Th21, A6, A7;

then A14: P1 +* (stop J) halts_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))) by SCMPDS_6:def 3;

A15: Comput (P2,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))) = Comput (P2,(Comput (P2,s,(LifeSpan (P1,s)))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))) by EXTPRO_1:4;

J is_closed_on Comput (P1,s,(LifeSpan (P1,s))),P1 by A2, A3, A4, Th21, A6, A7;

then A16: J is_closed_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))),P1 +* (stop J) by SCMPDS_6:24;

then CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))))) = CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))))) by A15, A9, A8, A11, A13, SCMPDS_6:31;

then A17: CurInstr (P2,(Comput (P2,s,m))) = halt SCMPDS by A14, EXTPRO_1:def 15;

m <= k ;

A24: P1 halts_on s by A2, A6, A7, SCMPDS_6:def 3;

A25: Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by A24, EXTPRO_1:23;

I ';' J is_halting_on s,P by A1, A2, A3, A4, Th22, A7;

then P2 halts_on s by A5, A7, SCMPDS_6:def 3;

hence LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) by A25, A17, A23, EXTPRO_1:def 15; :: thesis: verum

for J being shiftable Program of

for s being 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

let I be halt-free Program of ; :: thesis: for J being shiftable Program of

for s being 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

let J be shiftable Program of ; :: thesis: for s being 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

let s be 0 -started State 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 & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) implies ( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) )

set spJ = stop J;

set IJ = I ';' J;

set sIJ = stop (I ';' J);

set m1 = LifeSpan (P1,s);

set sm = Comput (P1,s,(LifeSpan (P1,s)));

set s3 = Initialize (Comput (P1,s,(LifeSpan (P1,s))));

set P3 = P1 +* (stop J);

set m3 = LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,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 and

A5: P2 = P +* (stop (I ';' J)) and

A6: P1 = P +* (stop I) ; :: thesis: ( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

set s4 = Comput (P2,s,(LifeSpan (P1,s)));

set P4 = P2;

A7: Initialize s = s by MEMSTR_0:44;

hence A8: IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I by A1, A2, Th4, Th23, A5, A6; :: thesis: ( DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

A9: stop J c= P1 +* (stop J) by FUNCT_4:25;

A10: DataPart (Comput (P1,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by MEMSTR_0:45;

I ';' (J ';' (Stop SCMPDS)) = stop (I ';' J) by AFINSQ_1:27;

hence A11: DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by A10, A1, A2, Th17, A6, A7, A5; :: thesis: ( Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

reconsider m = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))) as Nat ;

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= P2 by A5, FUNCT_4:25;

hence A13: Shift ((stop J),(card I)) c= P2 by A12, XBOOLE_1:1; :: thesis: LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s)))))

J is_halting_on Comput (P1,s,(LifeSpan (P1,s))),P1 by A2, A3, A4, Th21, A6, A7;

then A14: P1 +* (stop J) halts_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))) by SCMPDS_6:def 3;

A15: Comput (P2,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))) = Comput (P2,(Comput (P2,s,(LifeSpan (P1,s)))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))) by EXTPRO_1:4;

J is_closed_on Comput (P1,s,(LifeSpan (P1,s))),P1 by A2, A3, A4, Th21, A6, A7;

then A16: J is_closed_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))),P1 +* (stop J) by SCMPDS_6:24;

then CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))))) = CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))))) by A15, A9, A8, A11, A13, SCMPDS_6:31;

then A17: CurInstr (P2,(Comput (P2,s,m))) = halt SCMPDS by A14, EXTPRO_1:def 15;

A18: now :: thesis: for k being Nat st (LifeSpan (P1,s)) + k < m holds

not CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS

not CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS

let k be Nat; :: thesis: ( (LifeSpan (P1,s)) + k < m implies not CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS )

assume (LifeSpan (P1,s)) + k < m ; :: thesis: not CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS

then A19: k < LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))) by XREAL_1:6;

assume A20: CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS ; :: thesis: contradiction

CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),k))) = CurInstr (P2,(Comput (P2,(Comput (P2,s,(LifeSpan (P1,s)))),k))) by A9, A16, A8, A11, A13, SCMPDS_6:31

.= halt SCMPDS by A20, EXTPRO_1:4 ;

hence contradiction by A14, A19, EXTPRO_1:def 15; :: thesis: verum

end;assume (LifeSpan (P1,s)) + k < m ; :: thesis: not CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS

then A19: k < LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))) by XREAL_1:6;

assume A20: CurInstr (P2,(Comput (P2,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS ; :: thesis: contradiction

CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),k))) = CurInstr (P2,(Comput (P2,(Comput (P2,s,(LifeSpan (P1,s)))),k))) by A9, A16, A8, A11, A13, SCMPDS_6:31

.= halt SCMPDS by A20, EXTPRO_1:4 ;

hence contradiction by A14, A19, EXTPRO_1:def 15; :: thesis: verum

now :: thesis: for k being Nat st k < m holds

CurInstr (P2,(Comput (P2,s,k))) <> halt SCMPDS

then A23:
for k being Nat st CurInstr (P2,(Comput (P2,s,k))) = halt SCMPDS holds CurInstr (P2,(Comput (P2,s,k))) <> halt SCMPDS

let k be Nat; :: thesis: ( k < m implies CurInstr (P2,(Comput (P2,s,b_{1}))) <> halt SCMPDS )

assume A21: k < m ; :: thesis: CurInstr (P2,(Comput (P2,s,b_{1}))) <> halt SCMPDS

end;assume A21: k < m ; :: thesis: CurInstr (P2,(Comput (P2,s,b

per cases
( k < LifeSpan (P1,s) or LifeSpan (P1,s) <= k )
;

end;

suppose
LifeSpan (P1,s) <= k
; :: thesis: CurInstr (P2,(Comput (P2,s,b_{1}))) <> halt SCMPDS

then consider kk being Nat such that

A22: (LifeSpan (P1,s)) + kk = k by NAT_1:10;

reconsider kk = kk as Nat ;

(LifeSpan (P1,s)) + kk = k by A22;

hence CurInstr (P2,(Comput (P2,s,k))) <> halt SCMPDS by A18, A21; :: thesis: verum

end;A22: (LifeSpan (P1,s)) + kk = k by NAT_1:10;

reconsider kk = kk as Nat ;

(LifeSpan (P1,s)) + kk = k by A22;

hence CurInstr (P2,(Comput (P2,s,k))) <> halt SCMPDS by A18, A21; :: thesis: verum

m <= k ;

A24: P1 halts_on s by A2, A6, A7, SCMPDS_6:def 3;

A25: Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by A24, EXTPRO_1:23;

I ';' J is_halting_on s,P by A1, A2, A3, A4, Th22, A7;

then P2 halts_on s by A5, A7, SCMPDS_6:def 3;

hence LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) by A25, A17, A23, EXTPRO_1:def 15; :: thesis: verum