OAI/Combinatorics/LowSpaceSubsetSum/Streams/StreamPrimitiveWork.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Counted binary searches and residue sorting

The counted routines follow the same branches as the executable search and sort. Their first components agree exactly with those routines. The counters charge predicate calls and merge/split operations, respectively; word arithmetic and mask access still require separate compilation charges.

  1. def OAI.LowSpaceSubsetSum.BinaryPivot.counted line 19
  2. theorem OAI.LowSpaceSubsetSum.BinaryPivot.counted_value line 26
  3. theorem OAI.LowSpaceSubsetSum.BinaryPivot.counted_queries line 32
  4. def OAI.LowSpaceSubsetSum.BinaryPivot.countedSearch line 41
  5. theorem OAI.LowSpaceSubsetSum.BinaryPivot.countedSearch_value line 44
  6. theorem OAI.LowSpaceSubsetSum.BinaryPivot.countedSearch_queries line 47
  7. def OAI.LowSpaceSubsetSum.ResidueSort.counted line 56
  8. theorem OAI.LowSpaceSubsetSum.ResidueSort.counted_value line 60
  9. theorem OAI.LowSpaceSubsetSum.ResidueSort.counted_work line 64
  10. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.counted_sort_value line 75
  11. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.counted_sort_work line 79
  12. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.any_state_comparisons line 85