OAI/Combinatorics/LowSpaceSubsetSum/Streams/FilteredStream.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The complete executable modular pair stream

Concrete lexicographic sorting, binary slice/pivot row initialization, empty leaf padding and tournament merging are composed here. The actual merge state stores only its tree of constant-size row cursors. All Cartesian lists and multisets in the statements are proof views.

  1. inductive OAI.LowSpaceSubsetSum.FilteredStream.Mode line 20
  2. def OAI.LowSpaceSubsetSum.FilteredStream.key line 24
  3. def OAI.LowSpaceSubsetSum.FilteredStream.steps line 28
  4. theorem OAI.LowSpaceSubsetSum.FilteredStream.steps_sufficient line 30
  5. theorem OAI.LowSpaceSubsetSum.FilteredStream.steps_le_index_bits line 36
  6. def OAI.LowSpaceSubsetSum.FilteredStream.row line 39
  7. theorem OAI.LowSpaceSubsetSum.FilteredStream.row_sorted line 48
  8. theorem OAI.LowSpaceSubsetSum.FilteredStream.row_perm line 57
  9. abbrev OAI.LowSpaceSubsetSum.FilteredStream.Cursor line 66
  10. def OAI.LowSpaceSubsetSum.FilteredStream.read line 68
  11. def OAI.LowSpaceSubsetSum.FilteredStream.view line 71
  12. theorem OAI.LowSpaceSubsetSum.FilteredStream.reader line 74
  13. def OAI.LowSpaceSubsetSum.FilteredStream.rowArray line 77
  14. theorem OAI.LowSpaceSubsetSum.FilteredStream.array_sorted line 81
  15. def OAI.LowSpaceSubsetSum.FilteredStream.start line 92
  16. theorem OAI.LowSpaceSubsetSum.FilteredStream.output_bag line 100
  17. def OAI.LowSpaceSubsetSum.FilteredStream.sortedStart line 123
  18. theorem OAI.LowSpaceSubsetSum.FilteredStream.sorted_output_bag line 130
  19. theorem OAI.LowSpaceSubsetSum.FilteredStream.sorted_output_sorted line 144
  20. theorem OAI.LowSpaceSubsetSum.FilteredStream.state_nodes line 151
  21. theorem OAI.LowSpaceSubsetSum.FilteredStream.sorted_output_mem line 156