OAI/Combinatorics/KMedian/Binary/BinaryAutomatic.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. class OAI.MetricKMedian.Binary.Automatic.Coding line 17
  2. abbrev OAI.MetricKMedian.Binary.Automatic.enc line 19
  3. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 20) line 20
  4. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 21) line 21
  5. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 22) line 22
  6. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 23) line 23
  7. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 24) line 24
  8. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 25) line 25
  9. instance OAI.MetricKMedian.Binary.Automatic.(instance at line 26) line 26
  10. def OAI.MetricKMedian.Binary.Automatic.Poly line 28
  11. def OAI.MetricKMedian.Binary.Automatic.Poly.program line 33
  12. theorem OAI.MetricKMedian.Binary.Automatic.Poly.of_program line 35
  13. theorem OAI.MetricKMedian.Binary.Automatic.Poly.identity line 37
  14. theorem OAI.MetricKMedian.Binary.Automatic.Poly.const line 38
  15. theorem OAI.MetricKMedian.Binary.Automatic.Poly.comp line 39
  16. theorem OAI.MetricKMedian.Binary.Automatic.Poly.pair line 41
  17. theorem OAI.MetricKMedian.Binary.Automatic.Poly.fst line 43
  18. theorem OAI.MetricKMedian.Binary.Automatic.Poly.snd line 44
  19. theorem OAI.MetricKMedian.Binary.Automatic.Poly.ite line 45
  20. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_map line 48
  21. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_add line 53
  22. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_sub line 54
  23. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_mul line 55
  24. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_div line 56
  25. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_lt line 57
  26. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_le line 58
  27. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_eq line 59
  28. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_min line 60
  29. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_max line 61
  30. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_add line 62
  31. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_sub line 63
  32. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_mul line 64
  33. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_lt line 65
  34. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_le line 66
  35. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_eq line 67
  36. theorem OAI.MetricKMedian.Binary.Automatic.Poly.bool_and line 68
  37. theorem OAI.MetricKMedian.Binary.Automatic.Poly.bool_or line 69
  38. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_neg line 70
  39. theorem OAI.MetricKMedian.Binary.Automatic.Poly.bool_not line 71
  40. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_ofNat line 72
  41. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_ofInt line 73
  42. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_length line 75
  43. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_indices line 76
  44. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_getD line 77
  45. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_head line 78
  46. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_tail line 79
  47. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_empty line 80
  48. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_append line 81
  49. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_cons line 82
  50. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_zip line 83
  51. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_filter line 84
  52. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_findIdx line 88
  53. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_getD_comp line 95
  54. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_head_comp line 98
  55. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_lt_comp line 101
  56. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_le_comp line 102
  57. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_eq_comp line 103
  58. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_lt_comp line 104
  59. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_le_comp line 105
  60. theorem OAI.MetricKMedian.Binary.Automatic.Poly.nat_eq_comp line 106
  61. theorem OAI.MetricKMedian.Binary.Automatic.Poly.ite_prop line 107
  62. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_flatMap line 112