OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredLeafCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Constructing all eight finite leaf profiles from stored lists

The three sets in a profile are built by the explicit tail insertion loop. All eight completed profiles are cached before returning the index view.

  1. def OAI.LowSpaceSubsetSum.StoredLeafCells.leaf line 18
  2. theorem OAI.LowSpaceSubsetSum.StoredLeafCells.leaf_value line 43
  3. theorem OAI.LowSpaceSubsetSum.StoredLeafCells.size_le line 61
  4. theorem OAI.LowSpaceSubsetSum.StoredLeafCells.leaf_cells line 65
  5. def OAI.LowSpaceSubsetSum.StoredLeafCells.run line 90
  6. theorem OAI.LowSpaceSubsetSum.StoredLeafCells.value line 99
  7. theorem OAI.LowSpaceSubsetSum.StoredLeafCells.cells line 104