OAI/Combinatorics/KMedianRecovery/Machines/ActionMachine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.entry line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.entry_computes line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.block line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.block_computes line 18
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryActions.block_replicate line 22
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.menus line 30
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.menus_computes line 32
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryActions.menus_weights line 37
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.delete line 40
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.delete_computes line 41
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.add line 42
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.add_computes line 43
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.run line 44
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryActions.run_computes line 46
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryActions.clients_sort line 51
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryActions.clients_bits line 54
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryActions.run_pair line 56