OAI/Computability/RationalHitting/SignedArithmetic.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.intCode line 8
  2. instance OAI.RationalHitting.StackLanguage.(instance at line 9) line 9
  3. lemma OAI.RationalHitting.StackLanguage.intCode_length line 10
  4. lemma OAI.RationalHitting.StackLanguage.nat_bits_mono line 13
  5. lemma OAI.RationalHitting.StackLanguage.difference_bits_length line 16
  6. def OAI.RationalHitting.StackLanguage.differenceAbs line 22
  7. def OAI.RationalHitting.StackLanguage.differenceSign line 23
  8. lemma OAI.RationalHitting.StackLanguage.eval_difference_base line 25
  9. lemma OAI.RationalHitting.StackLanguage.eval_differenceAbs line 37
  10. lemma OAI.RationalHitting.StackLanguage.eval_differenceSign line 48
  11. def OAI.RationalHitting.StackLanguage.Procedure.differenceAbs line 59
  12. def OAI.RationalHitting.StackLanguage.Procedure.differenceSign line 65
  13. theorem OAI.RationalHitting.StackLanguage.Poly.natDifferenceAbs line 73
  14. theorem OAI.RationalHitting.StackLanguage.Poly.natLt line 75
  15. theorem OAI.RationalHitting.StackLanguage.Poly.natDifference line 77
  16. theorem OAI.RationalHitting.StackLanguage.Poly.intSign line 86
  17. theorem OAI.RationalHitting.StackLanguage.Poly.intAbs line 89
  18. def OAI.RationalHitting.StackLanguage.positivePart line 99
  19. def OAI.RationalHitting.StackLanguage.negativePart line 100
  20. lemma OAI.RationalHitting.StackLanguage.int_decompose line 102
  21. theorem OAI.RationalHitting.StackLanguage.Poly.positivePart_poly line 109
  22. theorem OAI.RationalHitting.StackLanguage.Poly.negativePart_poly line 112
  23. theorem OAI.RationalHitting.StackLanguage.Poly.natCastInt line 116
  24. theorem OAI.RationalHitting.StackLanguage.Poly.intNeg line 119
  25. theorem OAI.RationalHitting.StackLanguage.Poly.intAdd line 122
  26. theorem OAI.RationalHitting.StackLanguage.Poly.intMul line 126
  27. theorem OAI.RationalHitting.StackLanguage.Poly.natZero line 136
  28. theorem OAI.RationalHitting.StackLanguage.Poly.intZero line 152
  29. theorem OAI.RationalHitting.StackLanguage.Poly.boolNot line 156
  30. theorem OAI.RationalHitting.StackLanguage.Poly.boolAnd line 159
  31. lemma OAI.RationalHitting.StackLanguage.unary_code_length line 170
  32. lemma OAI.RationalHitting.StackLanguage.nat_code_length line 173
  33. lemma OAI.RationalHitting.StackLanguage.prod_code_length line 174
  34. lemma OAI.RationalHitting.StackLanguage.succ_iterate line 177
  35. lemma OAI.RationalHitting.StackLanguage.bits_length_le line 182
  36. def OAI.RationalHitting.StackLanguage.Procedure.unaryPred line 188
  37. theorem OAI.RationalHitting.StackLanguage.Poly.unaryToNat line 208
  38. theorem OAI.RationalHitting.StackLanguage.Poly.unaryPred line 221
  39. theorem OAI.RationalHitting.StackLanguage.Poly.unaryZero line 225
  40. theorem OAI.RationalHitting.StackLanguage.Poly.unaryLt line 228
  41. theorem OAI.RationalHitting.StackLanguage.Poly.unaryLe line 231
  42. theorem OAI.RationalHitting.StackLanguage.Poly.unaryEq line 239
  43. lemma OAI.RationalHitting.StackLanguage.Poly.unaryPred_iterate line 244
  44. theorem OAI.RationalHitting.StackLanguage.Poly.unarySub line 250
  45. lemma OAI.RationalHitting.StackLanguage.int_add_bits_le line 266
  46. lemma OAI.RationalHitting.StackLanguage.int_mul_bits_le line 269
  47. lemma OAI.RationalHitting.StackLanguage.int_code_length line 272
  48. lemma OAI.RationalHitting.StackLanguage.powerStep_iterate line 274
  49. lemma OAI.RationalHitting.StackLanguage.int_pow_bits_le line 280
  50. theorem OAI.RationalHitting.StackLanguage.Poly.intPow line 290
  51. def OAI.RationalHitting.StackLanguage.sumStep line 313
  52. lemma OAI.RationalHitting.StackLanguage.sumStep_code_le line 315
  53. lemma OAI.RationalHitting.StackLanguage.sumStep_code_iterate_le line 327
  54. lemma OAI.RationalHitting.StackLanguage.sumStep_iterate_length line 333
  55. theorem OAI.RationalHitting.StackLanguage.Poly.listSum line 343