OAI/Combinatorics/LowSpaceSubsetSum/Storage/ScheduleBucketCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One residue bucket with a retained left dictionary and reused right workspace

  1. def OAI.LowSpaceSubsetSum.ScheduleBucketCells.afterLeft line 15
  2. def OAI.LowSpaceSubsetSum.ScheduleBucketCells.run line 26
  3. theorem OAI.LowSpaceSubsetSum.ScheduleBucketCells.afterLeft_value line 35
  4. theorem OAI.LowSpaceSubsetSum.ScheduleBucketCells.value line 53
  5. theorem OAI.LowSpaceSubsetSum.ScheduleBucketCells.records_size line 71

    Source documentation

    The complete live left dictionary has at most one rejected extra record.

    theorem records_size (I : Instance n) (C : ℕ) (d : StoredEntry.Dictionary I C) :
    d.val.records.size ≤ C + 1 := (RecordedDictionary.storage d.property).1

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.StoredEntry.Dictionary, OAI.LowSpaceSubsetSum.RecordedDictionary.storage

  6. def OAI.LowSpaceSubsetSum.ScheduleBucketCells.reserve line 74
  7. theorem OAI.LowSpaceSubsetSum.ScheduleBucketCells.afterLeft_cells line 80
  8. theorem OAI.LowSpaceSubsetSum.ScheduleBucketCells.cells_explicit line 107
  9. theorem OAI.LowSpaceSubsetSum.ScheduleBucketCells.cells line 139