OAI/Combinatorics/LowSpaceSubsetSum/Compression/BudgetedCompressionPass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

One compression residue pass on retained reader contexts

The left bounded dictionary remains live during the right join. Overflow skips that join. The shared budget is decreased by the executed joins; no reference run is evaluated to choose the watchdog.

  1. structure OAI.LowSpaceSubsetSum.BudgetedCompressionPass.Data line 20
  2. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.leftFull line 30
  3. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.rightFull line 35
  4. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.reference line 40
  5. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.left line 44
  6. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.right line 49
  7. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.run line 54
  8. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionPass.value line 61
  9. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionPass.account line 90
  10. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.leftBill line 117
  11. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.rightBill line 121
  12. def OAI.LowSpaceSubsetSum.BudgetedCompressionPass.allowance line 125
  13. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionPass.complete line 129
  14. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionPass.remaining line 165