OAI/Combinatorics/KMedianRecovery/Encoding/StateBits.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.stateBits line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.context line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.oldBudget line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.newFacility line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.newBudget line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.context_computes line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.oldBudget_computes line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.newFacility_computes line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.newBudget_computes line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.ctxField line 22
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.ctxField_computes line 23
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.allFacilities line 24
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.allFacilities_computes line 25
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.allFacilities_context line 26
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.opened line 31
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.opened_computes line 33
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.opened_pack line 36
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.updatedContext line 44
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.updatedContext_computes line 46
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.updatedContext_pack line 51
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.active line 59
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.active_computes line 60
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.active_pack line 62
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.budgetItem line 75
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.budgetItem_computes line 78
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.budgetItem_pack line 83
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.updatedBudget line 92
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.updatedBudget_computes line 94
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.updatedBudget_pack line 99
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.run line 109
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.run_computes line 110
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseUpdate.run_pack line 111