let s be State of SCMPDS; :: thesis: for I being halt-free Program of SCMPDS st Initialize (stop I) c= s & I is_halting_on s & card I > 0 holds
LifeSpan ((ProgramPart s),s) > 0
let I be halt-free Program of SCMPDS; :: thesis: ( Initialize (stop I) c= s & I is_halting_on s & card I > 0 implies LifeSpan ((ProgramPart s),s) > 0 )
set si = (Initialize s) +* (stop I);
assume that
A1: Initialize (stop I) c= s and
A2: I is_halting_on s and
A3: card I > 0 ; :: thesis: LifeSpan ((ProgramPart s),s) > 0
I1: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
A4: s = (Initialize s) +* (stop I) by A1, I1, FUNCT_4:79;
assume LifeSpan ((ProgramPart s),s) <= 0 ; :: thesis: contradiction
then A5: LifeSpan ((ProgramPart s),s) = 0 ;
A6: I c= Initialize (stop I) by SCMPDS_6:17;
then A7: dom I c= dom (Initialize (stop I)) by GRFUNC_1:8;
A8: 0 in dom I by A3, AFINSQ_1:70;
u: Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),0) = (Initialize s) +* (stop I) by EXTPRO_1:3;
Y: (ProgramPart ((Initialize s) +* (stop I))) /. (IC ((Initialize s) +* (stop I))) = ((Initialize s) +* (stop I)) . (IC ((Initialize s) +* (stop I))) by COMPOS_1:38;
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A2, SCMPDS_6:def 3;
then halt SCMPDS = CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),0))) by A4, A5, EXTPRO_1:def 14
.= CurInstr ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by u
.= s . 0 by A4, Y, SCMPDS_6:21
.= (Initialize (stop I)) . 0 by A1, A8, A7, GRFUNC_1:8
.= I . 0 by A8, A6, GRFUNC_1:8 ;
hence contradiction by A8, SCMPDS_5:def 3; :: thesis: verum