OAI/Computability/RationalHitting/UnaryArithmetic.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalHitting.StackLanguage.unaryMulStep_iterate line 8
  2. theorem OAI.RationalHitting.StackLanguage.Poly.unaryMul line 16
  3. theorem OAI.RationalHitting.StackLanguage.Poly.unaryPow line 31
  4. abbrev OAI.RationalHitting.StackLanguage.DivState line 45
  5. def OAI.RationalHitting.StackLanguage.divStep line 46
  6. lemma OAI.RationalHitting.StackLanguage.divStep_size line 50
  7. lemma OAI.RationalHitting.StackLanguage.divStep_iterate_size line 54
  8. lemma OAI.RationalHitting.StackLanguage.divStep_expected line 63
  9. lemma OAI.RationalHitting.StackLanguage.divStep_iterate line 84
  10. theorem OAI.RationalHitting.StackLanguage.Poly.divStep_poly line 93
  11. theorem OAI.RationalHitting.StackLanguage.Poly.unaryDivMod line 109
  12. theorem OAI.RationalHitting.StackLanguage.Poly.unaryDiv line 119
  13. theorem OAI.RationalHitting.StackLanguage.Poly.unaryMod line 120
  14. def OAI.RationalHitting.StackLanguage.Procedure.wordLength line 129
  15. theorem OAI.RationalHitting.StackLanguage.Poly.bitLength line 145
  16. theorem OAI.RationalHitting.StackLanguage.Poly.natBitLength line 149
  17. theorem OAI.RationalHitting.StackLanguage.Poly.natSize line 153
  18. def OAI.RationalHitting.StackLanguage.doubleBelow line 162
  19. def OAI.RationalHitting.StackLanguage.doubleState line 164
  20. lemma OAI.RationalHitting.StackLanguage.doubleBelow_iterate_bound line 166
  21. lemma OAI.RationalHitting.StackLanguage.doubleState_iterate line 177
  22. lemma OAI.RationalHitting.StackLanguage.doubleBelow_iterate_pow line 183
  23. lemma OAI.RationalHitting.StackLanguage.nat_size_log line 195
  24. theorem OAI.RationalHitting.StackLanguage.Poly.doubleState_poly line 205
  25. theorem OAI.RationalHitting.StackLanguage.Poly.unaryNextPower line 212
  26. theorem OAI.RationalHitting.StackLanguage.Poly.unaryLogTwo line 225