let s be State of ; :: thesis: for I being No-StopCode Program of 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 ; :: 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: inspos 0 in dom I by A3, SCMPDS_4:1;
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A2, SCMPDS_6:def 3;
then halt SCMPDS = CurInstr (Computation (s +* (Initialized (stop I))),0 ) by A4, A5, AMI_1:def 46
.= CurInstr (s +* (Initialized (stop I))) by AMI_1:13
.= s . (inspos 0 ) by A4, SCMPDS_6:21
.= (Initialized (stop I)) . (inspos 0 ) by A1, A8, A7, GRFUNC_1:8
.= I . (inspos 0 ) by A8, A6, GRFUNC_1:8 ;
hence contradiction by A8, SCMPDS_5:def 3; :: thesis: verum