theorem Th28: :: SCMBSORT:43

for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )