theorem Th7: :: SCMRING4:7

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 b₂) -valued finite non halt-free Function
for p being non empty b₉ -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds
(Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b