OAI/Combinatorics/KMedianRecovery/Recovery/Basic2.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.NatOps.eq line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.kindWord line 26
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.field line 35
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.field_computes line 36
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.query line 38
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.query_computes line 39
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.active line 40
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.active_computes line 41
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.distanceWords line 43
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.distanceWords_computes line 45
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.distance line 53
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.distance_computes line 54
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.tag line 56
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.tag_eq_computes line 57
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.chooseTag line 64
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.chooseActive line 70
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.near line 76
  18. instance OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.nearDecidable line 78
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.near_computes line 80
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.constant line 90
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.constant_computes line 100
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningConstant.constant_source line 117