OAI/Combinatorics/LowSpaceSubsetSum/Streams/MergedReader.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The executable tournament merge as a finite reader

Only the tournament and its row cursors are stored. The complete output list is a proof view, defined by the remaining-occurrence potential. The reader law connects this actual merge to the stopped joins and bounded dictionaries.

  1. structure OAI.LowSpaceSubsetSum.MergedReader.State line 20
  2. theorem OAI.LowSpaceSubsetSum.MergedReader.advance_sorted line 26
  3. theorem OAI.LowSpaceSubsetSum.MergedReader.advance_consumes_one line 41
  4. def OAI.LowSpaceSubsetSum.MergedReader.next line 56
  5. def OAI.LowSpaceSubsetSum.MergedReader.output line 67

    Source documentation

    The output view is never a field of the executable state.

    def output (key : α → ℤ) (read : σ → Option (α × σ))
    (view : σ → List α) (s : State key view d) : List α :=
…

    Mentions: OAI.LowSpaceSubsetSum.MergedReader.State

  6. theorem OAI.LowSpaceSubsetSum.MergedReader.next_none line 71
  7. theorem OAI.LowSpaceSubsetSum.MergedReader.next_some line 82
  8. theorem OAI.LowSpaceSubsetSum.MergedReader.reader line 100
  9. theorem OAI.LowSpaceSubsetSum.MergedReader.output_bag line 117
  10. theorem OAI.LowSpaceSubsetSum.MergedReader.output_length line 123
  11. theorem OAI.LowSpaceSubsetSum.MergedReader.output_sorted line 130
  12. def OAI.LowSpaceSubsetSum.MergedReader.start line 136
  13. theorem OAI.LowSpaceSubsetSum.MergedReader.start_output_bag line 146
  14. theorem OAI.LowSpaceSubsetSum.MergedReader.start_output_length line 155
  15. theorem OAI.LowSpaceSubsetSum.MergedReader.nodes_exact line 164
  16. def OAI.LowSpaceSubsetSum.MergedReader.advanceComparisons line 167
  17. theorem OAI.LowSpaceSubsetSum.MergedReader.advanceComparisons_le line 172