let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds
LifeSpan (P,s) > 0

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds
LifeSpan (P,s) > 0

let I be halt-free Program of ; :: thesis: ( stop I c= P & I is_halting_on s,P implies LifeSpan (P,s) > 0 )
set si = Initialize s;
set Pi = P +* (stop I);
assume that
A2: stop I c= P and
A3: I is_halting_on s,P ; :: thesis: LifeSpan (P,s) > 0
A4: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A5: P = P +* (stop I) by ;
A6: s = Initialize s by ;
assume LifeSpan (P,s) <= 0 ; :: thesis: contradiction
then A7: LifeSpan (P,s) = 0 ;
A8: I c= stop I by AFINSQ_1:74;
then A9: dom I c= dom (stop I) by RELAT_1:11;
A10: 0 in dom I by AFINSQ_1:66;
A11: (P +* (stop I)) /. (IC ()) = (P +* (stop I)) . (IC ()) by PBOOLE:143;
A12: stop I c= P +* (stop I) by FUNCT_4:25;
P +* (stop I) halts_on Initialize s by ;
then halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),0))) by
.= (P +* (stop I)) . 0 by
.= (stop I) . 0 by
.= I . 0 by ;
hence contradiction by A10, COMPOS_1:def 27; :: thesis: verum