theorem Th9:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
0 -started State of
SCM+FSA for
I being
really-closed Program of
SCM+FSA st
I c= P1 &
I c= P2 &
DataPart s1 = DataPart s2 holds
for
i being
Nat holds
(
IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )