OAI/Combinatorics/LowSpaceSubsetSum/Streams/JoinUserMap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Erasing proof-carrying callback states through the actual join

This refinement lets a counted dictionary carry its invariant intrinsically, while retaining exactly the original join's cursors, counters and halt behavior.

  1. def OAI.LowSpaceSubsetSum.TieReplay.mapUser line 18
  2. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_mapUser line 21
  3. theorem OAI.LowSpaceSubsetSum.TieReplay.run_mapUser line 42
  4. theorem OAI.LowSpaceSubsetSum.JoinOne.run_mapUser line 54
  5. def OAI.LowSpaceSubsetSum.TieGroup.mapUser line 82
  6. def OAI.LowSpaceSubsetSum.TieGroup.mapResult line 85
  7. theorem OAI.LowSpaceSubsetSum.TieGroup.step_mapUser line 88
  8. theorem OAI.LowSpaceSubsetSum.TieGroup.run_mapUser line 98
  9. def OAI.LowSpaceSubsetSum.StreamJoin.mapUser line 123
  10. def OAI.LowSpaceSubsetSum.StreamJoin.mapStopped line 126
  11. theorem OAI.LowSpaceSubsetSum.StreamJoin.step_mapUser line 129
  12. theorem OAI.LowSpaceSubsetSum.StreamJoin.stoppedAcc_mapUser line 153
  13. theorem OAI.LowSpaceSubsetSum.StreamJoin.run_mapUser line 172