OAI/Combinatorics/LowSpaceSubsetSum/Streams/StreamJoin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A finite-state join of two sorted streams

Unequal keys consume one occurrence. Equal keys invoke the bounded-buffer Cartesian reporter and continue from its two saved endpoints. The loop keeps only the two generator states, callback state, and counters. Its finite output lists and matching potential are analysis objects only.

  1. structure OAI.LowSpaceSubsetSum.StreamJoin.State line 21
  2. def OAI.LowSpaceSubsetSum.StreamJoin.start line 30
  3. def OAI.LowSpaceSubsetSum.StreamJoin.step line 32
  4. def OAI.LowSpaceSubsetSum.StreamJoin.runAcc line 53
  5. def OAI.LowSpaceSubsetSum.StreamJoin.run line 61
  6. def OAI.LowSpaceSubsetSum.StreamJoin.rank line 67
  7. def OAI.LowSpaceSubsetSum.StreamJoin.potential line 70
  8. def OAI.LowSpaceSubsetSum.StreamJoin.WellFormed line 74
  9. theorem OAI.LowSpaceSubsetSum.StreamJoin.step_done line 81
  10. theorem OAI.LowSpaceSubsetSum.StreamJoin.runAcc_done line 88