theorem Th17:
for
s being
State of
SCM+FSA for
P being
Instruction-Sequence of
SCM+FSA for
I being
really-closed Program of
SCM+FSA for
J being
Program of
SCM+FSA st
I is_halting_on s,
P holds
( ( for
k being
Nat st
k <= LifeSpan (
(P +* I),
(Initialize s)) holds
(
IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) &
CurInstr (
(P +* (Directed I)),
(Comput ((P +* (Directed I)),(Initialize s),k)))
= CurInstr (
(P +* (I ";" J)),
(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) &
DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) &
IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )