:: deftheorem Def14 defines arr_computation EXCHSORT:def 14 :
for O being non empty connected Poset
for R being array of O
for b₃ being non empty array holds
( b₃ is arr_computation of R iff ( b₃ . (base- b₃) = R & ( for a being Ordinal st a in dom b₃ holds
b₃ . a is array of O ) & ( for a being Ordinal st a in dom b₃ & succ a in dom b₃ holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & b₃ . a = R & b₃ . (succ a) = Swap (R,x,y) ) ) ) );