theorem Th2:
for
P being
Instruction-Sequence of
SCMPDS for
s,
sm being
State of
SCMPDS for
I being
halt-free shiftable Program of
for
a being
Int_position for
i being
Integer for
m being
Nat st
I is_closed_on s,
P &
I is_halting_on s,
P &
s . (DataLoc ((s . a),i)) > 0 &
m = (LifeSpan ((P +* (stop I)),(Initialize s))) + 2 &
sm = Comput (
(P +* (stop (while>0 (a,i,I)))),
(Initialize s),
m) holds
(
DataPart sm = DataPart (IExec (I,P,(Initialize s))) &
Initialize sm = sm )