OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredEncodingCells.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Actual key construction and safe insertion scratch

The Boolean key is generated from the bounded index list. The trace includes recursive frames, both partial bit lists and the append allocation. Keys are computed once before the cached trie feed.

  1. def OAI.LowSpaceSubsetSum.StoredEncodingCells.maskIndices line 18
  2. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.maskIndices_value line 25
  3. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.maskIndices_cells line 32
  4. def OAI.LowSpaceSubsetSum.StoredEncodingCells.maskBits line 41
  5. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.maskBits_value line 45
  6. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.maskBits_cells line 49
  7. def OAI.LowSpaceSubsetSum.StoredEncodingCells.bits line 56
  8. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.bits_value line 62
  9. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.bits_cells line 68
  10. def OAI.LowSpaceSubsetSum.StoredEncodingCells.encode line 73
  11. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.encode_value line 80
  12. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.encode_cells line 85
  13. def OAI.LowSpaceSubsetSum.StoredEncodingCells.feed line 93
  14. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.feed_value line 97
  15. theorem OAI.LowSpaceSubsetSum.StoredEncodingCells.feed_cells line 102