OAI/Combinatorics/LowSpaceSubsetSum/Storage/SubsetCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Memory of concrete subset-family generation

The trace retains the first recursive family while generating the second, then counts append/map output alongside both families. Its work projection is exactly the output-sensitive generator.

  1. def OAI.LowSpaceSubsetSum.SubsetCells.all line 16
  2. theorem OAI.LowSpaceSubsetSum.SubsetCells.all_value line 23
  3. theorem OAI.LowSpaceSubsetSum.SubsetCells.all_cells line 28
  4. def OAI.LowSpaceSubsetSum.SubsetCells.select line 44
  5. theorem OAI.LowSpaceSubsetSum.SubsetCells.select_value line 59
  6. theorem OAI.LowSpaceSubsetSum.SubsetCells.select_step line 69
  7. theorem OAI.LowSpaceSubsetSum.SubsetCells.select_cells line 99
  8. theorem OAI.LowSpaceSubsetSum.SubsetCells.select_cells_card line 132