OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedRepresentationEmit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Executed validity, weight and mask construction for parent reports

  1. abbrev OAI.LowSpaceSubsetSum.CountedRepresentationEmit.ParentRecord line 11
  2. def OAI.LowSpaceSubsetSum.CountedRepresentationEmit.filterMask line 13
  3. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.filterMask_value line 20
  4. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.filterMask_length line 27
  5. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.filterMask_work line 32
  6. def OAI.LowSpaceSubsetSum.CountedRepresentationEmit.topIndices line 41
  7. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.topIndices_length line 44
  8. def OAI.LowSpaceSubsetSum.CountedRepresentationEmit.topMask line 52
  9. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.topMask_value line 57
  10. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.topMask_work line 64
  11. def OAI.LowSpaceSubsetSum.CountedRepresentationEmit.parentWeight line 73
  12. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.parentWeight_value line 80
  13. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.parentWeight_work line 88
  14. def OAI.LowSpaceSubsetSum.CountedRepresentationEmit.emit line 97
  15. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.emit_value line 106
  16. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.emit_work line 117
  17. theorem OAI.LowSpaceSubsetSum.CountedRepresentationEmit.emit_scale line 125