OAI/Combinatorics/KMedianRecovery/Recovery/Computes.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.bits_eq_nil line 15
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.le_computes line 24
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.lessEqual line 30
  4. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.choose line 41
  5. abbrev OAI.MetricKMedianRecovery.BitMachine.WordSelection.program line 44
  6. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.cfg line 84
  7. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.done line 85
  8. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.start_true line 87
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.start_false line 89
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.start_nil line 91
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.parse_nil line 93
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.parse_one line 95
  13. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.parse_false line 97
  14. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.parse_true line 99
  15. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.discard_nil line 102
  16. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.discard_one line 104
  17. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.discard_false line 106
  18. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.discard_true line 108
  19. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.clear_nil line 111
  20. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.clear_cons line 113
  21. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.restore_nil line 115
  22. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.restore_cons line 117
  23. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.parse_phase line 120
  24. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.restore_phase line 140
  25. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.discard_phase line 149
  26. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.clear_phase line 168
  27. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.true_phase line 175
  28. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.outputs line 185
  29. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.initial line 202
  30. lemma OAI.MetricKMedianRecovery.BitMachine.WordSelection.final line 206
  31. def OAI.MetricKMedianRecovery.BitMachine.WordSelection.choose_computes line 211
  32. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.cond line 220
  33. def OAI.MetricKMedianRecovery.BitMachine.id_computes line 227