OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedSeparatorPreparation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Executing the integer separator parameters before family generation

  1. abbrev OAI.LowSpaceSubsetSum.WordSeedMeasured.SeparatorPrepared line 11
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.separatorCompute line 14
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.familiesFromSeparatorData line 18
  4. def OAI.LowSpaceSubsetSum.WordSeedMeasured.familiesPrepared line 29
  5. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.separatorCompute_work line 36
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.separatorCompute_cells line 43
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.familiesPrepared_bounded line 49