OAI/Combinatorics/LowSpaceSubsetSum/Storage/IntervalDomainCells.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Live storage for arithmetic interval domain construction

The scan tests only the two interval endpoints. It filters the bounded index list, looks up the stored permutation, and sorts the resulting indices. The immutable permutation array is shared throughout.

  1. def OAI.LowSpaceSubsetSum.IntervalDomainCells.test line 18
  2. def OAI.LowSpaceSubsetSum.IntervalDomainCells.positions line 21
  3. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.positions_value line 25
  4. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.positions_length line 30
  5. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.positions_length_interval line 36
  6. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.positions_cells line 53
  7. def OAI.LowSpaceSubsetSum.IntervalDomainCells.map line 59
  8. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.map_value line 65
  9. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.map_cells line 71
  10. def OAI.LowSpaceSubsetSum.IntervalDomainCells.compare line 77
  11. def OAI.LowSpaceSubsetSum.IntervalDomainCells.run line 79
  12. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.run_value line 85
  13. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.run_length line 90
  14. theorem OAI.LowSpaceSubsetSum.IntervalDomainCells.run_cells line 97