OAI/Combinatorics/LowSpaceSubsetSum/Streams/ReaderMap.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Semantic maps for the mutable reader structures

Mapping records preserves the tournament paths and all cursor coordinates. Immutable backing arrays are mapped once; they are not copied by a read.

  1. def OAI.LowSpaceSubsetSum.Tournament.map line 17
  2. theorem OAI.LowSpaceSubsetSum.Tournament.winner_map line 21
  3. theorem OAI.LowSpaceSubsetSum.Tournament.nodes_map line 24
  4. theorem OAI.LowSpaceSubsetSum.Tournament.pick_map line 30
  5. theorem OAI.LowSpaceSubsetSum.Tournament.node_map line 35
  6. theorem OAI.LowSpaceSubsetSum.Tournament.valid_map line 39
  7. theorem OAI.LowSpaceSubsetSum.Tournament.lookup_map line 47
  8. theorem OAI.LowSpaceSubsetSum.Tournament.replace_map line 55
  9. theorem OAI.LowSpaceSubsetSum.Tournament.build_map line 64
  10. theorem OAI.LowSpaceSubsetSum.CyclicCursor.trace_map line 78
  11. def OAI.LowSpaceSubsetSum.SliceCursor.mapRange line 92
  12. def OAI.LowSpaceSubsetSum.SliceCursor.mapState line 95
  13. theorem OAI.LowSpaceSubsetSum.SliceCursor.values_map line 98
  14. theorem OAI.LowSpaceSubsetSum.SliceCursor.next_map line 102
  15. theorem OAI.LowSpaceSubsetSum.SliceCursor.output_map line 112
  16. def OAI.LowSpaceSubsetSum.PairCursor.mapState line 129
  17. theorem OAI.LowSpaceSubsetSum.PairCursor.next_map line 132
  18. theorem OAI.LowSpaceSubsetSum.PairCursor.output_map line 141
  19. def OAI.LowSpaceSubsetSum.FilteredStream.mapCursor line 156
  20. theorem OAI.LowSpaceSubsetSum.FilteredStream.read_map line 160
  21. theorem OAI.LowSpaceSubsetSum.FilteredStream.view_map line 171
  22. theorem OAI.LowSpaceSubsetSum.PaddedRows.rows_map line 183
  23. def OAI.LowSpaceSubsetSum.RowMerge.mapFront line 194
  24. theorem OAI.LowSpaceSubsetSum.RowMerge.front_map line 197
  25. theorem OAI.LowSpaceSubsetSum.RowMerge.start_map line 207
  26. theorem OAI.LowSpaceSubsetSum.RowMerge.advance_map line 223
  27. theorem OAI.LowSpaceSubsetSum.RowMerge.aligned_map line 246
  28. theorem OAI.LowSpaceSubsetSum.RowMerge.remaining_map line 255
  29. theorem OAI.LowSpaceSubsetSum.RowMerge.rowsSorted_map line 266
  30. theorem OAI.LowSpaceSubsetSum.RowMerge.potential_map line 275
  31. theorem OAI.LowSpaceSubsetSum.RowMerge.trace_map line 285
  32. def OAI.LowSpaceSubsetSum.MergedReader.mapState line 313
  33. theorem OAI.LowSpaceSubsetSum.MergedReader.next_map line 322
  34. theorem OAI.LowSpaceSubsetSum.MergedReader.output_map line 347