OAI/Combinatorics/LowSpaceSubsetSum/Storage/ListSetCells.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite-set metadata built from a stored list

Insertion first scans the current set through its quotient-invariant stored list. The tail loop retains only the current set, input suffix and scalar counters; duplicate occurrences do not enlarge the set.

  1. def OAI.LowSpaceSubsetSum.ListSetCells.insert line 16
  2. theorem OAI.LowSpaceSubsetSum.ListSetCells.insert_value line 20
  3. theorem OAI.LowSpaceSubsetSum.ListSetCells.insert_work line 27
  4. def OAI.LowSpaceSubsetSum.ListSetCells.loop line 32
  5. theorem OAI.LowSpaceSubsetSum.ListSetCells.loop_value line 39
  6. theorem OAI.LowSpaceSubsetSum.ListSetCells.loop_work line 49
  7. theorem OAI.LowSpaceSubsetSum.ListSetCells.loop_cells line 64
  8. def OAI.LowSpaceSubsetSum.ListSetCells.run line 78
  9. theorem OAI.LowSpaceSubsetSum.ListSetCells.value line 80
  10. theorem OAI.LowSpaceSubsetSum.ListSetCells.work line 83
  11. theorem OAI.LowSpaceSubsetSum.ListSetCells.cells line 86
  12. theorem OAI.LowSpaceSubsetSum.ListSetCells.three_work line 89