OAI/Computability/RationalHitting/RationalArithmetic.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.chooseClean line 8
  2. lemma OAI.RationalHitting.StackLanguage.eval_chooseClean line 10
  3. def OAI.RationalHitting.StackLanguage.Procedure.choose line 33
  4. theorem OAI.RationalHitting.StackLanguage.Poly.choose line 47
  5. def OAI.RationalHitting.StackLanguage.unpackInt line 60
  6. lemma OAI.RationalHitting.StackLanguage.eval_unpackInt line 62
  7. def OAI.RationalHitting.StackLanguage.rationalClean line 77
  8. abbrev OAI.RationalHitting.StackLanguage.NZInt line 80
  9. lemma OAI.RationalHitting.StackLanguage.eval_rationalClean line 82
  10. def OAI.RationalHitting.StackLanguage.Procedure.rationalEncode line 118
  11. theorem OAI.RationalHitting.StackLanguage.Poly.rationalEncodeNZ line 137
  12. theorem OAI.RationalHitting.StackLanguage.Poly.safeDen line 142
  13. theorem OAI.RationalHitting.StackLanguage.Poly.rationalEncode line 147
  14. theorem OAI.RationalHitting.StackLanguage.Poly.unaryEta line 164
  15. theorem OAI.RationalHitting.StackLanguage.Poly.unaryAddFun line 167
  16. theorem OAI.RationalHitting.StackLanguage.Poly.unarySubFun line 170
  17. theorem OAI.RationalHitting.StackLanguage.Poly.unaryMulFun line 173
  18. theorem OAI.RationalHitting.StackLanguage.Poly.unaryDivFun line 176
  19. theorem OAI.RationalHitting.StackLanguage.Poly.unaryModFun line 179
  20. theorem OAI.RationalHitting.StackLanguage.Poly.unaryPowFun line 182
  21. theorem OAI.RationalHitting.StackLanguage.Poly.unaryCastInt line 185
  22. theorem OAI.RationalHitting.StackLanguage.Poly.unaryCastIntFun line 188
  23. theorem OAI.RationalHitting.StackLanguage.Poly.unaryEqFun line 190
  24. theorem OAI.RationalHitting.StackLanguage.Poly.unaryLtFun line 193
  25. theorem OAI.RationalHitting.StackLanguage.Poly.chooseFun line 196
  26. theorem OAI.RationalHitting.StackLanguage.Poly.intPowFun line 199
  27. theorem OAI.RationalHitting.StackLanguage.Poly.ite line 203
  28. theorem OAI.RationalHitting.StackLanguage.Poly.sumUp line 208
  29. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 216) line 216
  30. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 217) line 217
  31. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 218) line 218
  32. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 219) line 219
  33. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 220) line 220
  34. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 221) line 221
  35. instance OAI.RationalHitting.StackLanguage.Unary.(instance at line 222) line 222
  36. def OAI.RationalHitting.StackLanguage.Unary.toInt line 223
  37. def OAI.RationalHitting.StackLanguage.Unary.choose line 224
  38. def OAI.RationalHitting.StackLanguage.Unary.powInt line 225
  39. def OAI.RationalHitting.StackLanguage.Unary.eqb line 226
  40. def OAI.RationalHitting.StackLanguage.Unary.ltb line 227
  41. theorem OAI.RationalHitting.StackLanguage.Poly.uAdd line 231
  42. theorem OAI.RationalHitting.StackLanguage.Poly.uSub line 232
  43. theorem OAI.RationalHitting.StackLanguage.Poly.uMul line 233
  44. theorem OAI.RationalHitting.StackLanguage.Poly.uDiv line 234
  45. theorem OAI.RationalHitting.StackLanguage.Poly.uMod line 235
  46. theorem OAI.RationalHitting.StackLanguage.Poly.uPow line 236
  47. theorem OAI.RationalHitting.StackLanguage.Poly.uInt line 237
  48. theorem OAI.RationalHitting.StackLanguage.Poly.uChoose line 238
  49. theorem OAI.RationalHitting.StackLanguage.Poly.uPowInt line 240
  50. theorem OAI.RationalHitting.StackLanguage.Poly.uEq line 241
  51. theorem OAI.RationalHitting.StackLanguage.Poly.uLt line 242
  52. example OAI.RationalHitting.StackLanguage.Poly.(example at line 244) line 244
  53. example OAI.RationalHitting.StackLanguage.Poly.(example at line 247) line 247