OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedWeights.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Indexed membership, signed sums and fixed-width key generation

The runtime mask is an indexed list; its finite set is only a proof view. The operation tally counts index comparisons, addition, testBit and list construction. Numerical values occupy the word widths proved separately. Every finite indexed mask is permitted, including repeated input values.

  1. def OAI.LowSpaceSubsetSum.CountedWeights.member line 17
  2. theorem OAI.LowSpaceSubsetSum.CountedWeights.member_value line 24
  3. theorem OAI.LowSpaceSubsetSum.CountedWeights.member_work line 30
  4. def OAI.LowSpaceSubsetSum.CountedWeights.sumIndices line 36
  5. theorem OAI.LowSpaceSubsetSum.CountedWeights.sumIndices_value line 43
  6. theorem OAI.LowSpaceSubsetSum.CountedWeights.sumIndices_work line 50
  7. def OAI.LowSpaceSubsetSum.CountedWeights.weight line 59
  8. theorem OAI.LowSpaceSubsetSum.CountedWeights.weight_value line 62
  9. theorem OAI.LowSpaceSubsetSum.CountedWeights.weight_work line 67
  10. def OAI.LowSpaceSubsetSum.CountedWeights.maskIndices line 73
  11. theorem OAI.LowSpaceSubsetSum.CountedWeights.maskIndices_value line 80
  12. theorem OAI.LowSpaceSubsetSum.CountedWeights.maskIndices_work line 86
  13. def OAI.LowSpaceSubsetSum.CountedWeights.maskBits line 95
  14. theorem OAI.LowSpaceSubsetSum.CountedWeights.maskBits_value line 97
  15. theorem OAI.LowSpaceSubsetSum.CountedWeights.maskBits_work line 102
  16. def OAI.LowSpaceSubsetSum.CountedWeights.bits line 109

    Source documentation

    Each output bit uses one testBit operation and one list record.

    def bits (value : ℕ) : ℕ → ℕ → List Bool × ℕ
  | 0, _ => ([], 1)
  | k + 1, start =>
    let rest := bits value k (start + 1)
…
  17. theorem OAI.LowSpaceSubsetSum.CountedWeights.bits_value line 115
  18. theorem OAI.LowSpaceSubsetSum.CountedWeights.bits_work line 127
  19. def OAI.LowSpaceSubsetSum.CountedWeights.natBits line 132
  20. theorem OAI.LowSpaceSubsetSum.CountedWeights.natBits_value line 134
  21. def OAI.LowSpaceSubsetSum.CountedWeights.entryKey line 138
  22. theorem OAI.LowSpaceSubsetSum.CountedWeights.entryKey_value line 143
  23. theorem OAI.LowSpaceSubsetSum.CountedWeights.entryKey_work line 148