OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredSumReader.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Executed integer-sum counting

The initializer reads the shared half-sum arrays directly. Its tournament and the tail-recursive counter are the only evolving state; the full output stream remains a proof view. Work includes initial rows and every key read.

  1. abbrev OAI.LowSpaceSubsetSum.MeasuredSumReader.key line 16
  2. def OAI.LowSpaceSubsetSum.MeasuredSumReader.read line 18
  3. def OAI.LowSpaceSubsetSum.MeasuredSumReader.front line 22
  4. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.front_value line 30
  5. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.front_work line 39
  6. def OAI.LowSpaceSubsetSum.MeasuredSumReader.tree line 46
  7. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.tree_value line 51
  8. def OAI.LowSpaceSubsetSum.MeasuredSumReader.start line 59
  9. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.start_value line 66
  10. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.start_work line 76
  11. def OAI.LowSpaceSubsetSum.MeasuredSumReader.next line 87
  12. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.next_value line 92
  13. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.next_work line 97
  14. def OAI.LowSpaceSubsetSum.MeasuredSumReader.count line 105
  15. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.count_value line 110
  16. theorem OAI.LowSpaceSubsetSum.MeasuredSumReader.count_work line 115