theorem Th62:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
I being
really-closed Program of
SCM+FSA st
I is_halting_on s1,
P1 &
DataPart s1 = DataPart s2 holds
for
k being
Nat holds
(
Comput (
(P1 +* I),
(Initialize s1),
k)
= Comput (
(P2 +* I),
(Initialize s2),
k) &
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),k)))
= CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),k))) )