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
A4: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
A5: s = (Initialize s) +* (stop I) by A1, A4, FUNCT_4:79;
assume LifeSpan ((ProgramPart s),s) <= 0 ; :: thesis: contradiction
then A6: LifeSpan ((ProgramPart s),s) = 0 ;
A7: I c= Initialize (stop I) by SCMPDS_6:17;
then A8: dom I c= dom (Initialize (stop I)) by GRFUNC_1:8;
A9: 0 in dom I by A3, AFINSQ_1:70;
A10: Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),0) = (Initialize s) +* (stop I) by EXTPRO_1:3;
A11: (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 A5, A6, EXTPRO_1:def 14
.= CurInstr ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by A10
.= s . 0 by A5, A11, SCMPDS_6:21
.= (Initialize (stop I)) . 0 by A1, A9, A8, GRFUNC_1:8
.= I . 0 by A9, A7, GRFUNC_1:8 ;
hence contradiction by A9, SCMPDS_5:def 3; :: thesis: verum