theorem Th26: :: SCMBSORT:41

for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( s . (fsloc 0),(IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . (fsloc 0)) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . i & x2 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )