theorem Th5:
for
s1,
s2 being
State of
SCM+FSA for
p1,
p2 being
Instruction-Sequence of
SCM+FSA for
I being
really-closed InitHalting Program of
SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s1 &
Initialize ((intloc 0) .--> 1) c= s2 &
I c= p1 &
I c= p2 &
s1 = s2 holds
for
k being
Nat holds
(
Comput (
p1,
s1,
k)
= Comput (
p2,
s2,
k) &
CurInstr (
p1,
(Comput (p1,s1,k)))
= CurInstr (
p2,
(Comput (p2,s2,k))) )