theorem Th8:
for
n being
Nat for
R being non
trivial Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) for
P1,
P2 being
Instruction-Sequence of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b9 -autonomic FinPartState of
(SCM R) st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 &
CurInstr (
P1,
(Comput (P1,s1,n)))
= AddTo (
a,
b) &
a in dom p holds
((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b)