theorem Th13: :: SCMBSORT:14

for p1, p2 being Instruction-Sequence of SCM+FSA
for i, k being Nat
for t being FinPartState of SCM+FSA
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( 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)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )