OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredStoredRecords.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Executed generation retaining bounded index lists

The subset generators return index lists. Wrapping them as bounded masks retains those lists; finite sets occur only in the semantic specification. The work counter includes wrapping and both Cartesian-product traversals.

  1. theorem OAI.LowSpaceSubsetSum.IndexedMask.selectedList_length line 17
  2. theorem OAI.LowSpaceSubsetSum.IndexedMask.allList_length line 22
  3. def OAI.LowSpaceSubsetSum.IndexedMask.measuredSelected line 27
  4. def OAI.LowSpaceSubsetSum.IndexedMask.measuredAll line 33
  5. theorem OAI.LowSpaceSubsetSum.IndexedMask.measuredSelected_value line 38
  6. theorem OAI.LowSpaceSubsetSum.IndexedMask.measuredAll_value line 41
  7. theorem OAI.LowSpaceSubsetSum.IndexedMask.selected_length line 44

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

  8. theorem OAI.LowSpaceSubsetSum.IndexedMask.all_length line 48

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

  9. def OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredRecords line 58
  10. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredRecords_value line 75
  11. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredRecords_cost line 80
  12. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredRecords_work line 104
  13. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.measuredStoredRecords_scale line 109