let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds
LifeSpan (P,s) > 0
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds
LifeSpan (P,s) > 0
let I be halt-free Program of ; :: thesis: ( stop I c= P & I is_halting_on s,P implies LifeSpan (P,s) > 0 )
set si = Initialize s;
set Pi = P +* (stop I);
assume that
A2: stop I c= P and
A3: I is_halting_on s,P ; :: thesis: LifeSpan (P,s) > 0
A4: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A5: P = P +* (stop I) by A2, FUNCT_4:98;
A6: s = Initialize s by A4, FUNCT_4:98;
assume LifeSpan (P,s) <= 0 ; :: thesis: contradiction
then A7: LifeSpan (P,s) = 0 ;
A8: I c= stop I by AFINSQ_1:74;
then A9: dom I c= dom (stop I) by RELAT_1:11;
A10: 0 in dom I by AFINSQ_1:66;
A11: (P +* (stop I)) /. (IC (Initialize s)) = (P +* (stop I)) . (IC (Initialize s)) by PBOOLE:143;
A12: stop I c= P +* (stop I) by FUNCT_4:25;
P +* (stop I) halts_on Initialize s by A3, SCMPDS_6:def 3;
then halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),0))) by A6, A7, A5, EXTPRO_1:def 15
.= (P +* (stop I)) . 0 by A11, MEMSTR_0:def 11
.= (stop I) . 0 by A10, A9, A12, GRFUNC_1:2
.= I . 0 by A10, A8, GRFUNC_1:2 ;
hence contradiction by A10, COMPOS_1:def 27; :: thesis: verum