OAI/Combinatorics/LowSpaceSubsetSum/Storage/PreparedCollectCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Live storage of the full guarded parent collection

The first prepared context remains live while the second is built. Both shared right arrays then remain live throughout the stopped join. The returned safe dictionary replaces the contexts after collection; no list of emitted matches is retained.

  1. def OAI.LowSpaceSubsetSum.PreparedCollectCells.contextCells line 20
  2. theorem OAI.LowSpaceSubsetSum.PreparedCollectCells.contextCells_bound line 24
  3. def OAI.LowSpaceSubsetSum.PreparedCollectCells.resultCells line 39

    Source documentation

    The projected return value has no reader or array fields.

    def resultCells {I : Instance n} {C : ℕ} (out : PreparedParentExecution.Result I C) : ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.PreparedParentExecution.Result

  4. theorem OAI.LowSpaceSubsetSum.PreparedCollectCells.resultCells_bound line 42
  5. def OAI.LowSpaceSubsetSum.PreparedCollectCells.run line 53
  6. theorem OAI.LowSpaceSubsetSum.PreparedCollectCells.run_value line 67
  7. theorem OAI.LowSpaceSubsetSum.PreparedCollectCells.padded_power line 81
  8. theorem OAI.LowSpaceSubsetSum.PreparedCollectCells.scalar_bound line 88
  9. theorem OAI.LowSpaceSubsetSum.PreparedCollectCells.run_cells line 115