OAI/Computability/MinUncut/Search/ArithmeticTactic.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Preprocess.c_epsilon line 49
  2. lemma OAI.MinUncut.Preprocess.c_atomConstant line 54
  3. lemma OAI.MinUncut.Preprocess.inner_check_0 line 64
  4. lemma OAI.MinUncut.Preprocess.inner_check_1 line 67
  5. lemma OAI.MinUncut.Preprocess.inner_check_2 line 70
  6. lemma OAI.MinUncut.Preprocess.inner_check_3 line 73
  7. lemma OAI.MinUncut.Preprocess.inner_check_4 line 76
  8. lemma OAI.MinUncut.Preprocess.inner_check_5 line 79
  9. lemma OAI.MinUncut.Preprocess.inner_check_6 line 82
  10. lemma OAI.MinUncut.Preprocess.inner_check_7 line 85
  11. lemma OAI.MinUncut.Preprocess.inner_check_8 line 88
  12. lemma OAI.MinUncut.Preprocess.inner_check_9 line 91
  13. lemma OAI.MinUncut.Preprocess.inner_check_10 line 94
  14. lemma OAI.MinUncut.Preprocess.inner_check_11 line 97
  15. lemma OAI.MinUncut.Preprocess.inner_check_12 line 100
  16. lemma OAI.MinUncut.Preprocess.inner_check_13 line 103
  17. lemma OAI.MinUncut.Preprocess.inner_check_14 line 106
  18. lemma OAI.MinUncut.Preprocess.inner_check_15 line 109
  19. lemma OAI.MinUncut.Preprocess.inner_check_16 line 112
  20. lemma OAI.MinUncut.Preprocess.inner_check_17 line 115
  21. lemma OAI.MinUncut.Preprocess.inner_check_18 line 118
  22. lemma OAI.MinUncut.Preprocess.inner_check_computable line 122
  23. lemma OAI.MinUncut.Preprocess.c_amplitude line 125
  24. lemma OAI.MinUncut.Preprocess.c_hints line 127
  25. lemma OAI.MinUncut.Preprocess.c_rate line 138
  26. lemma OAI.MinUncut.Preprocess.c_listBound line 139
  27. lemma OAI.MinUncut.Preprocess.c_radicand line 141
  28. lemma OAI.MinUncut.Preprocess.c_oTheta line 144
  29. lemma OAI.MinUncut.Preprocess.c_oP line 146
  30. lemma OAI.MinUncut.Preprocess.c_oB4 line 148
  31. lemma OAI.MinUncut.Preprocess.outer_check_0 line 150
  32. lemma OAI.MinUncut.Preprocess.outer_check_1 line 151
  33. lemma OAI.MinUncut.Preprocess.outer_check_2 line 152
  34. lemma OAI.MinUncut.Preprocess.outer_check_3 line 153
  35. lemma OAI.MinUncut.Preprocess.outer_check_4 line 154
  36. lemma OAI.MinUncut.Preprocess.outer_check_5 line 155
  37. lemma OAI.MinUncut.Preprocess.outer_check_6 line 156
  38. lemma OAI.MinUncut.Preprocess.outer_check_7 line 157
  39. lemma OAI.MinUncut.Preprocess.outer_check_8 line 158
  40. lemma OAI.MinUncut.Preprocess.outer_check_computable line 159
  41. lemma OAI.MinUncut.Preprocess.c_qError line 161
  42. lemma OAI.MinUncut.Preprocess.c_gT line 163
  43. lemma OAI.MinUncut.Preprocess.c_gL line 165
  44. lemma OAI.MinUncut.Preprocess.c_gr line 167
  45. lemma OAI.MinUncut.Preprocess.c_gE line 169
  46. lemma OAI.MinUncut.Preprocess.grid_check_0 line 171
  47. lemma OAI.MinUncut.Preprocess.grid_check_1 line 172
  48. lemma OAI.MinUncut.Preprocess.grid_check_2 line 173
  49. lemma OAI.MinUncut.Preprocess.grid_check_3 line 176
  50. lemma OAI.MinUncut.Preprocess.c_gErrorArg line 181
  51. lemma OAI.MinUncut.Preprocess.c_gError line 183
  52. lemma OAI.MinUncut.Preprocess.c_gCoef line 185
  53. lemma OAI.MinUncut.Preprocess.grid_check_4 line 187
  54. lemma OAI.MinUncut.Preprocess.grid_check_computable line 189
  55. def OAI.MinUncut.Preprocess.gridTail line 198
  56. def OAI.MinUncut.Preprocess.gridField line 199
  57. def OAI.MinUncut.Preprocess.gridExtract line 200
  58. lemma OAI.MinUncut.Preprocess.gridExtract_encode line 203
  59. lemma OAI.MinUncut.Preprocess.gridDecode_eq line 205
  60. lemma OAI.MinUncut.Preprocess.c_gridTail line 221
  61. lemma OAI.MinUncut.Preprocess.c_gridField line 222
  62. lemma OAI.MinUncut.Preprocess.c_gridMk line 225
  63. lemma OAI.MinUncut.Preprocess.gridExtract_eq line 227
  64. lemma OAI.MinUncut.Preprocess.c_gridExtract₁ line 232
  65. lemma OAI.MinUncut.Preprocess.c_gridExtract₂ line 234
  66. lemma OAI.MinUncut.Preprocess.c_gridExtract₃ line 236
  67. lemma OAI.MinUncut.Preprocess.c_gridExtractPair line 238
  68. lemma OAI.MinUncut.Preprocess.c_gridExtract line 241
  69. lemma OAI.MinUncut.Preprocess.c_oldGridEncode line 244
  70. lemma OAI.MinUncut.Preprocess.c_oldGridDecode line 252
  71. def OAI.MinUncut.Preprocess.parameterJ line 264
  72. lemma OAI.MinUncut.Preprocess.parameterJ_pos line 265
  73. lemma OAI.MinUncut.Preprocess.parameterJ_eq line 266
  74. lemma OAI.MinUncut.Preprocess.c_parameterJ line 269
  75. lemma OAI.MinUncut.Preprocess.inner_exists line 272
  76. def OAI.MinUncut.Preprocess.selectedInner line 274
  77. lemma OAI.MinUncut.Preprocess.selectedInner_check line 275
  78. lemma OAI.MinUncut.Preprocess.c_inner_pred line 277
  79. lemma OAI.MinUncut.Preprocess.c_selectedInner line 279
  80. lemma OAI.MinUncut.Preprocess.outer_exists line 284
  81. def OAI.MinUncut.Preprocess.selectedOuter line 286
  82. lemma OAI.MinUncut.Preprocess.selectedOuter_check line 287
  83. lemma OAI.MinUncut.Preprocess.c_outer_arguments line 289
  84. lemma OAI.MinUncut.Preprocess.c_outer_decide line 293
  85. lemma OAI.MinUncut.Preprocess.c_outer_pred line 299
  86. lemma OAI.MinUncut.Preprocess.c_selectedOuter line 301
  87. def OAI.MinUncut.Preprocess.selectedParameters line 303
  88. def OAI.MinUncut.Preprocess.gridPredicate line 306
  89. instance OAI.MinUncut.Preprocess.(instance at line 308) line 308
  90. lemma OAI.MinUncut.Preprocess.grid_exists line 309
  91. def OAI.MinUncut.Preprocess.selectedGrid line 314
  92. lemma OAI.MinUncut.Preprocess.selectedGrid_eq line 316
  93. lemma OAI.MinUncut.Preprocess.c_grid_valid line 322
  94. lemma OAI.MinUncut.Preprocess.c_grid_pred line 325
  95. lemma OAI.MinUncut.Preprocess.c_selectedGrid line 338