theorem Th13: :: SCMPDS_5:25

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of
for k being Nat st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds
Comput (P,s,k) = Comput ((P +* (stop I)),s,k)