let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free Program of SCMPDS 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 SCMPDS st stop I c= P & I is_halting_on s,P holds
LifeSpan (P,s) > 0
let I be halt-free Program of SCMPDS; :: 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);
A3: card I > 0 ;
assume that
A1: stop I c= P and
A2: I is_halting_on s,P ; :: thesis: LifeSpan (P,s) > 0
B1: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A4: P = P +* (stop I) by A1, FUNCT_4:98;
A5: s = Initialize s by B1, FUNCT_4:98;
assume LifeSpan (P,s) <= 0 ; :: thesis: contradiction
then A6: LifeSpan (P,s) = 0 ;
A7: I c= stop I by AFINSQ_1:74;
then A8: dom I c= dom (stop I) by RELAT_1:11;
A9: 0 in dom I by A3, AFINSQ_1:66;
A11: (P +* (stop I)) /. (IC (Initialize s)) = (P +* (stop I)) . (IC (Initialize s)) by PBOOLE:143;
XX: stop I c= P +* (stop I) by FUNCT_4:25;
P +* (stop I) halts_on Initialize s by A2, SCMPDS_6:def 3;
then halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),0))) by A5, A6, A4, EXTPRO_1:def 15
.= CurInstr ((P +* (stop I)),(Initialize s)) by EXTPRO_1:2
.= (P +* (stop I)) . 0 by A11, MEMSTR_0:def 8
.= (stop I) . 0 by A9, A8, XX, GRFUNC_1:2
.= I . 0 by A9, A7, GRFUNC_1:2 ;
hence contradiction by A9, COMPOS_1:def 25; :: thesis: verum