OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredNodeCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The concrete stored-mask filter realizes the traversal cell bound

  1. def OAI.LowSpaceSubsetSum.StoredNodeCells.prepare line 14
  2. theorem OAI.LowSpaceSubsetSum.StoredNodeCells.prepare_value line 20
  3. theorem OAI.LowSpaceSubsetSum.StoredNodeCells.prepare_cells line 33
  4. def OAI.LowSpaceSubsetSum.StoredNodeCells.run line 41

    Source documentation

    The full filter is reached only after its work charge is reserved.

    def run (b : Block n g) (lo hi : ℕ) (xs ys : List (StoredEntry n))
    (nx ny budget : ℕ) : BudgetedSeparatorCall.Outcome (BudgetedSeparatorNode.Frame
      (StoredEntry n) (StoredEntry n)) × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.BudgetedSeparatorCall.Outcome, OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.Frame

  5. theorem OAI.LowSpaceSubsetSum.StoredNodeCells.run_value line 50
  6. theorem OAI.LowSpaceSubsetSum.StoredNodeCells.run_cells line 57