theorem :: SCMPDS_7:26

for P being Instruction-Sequence of SCMPDS
for I being Program of
for s being State of SCMPDS
for k being Nat st 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