theorem :: SCMFSA_3:14

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))) = (f,db) := da & f in dom p holds
for k1, k2 being Nat st k1 = |.((Comput (P1,s1,i)) . db).| & k2 = |.((Comput (P2,s2,i)) . db).| holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))