OAI/Computability/MinUncut/Search/RawRationalArithmetic.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Preprocess.RawRat line 7
  2. def OAI.MinUncut.Preprocess.RawRat.value line 10
  3. def OAI.MinUncut.Preprocess.RawRat.ofNat line 11
  4. def OAI.MinUncut.Preprocess.RawRat.neg line 12
  5. def OAI.MinUncut.Preprocess.RawRat.add line 13
  6. def OAI.MinUncut.Preprocess.RawRat.mul line 16
  7. def OAI.MinUncut.Preprocess.RawRat.inv line 18
  8. def OAI.MinUncut.Preprocess.RawRat.le line 21
  9. def OAI.MinUncut.Preprocess.RawRat.lt line 23
  10. instance OAI.MinUncut.Preprocess.RawRat.(instance at line 25) line 25
  11. instance OAI.MinUncut.Preprocess.RawRat.(instance at line 26) line 26
  12. lemma OAI.MinUncut.Preprocess.RawRat.value_nat line 28
  13. lemma OAI.MinUncut.Preprocess.RawRat.value_neg line 29
  14. lemma OAI.MinUncut.Preprocess.RawRat.product_denominator line 30
  15. lemma OAI.MinUncut.Preprocess.RawRat.value_add line 35
  16. lemma OAI.MinUncut.Preprocess.RawRat.value_mul line 42
  17. lemma OAI.MinUncut.Preprocess.RawRat.value_inv line 48
  18. lemma OAI.MinUncut.Preprocess.RawRat.le_iff line 68
  19. lemma OAI.MinUncut.Preprocess.RawRat.lt_iff line 76
  20. lemma OAI.MinUncut.Preprocess.primrec_pow line 87
  21. lemma OAI.MinUncut.Preprocess.primrec_factorial line 96
  22. lemma OAI.MinUncut.Preprocess.choose_factorial line 105
  23. lemma OAI.MinUncut.Preprocess.primrec_choose line 112
  24. lemma OAI.MinUncut.Preprocess.RawRat.primrec_ofNat line 123
  25. lemma OAI.MinUncut.Preprocess.RawRat.primrec_neg line 124
  26. lemma OAI.MinUncut.Preprocess.RawRat.primrec_add line 127
  27. lemma OAI.MinUncut.Preprocess.RawRat.primrec_mul line 138
  28. lemma OAI.MinUncut.Preprocess.RawRat.primrec_inv line 149
  29. lemma OAI.MinUncut.Preprocess.RawRat.primrec_le line 158
  30. lemma OAI.MinUncut.Preprocess.RawRat.primrec_lt line 170
  31. def OAI.MinUncut.Preprocess.RawRat.pow line 181
  32. lemma OAI.MinUncut.Preprocess.RawRat.value_pow line 184
  33. lemma OAI.MinUncut.Preprocess.RawRat.primrec_pow line 188
  34. def OAI.MinUncut.Preprocess.RawRat.ceil line 197
  35. lemma OAI.MinUncut.Preprocess.RawRat.primrec_ceil line 198
  36. lemma OAI.MinUncut.Preprocess.RawRat.ceil_eq line 207
  37. def OAI.MinUncut.Preprocess.RawRat.represent line 239
  38. lemma OAI.MinUncut.Preprocess.RawRat.value_represent line 240
  39. lemma OAI.MinUncut.Preprocess.primrec_gcd line 253
  40. lemma OAI.MinUncut.Preprocess.primrec_intCode line 274
  41. lemma OAI.MinUncut.Preprocess.intCode_nat line 276
  42. lemma OAI.MinUncut.Preprocess.intCode_negSucc line 278
  43. lemma OAI.MinUncut.Preprocess.primrec_intAbs line 281
  44. lemma OAI.MinUncut.Preprocess.primrec_intToNat line 288
  45. lemma OAI.MinUncut.Preprocess.primrec_intNegToNat line 297
  46. abbrev OAI.MinUncut.Preprocess.RationalPair line 307
  47. lemma OAI.MinUncut.Preprocess.rationalPair_prim line 308
  48. instance OAI.MinUncut.Preprocess.rationalPairPrimcodable line 313
  49. def OAI.MinUncut.Preprocess.rationalEquiv line 315
  50. instance OAI.MinUncut.Preprocess.rationalPrimcodable line 321
  51. lemma OAI.MinUncut.Preprocess.primrec_ratNum line 323
  52. lemma OAI.MinUncut.Preprocess.primrec_ratDen line 325
  53. lemma OAI.MinUncut.Preprocess.primrec_represent line 327
  54. def OAI.MinUncut.Preprocess.candidate line 335
  55. lemma OAI.MinUncut.Preprocess.candidate_eq line 338
  56. lemma OAI.MinUncut.Preprocess.candidate_exists line 350
  57. lemma OAI.MinUncut.Preprocess.candidate_primrec line 359
  58. lemma OAI.MinUncut.Preprocess.computable_value line 371
  59. lemma OAI.MinUncut.Preprocess.computable_ratAdd line 382
  60. lemma OAI.MinUncut.Preprocess.computable_ratMul line 387
  61. lemma OAI.MinUncut.Preprocess.computable_ratNeg line 392
  62. lemma OAI.MinUncut.Preprocess.computable_ratInv line 395
  63. lemma OAI.MinUncut.Preprocess.computable_ratSub line 398
  64. lemma OAI.MinUncut.Preprocess.computable_ratDiv line 401
  65. lemma OAI.MinUncut.Preprocess.computable_ratPow line 404
  66. lemma OAI.MinUncut.Preprocess.computable_ratNat line 408
  67. lemma OAI.MinUncut.Preprocess.primrec_ratLe line 410
  68. lemma OAI.MinUncut.Preprocess.primrec_ratLt line 413
  69. lemma OAI.MinUncut.Preprocess.primrec_ratCeil line 416
  70. lemma OAI.MinUncut.Preprocess.ca_id line 427
  71. lemma OAI.MinUncut.Preprocess.ca_const line 428
  72. lemma OAI.MinUncut.Preprocess.ca_fst line 429
  73. lemma OAI.MinUncut.Preprocess.ca_snd line 430
  74. lemma OAI.MinUncut.Preprocess.ca_comp line 431
  75. lemma OAI.MinUncut.Preprocess.ca_pair line 433
  76. lemma OAI.MinUncut.Preprocess.ca_add line 435
  77. lemma OAI.MinUncut.Preprocess.ca_sub line 437
  78. lemma OAI.MinUncut.Preprocess.ca_mul line 439
  79. lemma OAI.MinUncut.Preprocess.ca_pow line 441
  80. lemma OAI.MinUncut.Preprocess.ca_div line 443
  81. lemma OAI.MinUncut.Preprocess.ca_mod line 445
  82. lemma OAI.MinUncut.Preprocess.ca_choose line 447
  83. lemma OAI.MinUncut.Preprocess.ca_factorial line 449
  84. lemma OAI.MinUncut.Preprocess.ca_ratCast line 451
  85. lemma OAI.MinUncut.Preprocess.ca_ratAdd line 453
  86. lemma OAI.MinUncut.Preprocess.ca_ratSub line 454
  87. lemma OAI.MinUncut.Preprocess.ca_ratMul line 455
  88. lemma OAI.MinUncut.Preprocess.ca_ratDiv line 456
  89. lemma OAI.MinUncut.Preprocess.ca_ratInv line 457
  90. lemma OAI.MinUncut.Preprocess.ca_ratPow line 458
  91. lemma OAI.MinUncut.Preprocess.ca_ratCeil line 459
  92. lemma OAI.MinUncut.Preprocess.ca_and line 461
  93. lemma OAI.MinUncut.Preprocess.ca_natLe line 467
  94. lemma OAI.MinUncut.Preprocess.ca_natLt line 470
  95. lemma OAI.MinUncut.Preprocess.ca_ratLe line 473
  96. lemma OAI.MinUncut.Preprocess.ca_ratLt line 476
  97. example OAI.MinUncut.Preprocess.(example at line 480) line 480
  98. example OAI.MinUncut.Preprocess.(example at line 481) line 481
  99. lemma OAI.MinUncut.Preprocess.c_rangeMap line 488
  100. lemma OAI.MinUncut.Preprocess.ca_range line 501
  101. lemma OAI.MinUncut.Preprocess.ca_sum line 503
  102. lemma OAI.MinUncut.Preprocess.c_boundedSum line 508