OAI/Computability/RationalHitting/BinaryGcd.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.subEmbed line 8
  2. def OAI.RationalHitting.StackLanguage.subtract10 line 10
  3. lemma OAI.RationalHitting.StackLanguage.eval_subtract10 line 12
  4. def OAI.RationalHitting.StackLanguage.reducePick line 28
  5. lemma OAI.RationalHitting.StackLanguage.eval_reducePick line 31
  6. def OAI.RationalHitting.StackLanguage.reduceOnce line 52
  7. def OAI.RationalHitting.StackLanguage.divScratch line 56
  8. lemma OAI.RationalHitting.StackLanguage.eval_reduceOnce line 59
  9. lemma OAI.RationalHitting.StackLanguage.wordValue_bits line 106
  10. def OAI.RationalHitting.StackLanguage.divBody line 114

    Source documentation

    Remainder 0, denominator 5, unread MSD numerator 6, quotient 7.

    def divBody : Program (Fin 10) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  11. def OAI.RationalHitting.StackLanguage.divLoop line 116
  12. lemma OAI.RationalHitting.StackLanguage.eval_divBody line 118
  13. lemma OAI.RationalHitting.StackLanguage.eval_divLoop line 136
  14. def OAI.RationalHitting.StackLanguage.divide line 177

    Source documentation

    Binary division starts with numerator in 0 and denominator in 5. The original denominator is retained; quotient is placed in 7, remainder in 0. Every other register is cleared.

    def divide : Program (Fin 10) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  15. lemma OAI.RationalHitting.StackLanguage.eval_divide line 180