for P being Instruction-Sequence of SCMPDS
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