OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationStoredRecords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Retaining generated mask lists in raw-leaf records

Masks are wrapped at the point they are generated. Their finite-set views are used only by the correctness statements. No canonical sorting or reconstruction of a finite set is performed for an emitted record.

  1. theorem OAI.LowSpaceSubsetSum.IndexedMask.selected_length line 18

    Distinct definitions of this name: OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredStoredRecords.lean:44 (different declaration text). Qualify references as OAI.LowSpaceSubsetSum.IndexedMask.selected_length@path.

  2. theorem OAI.LowSpaceSubsetSum.IndexedMask.all_length line 23

    Distinct definitions of this name: OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredStoredRecords.lean:48 (different declaration text). Qualify references as OAI.LowSpaceSubsetSum.IndexedMask.all_length@path.

  3. def OAI.LowSpaceSubsetSum.IndexedMask.selected line 28
  4. def OAI.LowSpaceSubsetSum.IndexedMask.all line 32
  5. theorem OAI.LowSpaceSubsetSum.IndexedMask.selected_semantic line 36
  6. theorem OAI.LowSpaceSubsetSum.IndexedMask.all_semantic line 41
  7. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.map_product line 52
  8. def OAI.LowSpaceSubsetSum.RepresentationLeaf.storedRecords line 60
  9. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.storedRecords_semantic line 71
  10. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.storedRecords_length line 85
  11. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.storedRecords_mem line 90
  12. theorem OAI.LowSpaceSubsetSum.ResidueSort.map_sort line 102
  13. def OAI.LowSpaceSubsetSum.RepresentationPairData.leftRecords line 114
  14. def OAI.LowSpaceSubsetSum.RepresentationPairData.rawRightRecords line 117
  15. def OAI.LowSpaceSubsetSum.RepresentationPairData.rightRecords line 120
  16. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.leftRecords_semantic line 123
  17. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.rawRightRecords_semantic line 129
  18. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.rightRecords_semantic line 136
  19. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.leftRecords_size line 140
  20. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.rightRecords_size line 144