OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredTerminalCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The terminal check with exact sort-and-match storage accounting

The record payloads stay in the retained dictionary arrays. List spines and sort continuations are accounted explicitly; both sorts execute in order. The matching loop is tail recursive and retains two list cursors.

  1. def OAI.LowSpaceSubsetSum.StoredTerminalCells.lengthAcc line 17
  2. theorem OAI.LowSpaceSubsetSum.StoredTerminalCells.lengthAcc_eq line 21
  3. def OAI.LowSpaceSubsetSum.StoredTerminalCells.run line 27
  4. theorem OAI.LowSpaceSubsetSum.StoredTerminalCells.run_value line 37
  5. theorem OAI.LowSpaceSubsetSum.StoredTerminalCells.run_cells line 45
  6. def OAI.LowSpaceSubsetSum.StoredTerminalCells.budgeted line 62

    Source documentation

    No terminal allocation occurs before its guard succeeds.

    def budgeted (target : ℤ) (xs ys : List (StoredEntry n)) (nx ny budget : ℕ) :
    BudgetedSeparatorCall.Outcome Bool × ℕ :=
…

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

  7. theorem OAI.LowSpaceSubsetSum.StoredTerminalCells.budgeted_value line 70
  8. theorem OAI.LowSpaceSubsetSum.StoredTerminalCells.budgeted_cells line 76