theorem :: SCMFSA_3:13

for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b₁ -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
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = |.((Comput (P1,s1,i)) . db).| & k2 = |.((Comput (P2,s2,i)) . db).| holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2