OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSchedulePreparation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Constructing the residue-loop schedule from stored arrays

  1. abbrev OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.width line 12
  2. def OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.ofStored line 14
  3. def OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.fromSuccess line 33
  4. def OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.run line 54
  5. theorem OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.coordinates_ext line 63
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.ofStored_eq line 69
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.fromSuccess_eq line 109
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.work line 119
  9. theorem OAI.LowSpaceSubsetSum.RepresentationSchedulePreparation.schedule_run_congr line 127