OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredOrderedMixers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reading the computed mixer order into three stored domains

The only order read by this program is the three-entry integer parameter array. A length guard makes the subsequent label-array reads total.

  1. def OAI.LowSpaceSubsetSum.StoredOrderedMixers.lists line 17
  2. abbrev OAI.LowSpaceSubsetSum.StoredOrderedMixers.Domains line 20
  3. def OAI.LowSpaceSubsetSum.StoredOrderedMixers.run line 22
  4. theorem OAI.LowSpaceSubsetSum.StoredOrderedMixers.run_of_lengths line 29
  5. theorem OAI.LowSpaceSubsetSum.StoredOrderedMixers.lists_source line 36
  6. theorem OAI.LowSpaceSubsetSum.StoredOrderedMixers.complete line 49
  7. theorem OAI.LowSpaceSubsetSum.StoredOrderedMixers.work line 65