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

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