OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSortCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Stored-record sorting with explicit live-cell accounting

The comparison function executes both bounded-list weight evaluations. The array, its list view, merge recursion, and final array allocation are included.

  1. def OAI.LowSpaceSubsetSum.RepresentationSortCells.compare line 17
  2. theorem OAI.LowSpaceSubsetSum.RepresentationSortCells.compare_value line 24
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSortCells.compare_cells line 28
  4. def OAI.LowSpaceSubsetSum.RepresentationSortCells.sort line 36
  5. theorem OAI.LowSpaceSubsetSum.RepresentationSortCells.sort_value line 41
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSortCells.bound line 49
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSortCells.sort_cells line 75