theorem Th25:
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 for
a being
Int-Location st ( for
d being
read-write Int-Location st
a <> d holds
s1 . d = s2 . d ) & ( for
f being
FinSeq-Location holds
s1 . f = s2 . f ) & not
I refers a &
I is_halting_on Initialized s1,
P1 holds
( ( for
d being
Int-Location st
a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for
f being
FinSeq-Location holds
(IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) &
IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )