let s be State of SCMPDS ; :: thesis: for I being No-StopCode Program of SCMPDS st Initialized (stop I) c= s & I is_halting_on s & card I > 0 holds
LifeSpan s > 0
let I be No-StopCode Program of SCMPDS ; :: thesis: ( Initialized (stop I) c= s & I is_halting_on s & card I > 0 implies LifeSpan s > 0 )
set II = Initialized (stop I);
set si = s +* (Initialized (stop I));
assume that
A1: Initialized (stop I) c= s and
A2: I is_halting_on s and
A3: card I > 0 ; :: thesis: LifeSpan s > 0
A4: s = s +* (Initialized (stop I)) by A1, FUNCT_4:79;
assume LifeSpan s <= 0 ; :: thesis: contradiction
then A5: LifeSpan s = 0 ;
A6: I c= Initialized (stop I) by SCMPDS_6:17;
then A7: dom I c= dom (Initialized (stop I)) by GRFUNC_1:8;
A8: 0 in dom I by A3, SCMPDS_4:1;
u: Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),0 = s +* (Initialized (stop I)) by AMI_1:13;
Y: (ProgramPart (s +* (Initialized (stop I)))) /. (IC (s +* (Initialized (stop I)))) = (s +* (Initialized (stop I))) . (IC (s +* (Initialized (stop I)))) by AMI_1:150;
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A2, SCMPDS_6:def 3;
then halt SCMPDS = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),0 )),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),0 ) by A4, A5, AMI_1:def 46
.= CurInstr (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))) by u
.= s . 0 by A4, SCMPDS_6:21, Y
.= (Initialized (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