OAI/Combinatorics/LowSpaceSubsetSum/Streams/JoinReaderMap.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Stored-record erasure through buffered joins

The erasure maps both emitted records and reader cursors. Counters and stop flags are preserved, so the work ledger can be transferred to the source parent task without changing the order of equal-weight occurrences.

  1. def OAI.LowSpaceSubsetSum.TieBuffer.mapAll line 20
  2. theorem OAI.LowSpaceSubsetSum.TieBuffer.fillAcc_map line 23
  3. theorem OAI.LowSpaceSubsetSum.TieBuffer.fill_map line 41
  4. theorem OAI.LowSpaceSubsetSum.TieBuffer.hasKey_map line 48
  5. def OAI.LowSpaceSubsetSum.TieReplay.mapAll line 59
  6. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_map line 62
  7. theorem OAI.LowSpaceSubsetSum.TieReplay.run_map line 85
  8. theorem OAI.LowSpaceSubsetSum.BufferReplay.read_map line 99
  9. theorem OAI.LowSpaceSubsetSum.BufferReplay.run_map line 104
  10. theorem OAI.LowSpaceSubsetSum.JoinOne.run_map line 118
  11. def OAI.LowSpaceSubsetSum.TieGroup.mapReaders line 147
  12. def OAI.LowSpaceSubsetSum.TieGroup.mapReadersResult line 150
  13. theorem OAI.LowSpaceSubsetSum.TieGroup.step_mapReaders line 155
  14. theorem OAI.LowSpaceSubsetSum.TieGroup.run_mapReaders line 168
  15. def OAI.LowSpaceSubsetSum.StreamJoin.mapReaders line 203
  16. def OAI.LowSpaceSubsetSum.StreamJoin.mapReadersStopped line 206
  17. theorem OAI.LowSpaceSubsetSum.StreamJoin.step_mapReaders line 210
  18. theorem OAI.LowSpaceSubsetSum.StreamJoin.stoppedAcc_mapReaders line 241