theorem Th14: :: SCMBSORT:15

for p1, p2 being Instruction-Sequence of SCM+FSA
for i, k being Nat
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & ( for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (Comput (p1,s1,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) )