OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedDedup.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Linear duplicate removal after sorting compressed weights

The output is exactly the compact list used by the decision core. The implementation removes adjacent repeats and never searches the tail for a duplicate. Its counter charges one equality test and constant list work per input occurrence.

  1. def OAI.LowSpaceSubsetSum.CountedDedup.tail line 19
  2. def OAI.LowSpaceSubsetSum.CountedDedup.run line 29
  3. theorem OAI.LowSpaceSubsetSum.CountedDedup.tail_value line 33
  4. theorem OAI.LowSpaceSubsetSum.CountedDedup.tail_work line 40
  5. theorem OAI.LowSpaceSubsetSum.CountedDedup.run_value line 46
  6. theorem OAI.LowSpaceSubsetSum.CountedDedup.run_sorted_value line 51
  7. theorem OAI.LowSpaceSubsetSum.CountedDedup.run_work line 55
  8. def OAI.LowSpaceSubsetSum.CompactWeightWork.run line 66
  9. theorem OAI.LowSpaceSubsetSum.CompactWeightWork.run_value line 71
  10. theorem OAI.LowSpaceSubsetSum.CompactWeightWork.run_work line 81