OAI/Combinatorics/LowSpaceSubsetSum/Streams/RowMerge.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

A tournament merge with one current occurrence per row

The shared immutable input arrays are parameters of the row reader. Each leaf contains a row identifier, its current item, and its cursor after that item. Advancing the winning row performs one row read and one tournament replacement. The remaining lists below are ghost views used for correctness; the merge state stores no pair-product list.

  1. abbrev OAI.LowSpaceSubsetSum.RowMerge.Path line 23
  2. structure OAI.LowSpaceSubsetSum.RowMerge.Front line 25
  3. def OAI.LowSpaceSubsetSum.RowMerge.front line 30
  4. def OAI.LowSpaceSubsetSum.RowMerge.start line 33
  5. def OAI.LowSpaceSubsetSum.RowMerge.Aligned line 37
  6. theorem OAI.LowSpaceSubsetSum.RowMerge.front_row line 40
  7. theorem OAI.LowSpaceSubsetSum.RowMerge.start_aligned line 48
  8. theorem OAI.LowSpaceSubsetSum.RowMerge.start_valid line 54
  9. def OAI.LowSpaceSubsetSum.RowMerge.advance line 58
  10. theorem OAI.LowSpaceSubsetSum.RowMerge.advance_valid line 64
  11. theorem OAI.LowSpaceSubsetSum.RowMerge.advance_aligned line 77
  12. theorem OAI.LowSpaceSubsetSum.RowMerge.winner_at_own_row line 95
  13. theorem OAI.LowSpaceSubsetSum.RowMerge.winner_is_minimum line 104
  14. def OAI.LowSpaceSubsetSum.RowMerge.IsReader line 113

    Source documentation

    A row reader's finite output law, used only in the correctness proof.

    def IsReader (read : σ → Option (α × σ)) (view : σ → List α) : Prop :=
…
  15. theorem OAI.LowSpaceSubsetSum.RowMerge.cyclic_next_reader line 118
  16. def OAI.LowSpaceSubsetSum.RowMerge.remaining line 127
  17. theorem OAI.LowSpaceSubsetSum.RowMerge.start_remaining line 133
  18. theorem OAI.LowSpaceSubsetSum.RowMerge.replace_remaining line 146
  19. def OAI.LowSpaceSubsetSum.RowMerge.potential line 166
  20. theorem OAI.LowSpaceSubsetSum.RowMerge.replacement_consumes_one line 169