OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredArrayCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Prefix filtering while retaining bounded stored records

Membership tests scan the existing index lists. The filter uses the actual tail accumulator; its input, output, and final array share record payloads. The cell annotation also bounds a copying implementation of those payloads.

  1. def OAI.LowSpaceSubsetSum.StoredArrayCells.compatibleAcc line 19
  2. theorem OAI.LowSpaceSubsetSum.StoredArrayCells.compatibleAcc_value line 32
  3. theorem OAI.LowSpaceSubsetSum.StoredArrayCells.compatibleAcc_cells line 40
  4. def OAI.LowSpaceSubsetSum.StoredArrayCells.compatible line 56
  5. theorem OAI.LowSpaceSubsetSum.StoredArrayCells.compatible_value line 60
  6. theorem OAI.LowSpaceSubsetSum.StoredArrayCells.compatible_cells line 64
  7. def OAI.LowSpaceSubsetSum.StoredArrayCells.array line 71
  8. theorem OAI.LowSpaceSubsetSum.StoredArrayCells.array_value line 78
  9. theorem OAI.LowSpaceSubsetSum.StoredArrayCells.array_cells line 84