let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS st stop I c= P & Start-At (0,SCMPDS) c= s & I is_halting_on s,P holds
LifeSpan (P,s) > 0
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being halt-free Program of SCMPDS st stop I c= P & Start-At (0,SCMPDS) c= s & I is_halting_on s,P holds
LifeSpan (P,s) > 0
let I be halt-free Program of SCMPDS; :: thesis: ( stop I c= P & Start-At (0,SCMPDS) c= s & I is_halting_on s,P implies LifeSpan (P,s) > 0 )
set si = Initialize s;
set Pi = P +* (stop I);
A3: card I > 0 ;
assume that
A1: stop I c= P and
B1: Start-At (0,SCMPDS) c= s and
A2: I is_halting_on s,P ; :: thesis: LifeSpan (P,s) > 0
A4: P = P +* (stop I) by A1, FUNCT_4:104;
A5: s = Initialize s by FUNCT_4:104, B1;
assume LifeSpan (P,s) <= 0 ; :: thesis: contradiction
then A6: LifeSpan (P,s) = 0 ;
A7: I c= stop I by AFINSQ_1:78;
then A8: dom I c= dom (stop I) by RELAT_1:25;
A9: 0 in dom I by A3, AFINSQ_1:70;
A10: Comput ((P +* (stop I)),(Initialize s),0) = Initialize s by EXTPRO_1:3;
A11: (P +* (stop I)) /. (IC (Initialize s)) = (P +* (stop I)) . (IC (Initialize s)) by PBOOLE:158;
XX: stop I c= P +* (stop I) by FUNCT_4:26;
P +* (stop I) halts_on Initialize s by A2, SCMPDS_6:def 3;
then halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),0))) by A5, A6, EXTPRO_1:def 14, A4
.= CurInstr ((P +* (stop I)),(Initialize s)) by A10
.= (P +* (stop I)) . 0 by A11, COMPOS_1:def 16
.= (stop I) . 0 by A9, A8, GRFUNC_1:8, XX
.= I . 0 by A9, A7, GRFUNC_1:8 ;
hence contradiction by A9, SCMPDS_5:def 3; :: thesis: verum