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 SCMPDS_4:5;
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 AMI_1:13;
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, AMI_1:def 46
.= 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