OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredRestriction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Bounded-list prefix restrictions

Forcing one bit scans the ambient indices and retains the resulting list. This works for every bounded input list, including lists with repetitions; no finite-set insertion is executed by the prefix controller.

  1. def OAI.LowSpaceSubsetSum.IndexedMask.insert line 19
  2. theorem OAI.LowSpaceSubsetSum.IndexedMask.insert_value line 25
  3. theorem OAI.LowSpaceSubsetSum.IndexedMask.insert_work line 30
  4. structure OAI.LowSpaceSubsetSum.StoredRestriction line 41
  5. def OAI.LowSpaceSubsetSum.StoredRestriction.semantic line 49
  6. def OAI.LowSpaceSubsetSum.StoredRestriction.empty line 52
  7. theorem OAI.LowSpaceSubsetSum.StoredRestriction.empty_value line 54
  8. def OAI.LowSpaceSubsetSum.StoredRestriction.force line 56
  9. theorem OAI.LowSpaceSubsetSum.StoredRestriction.force_value line 64
  10. theorem OAI.LowSpaceSubsetSum.StoredRestriction.force_work line 69
  11. def OAI.LowSpaceSubsetSum.StoredRestriction.cells line 76
  12. theorem OAI.LowSpaceSubsetSum.StoredRestriction.cells_le line 79