OAI/Combinatorics/LowSpaceSubsetSum/Compression/BudgetedPreparedCompressionPass.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A prepaid compression pass including all four initializations

  1. def OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.charge line 13
  2. def OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.run line 15
  3. def OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.allowance line 19
  4. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.value line 22
  5. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.account line 32
  6. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.complete line 47
  7. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.remaining line 57
  8. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.source_value line 67
  9. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedCompressionPass.source_account line 78