OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionWeights.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Executing raw and compact subset-weight generation

Indices are supplied in canonical input order. The raw generator constructs the same sublists as the source program; every weight is evaluated by the measured integer routine. Mapping uses an accumulator and one final reversal.

  1. def OAI.LowSpaceSubsetSum.CompressionWeights.weightsAcc line 19
  2. theorem OAI.LowSpaceSubsetSum.CompressionWeights.weightsAcc_value line 25
  3. theorem OAI.LowSpaceSubsetSum.CompressionWeights.weightsAcc_work line 34
  4. def OAI.LowSpaceSubsetSum.CompressionWeights.raw line 47
  5. theorem OAI.LowSpaceSubsetSum.CompressionWeights.raw_value line 52
  6. theorem OAI.LowSpaceSubsetSum.CompressionWeights.raw_source line 56
  7. theorem OAI.LowSpaceSubsetSum.CompressionWeights.raw_length line 59
  8. theorem OAI.LowSpaceSubsetSum.CompressionWeights.raw_work line 63
  9. theorem OAI.LowSpaceSubsetSum.CompressionWeights.raw_scale line 77
  10. def OAI.LowSpaceSubsetSum.CompressionWeights.compact line 95
  11. theorem OAI.LowSpaceSubsetSum.CompressionWeights.compact_source line 101
  12. theorem OAI.LowSpaceSubsetSum.CompressionWeights.compact_scale line 107