OAI/Combinatorics/LowSpaceSubsetSum/Storage/BackgroundPreparationCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Live storage for the allocated background construction

The scanned outside list is shared by all eight row copies. The six integer width computations run before the size guard and are charged on both branches.

  1. def OAI.LowSpaceSubsetSum.BackgroundPreparationCells.assemble line 20
  2. def OAI.LowSpaceSubsetSum.BackgroundPreparationCells.core line 28
  3. theorem OAI.LowSpaceSubsetSum.BackgroundPreparationCells.core_value line 38
  4. def OAI.LowSpaceSubsetSum.BackgroundPreparationCells.run line 45
  5. theorem OAI.LowSpaceSubsetSum.BackgroundPreparationCells.value line 50
  6. theorem OAI.LowSpaceSubsetSum.BackgroundPreparationCells.cells line 63