OAI/Combinatorics/LowSpaceSubsetSum/Storage/SignMaskExecution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reading the sampled sign bits into a bounded stored mask

  1. def OAI.LowSpaceSubsetSum.SignMaskExecution.run line 10
  2. theorem OAI.LowSpaceSubsetSum.SignMaskExecution.value line 16
  3. theorem OAI.LowSpaceSubsetSum.SignMaskExecution.work line 23
  4. def OAI.LowSpaceSubsetSum.SignMaskExecution.cells line 25
  5. theorem OAI.LowSpaceSubsetSum.SignMaskExecution.cells_le line 28