OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationStreams.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Concrete sorted raw-child streams for representation

  1. structure OAI.LowSpaceSubsetSum.RepresentationPairData line 13

    Source documentation

    Runtime fields for one low-filtered child-pair stream.

    structure RepresentationPairData (n : ℕ) where
…
  2. abbrev OAI.LowSpaceSubsetSum.RepresentationPairData.Occ line 29
  3. def OAI.LowSpaceSubsetSum.RepresentationPairData.wl line 31
  4. def OAI.LowSpaceSubsetSum.RepresentationPairData.leftArray line 33
  5. def OAI.LowSpaceSubsetSum.RepresentationPairData.rightArray line 35
  6. def OAI.LowSpaceSubsetSum.RepresentationPairData.storedRight line 37
  7. abbrev OAI.LowSpaceSubsetSum.RepresentationPairData.State line 40
  8. def OAI.LowSpaceSubsetSum.RepresentationPairData.start line 43
  9. def OAI.LowSpaceSubsetSum.RepresentationPairData.read line 47
  10. def OAI.LowSpaceSubsetSum.RepresentationPairData.output line 52
  11. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.read_law line 56
  12. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_mem line 59
  13. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_sorted line 70
  14. def OAI.LowSpaceSubsetSum.RepresentationPairData.lengthBound line 76
  15. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_length_le line 78
  16. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.state_nodes line 96