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

for J being parahalting shiftable Program of

for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds

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

set D = SCM-Data-Loc ;

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

for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds

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

let J be parahalting shiftable Program of ; :: thesis: for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds

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

let s be 0 -started State of SCMPDS; :: thesis: ( stop (I ';' J) c= P & P1 = P +* (stop I) implies ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) )

set spJ = stop J;

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

set m1 = 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))))));

assume that

A1: stop (I ';' J) c= P and

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

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

set P4 = P;

A3: I c= stop (I ';' J) by Th1;

hence A4: IC (Comput (P,s,(LifeSpan (P1,s)))) = card I by A1, A2, Th14, XBOOLE_1:1; :: thesis: ( DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,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 A5: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:25;

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

then A7: P1 +* (stop J) halts_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))) by SCMPDS_4:def 7;

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

I ';' J c= stop (I ';' J) by AFINSQ_1:74;

then P +* (I ';' J) = P by A1, FUNCT_4:98, XBOOLE_1:1;

hence A9: DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by A8, A2, Th17; :: thesis: ( Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

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

thus A11: Shift ((stop J),(card I)) c= P by A5, A1; :: thesis: LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s)))))

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 (P,(Comput (P,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))))) by A10, A6, A4, A9, SCMPDS_4:29;

then A12: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A7, EXTPRO_1:def 15;

m <= k ;

stop I c= P1 by A2, FUNCT_4:25;

then P1 halts_on s by SCMPDS_4:def 7;

then A20: Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by EXTPRO_1:23;

P halts_on s by A1, SCMPDS_4:def 7;

hence LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) by A20, A12, A19, EXTPRO_1:def 15; :: thesis: verum

for J being parahalting shiftable Program of

for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds

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

set D = SCM-Data-Loc ;

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

for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds

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

let J be parahalting shiftable Program of ; :: thesis: for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds

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

let s be 0 -started State of SCMPDS; :: thesis: ( stop (I ';' J) c= P & P1 = P +* (stop I) implies ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) )

set spJ = stop J;

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

set m1 = 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))))));

assume that

A1: stop (I ';' J) c= P and

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

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

set P4 = P;

A3: I c= stop (I ';' J) by Th1;

hence A4: IC (Comput (P,s,(LifeSpan (P1,s)))) = card I by A1, A2, Th14, XBOOLE_1:1; :: thesis: ( DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,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 A5: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:25;

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

then A7: P1 +* (stop J) halts_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))) by SCMPDS_4:def 7;

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

I ';' J c= stop (I ';' J) by AFINSQ_1:74;

then P +* (I ';' J) = P by A1, FUNCT_4:98, XBOOLE_1:1;

hence A9: DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by A8, A2, Th17; :: thesis: ( Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

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

thus A11: Shift ((stop J),(card I)) c= P by A5, A1; :: thesis: LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s)))))

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 (P,(Comput (P,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))))) by A10, A6, A4, A9, SCMPDS_4:29;

then A12: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A7, EXTPRO_1:def 15;

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

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

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

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

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

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

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

A16: Comput (P,s,((LifeSpan (P1,s)) + k)) = Comput (P,(Comput (P,s,(LifeSpan (P1,s)))),k) by EXTPRO_1:4;

CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),k))) = halt SCMPDS by A15, A16, A6, A4, A9, A11, SCMPDS_4:29;

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

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

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

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

A16: Comput (P,s,((LifeSpan (P1,s)) + k)) = Comput (P,(Comput (P,s,(LifeSpan (P1,s)))),k) by EXTPRO_1:4;

CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),k))) = halt SCMPDS by A15, A16, A6, A4, A9, A11, SCMPDS_4:29;

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

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

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

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

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

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

end;assume A17: k < m ; :: thesis: CurInstr (P,(Comput (P,s,b

m <= k ;

stop I c= P1 by A2, FUNCT_4:25;

then P1 halts_on s by SCMPDS_4:def 7;

then A20: Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by EXTPRO_1:23;

P halts_on s by A1, SCMPDS_4:def 7;

hence LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) by A20, A12, A19, EXTPRO_1:def 15; :: thesis: verum