theorem Th14:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1 being
0 -started State of
SCM+FSA for
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I c= P1 &
I is_pseudo-closed_on s1,
P1 holds
for
n being
Nat st
Reloc (
I,
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
( ( for
i being
Nat st
i < pseudo-LifeSpan (
s1,
P1,
I) holds
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
n)
= CurInstr (
P2,
(Comput (P2,s2,i))) ) & ( for
i being
Nat st
i <= pseudo-LifeSpan (
s1,
P1,
I) holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )