let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for I being parahalting Program of

for k being Nat st k < LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) in dom I

let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of

for k being Nat st k < LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) in dom I

let I be parahalting Program of ; :: thesis: for k being Nat st k < LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) in dom I

let k be Nat; :: thesis: ( k < LifeSpan ((P +* (stop I)),s) implies IC (Comput ((P +* (stop I)),s,k)) in dom I )

set ss = s;

set PP = P +* (stop I);

set m = LifeSpan ((P +* (stop I)),s);

set Sk = Comput ((P +* (stop I)),s,k);

set Ik = IC (Comput ((P +* (stop I)),s,k));

A1: stop I c= P +* (stop I) by FUNCT_4:25;

then A2: P +* (stop I) halts_on s by SCMPDS_4:def 7;

reconsider n = IC (Comput ((P +* (stop I)),s,k)) as Nat ;

A3: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A1, SCMPDS_4:def 6;

A4: stop I c= P +* (stop I) by FUNCT_4:25;

assume A5: k < LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop I)),s,k)) in dom I

then n < (card I) + 1 by A3, AFINSQ_1:66;

then n <= card I by INT_1:7;

then n < card I by A6, XXREAL_0:1;

hence IC (Comput ((P +* (stop I)),s,k)) in dom I by AFINSQ_1:66; :: thesis: verum

for I being parahalting Program of

for k being Nat st k < LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) in dom I

let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of

for k being Nat st k < LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) in dom I

let I be parahalting Program of ; :: thesis: for k being Nat st k < LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) in dom I

let k be Nat; :: thesis: ( k < LifeSpan ((P +* (stop I)),s) implies IC (Comput ((P +* (stop I)),s,k)) in dom I )

set ss = s;

set PP = P +* (stop I);

set m = LifeSpan ((P +* (stop I)),s);

set Sk = Comput ((P +* (stop I)),s,k);

set Ik = IC (Comput ((P +* (stop I)),s,k));

A1: stop I c= P +* (stop I) by FUNCT_4:25;

then A2: P +* (stop I) halts_on s by SCMPDS_4:def 7;

reconsider n = IC (Comput ((P +* (stop I)),s,k)) as Nat ;

A3: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A1, SCMPDS_4:def 6;

A4: stop I c= P +* (stop I) by FUNCT_4:25;

assume A5: k < LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop I)),s,k)) in dom I

A6: now :: thesis: not n = card I

card (stop I) = (card I) + 1
by Lm1, AFINSQ_1:17;assume A7:
n = card I
; :: thesis: contradiction

A8: 0 in dom (Stop SCMPDS) by COMPOS_1:3;

A9: (Stop SCMPDS) . 0 = halt SCMPDS ;

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:143

.= (stop I) . (0 + n) by A3, A4, GRFUNC_1:2

.= halt SCMPDS by A7, A9, A8, AFINSQ_1:def 3 ;

hence contradiction by A5, A2, EXTPRO_1:def 15; :: thesis: verum

end;A8: 0 in dom (Stop SCMPDS) by COMPOS_1:3;

A9: (Stop SCMPDS) . 0 = halt SCMPDS ;

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:143

.= (stop I) . (0 + n) by A3, A4, GRFUNC_1:2

.= halt SCMPDS by A7, A9, A8, AFINSQ_1:def 3 ;

hence contradiction by A5, A2, EXTPRO_1:def 15; :: thesis: verum

then n < (card I) + 1 by A3, AFINSQ_1:66;

then n <= card I by INT_1:7;

then n < card I by A6, XXREAL_0:1;

hence IC (Comput ((P +* (stop I)),s,k)) in dom I by AFINSQ_1:66; :: thesis: verum