theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= SubFrom (
da,
db) &
da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)