theorem Th19: :: SCMPDS_6:28

for P being Instruction-Sequence of SCMPDS
for I being halt-free Program of
for s being State of SCMPDS
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS