theorem Th21:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
Directed I is_pseudo-closed_on s,
P holds
(
I ";" (Stop SCM+FSA) is_halting_on s,
P &
LifeSpan (
(P +* (I ";" (Stop SCM+FSA))),
(Initialize s))
= pseudo-LifeSpan (
s,
P,
(Directed I)) & ( for
n being
Nat st
n < pseudo-LifeSpan (
s,
P,
(Directed I)) holds
IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) & ( for
n being
Nat st
n <= pseudo-LifeSpan (
s,
P,
(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )