OAI/Combinatorics/LowSpaceSubsetSum/Storage/BudgetedFillCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Live cells in the tail-recursive prepaid tie buffer

The live counter retains the buffer and the two cursors around a fetch. Reader and key calls supply their own scratch traces. The loop drops its old cursor before the tail call, so the bound is independent of the query count.

  1. def OAI.LowSpaceSubsetSum.BudgetedFillCells.loop line 17
  2. theorem OAI.LowSpaceSubsetSum.BudgetedFillCells.loop_value line 42
  3. theorem OAI.LowSpaceSubsetSum.BudgetedFillCells.loop_cells line 67
  4. def OAI.LowSpaceSubsetSum.BudgetedFillCells.run line 112
  5. theorem OAI.LowSpaceSubsetSum.BudgetedFillCells.run_value line 117
  6. theorem OAI.LowSpaceSubsetSum.BudgetedFillCells.run_cells line 126