OAI/Combinatorics/LowSpaceSubsetSum/Storage/DistinctCountCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Live storage of the tail distinct-key counter

Each iteration drops the previous reader state after obtaining its successor. The trace retains the previous scalar key, count, remaining fuel and work counter, but no list of emitted values.

  1. def OAI.LowSpaceSubsetSum.DistinctCountCells.loop line 16
  2. theorem OAI.LowSpaceSubsetSum.DistinctCountCells.loop_value line 31
  3. theorem OAI.LowSpaceSubsetSum.DistinctCountCells.loop_cells line 47
  4. def OAI.LowSpaceSubsetSum.DistinctCountCells.run line 74
  5. theorem OAI.LowSpaceSubsetSum.DistinctCountCells.run_value line 79
  6. theorem OAI.LowSpaceSubsetSum.DistinctCountCells.run_cells line 86