OAI/Combinatorics/KMedian/Binary/BinaryWords.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.Word.value line 14
  2. theorem OAI.MetricKMedian.Binary.Word.value_nil line 18
  3. theorem OAI.MetricKMedian.Binary.Word.value_cons line 19
  4. theorem OAI.MetricKMedian.Binary.Word.value_bits line 21
  5. theorem OAI.MetricKMedian.Binary.Word.value_zero line 26
  6. theorem OAI.MetricKMedian.Binary.Word.bits_value line 31
  7. theorem OAI.MetricKMedian.Binary.Word.value_append line 54
  8. theorem OAI.MetricKMedian.Binary.Word.value_reverse_drop line 59
  9. theorem OAI.MetricKMedian.Binary.Word.drop_head line 69
  10. def OAI.MetricKMedian.Binary.Word.normalize line 74
  11. theorem OAI.MetricKMedian.Binary.Word.normalize_eq_bits line 76
  12. def OAI.MetricKMedian.Binary.WordTransducer.dropFalse line 87
  13. theorem OAI.MetricKMedian.Binary.WordTransducer.dropFalse_true line 93
  14. theorem OAI.MetricKMedian.Binary.WordTransducer.dropFalse_run line 98
  15. def OAI.MetricKMedian.Binary.PolyProgram.append line 109
  16. def OAI.MetricKMedian.Binary.PolyProgram.dropFalse line 113
  17. def OAI.MetricKMedian.Binary.PolyProgram.normalize line 117
  18. def OAI.MetricKMedian.Binary.PolyProgram.toBits line 120