OAI/Combinatorics/LowSpaceSubsetSum/Storage/ScalarJoinOneCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Live storage in buffered scalar replay

The parameter bounds describe concrete primitive calls. The proof is independent of the replay fuel: only the current cursor and user state, the shared tie buffer, and one cloned cursor remain live.

  1. def OAI.LowSpaceSubsetSum.ScalarJoinOneCells.bufferRead line 18
  2. def OAI.LowSpaceSubsetSum.ScalarJoinOneCells.buffer line 20
  3. theorem OAI.LowSpaceSubsetSum.ScalarJoinOneCells.buffer_value line 26
  4. theorem OAI.LowSpaceSubsetSum.ScalarJoinOneCells.buffer_cells line 35
  5. def OAI.LowSpaceSubsetSum.ScalarJoinOneCells.run line 47
  6. theorem OAI.LowSpaceSubsetSum.ScalarJoinOneCells.run_value line 77
  7. theorem OAI.LowSpaceSubsetSum.ScalarJoinOneCells.run_cells line 106