OAI/Computability/RationalHitting/BinaryAddition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalHitting.StackLanguage.wordValue_head_tail line 9
  2. def OAI.RationalHitting.StackLanguage.addWord line 17

    Source documentation

    Grade-school addition, scanning the second operand one bit at a time. The first operand is shifted after adding the incoming low bit.

    def addWord : List Bool → List Bool → List Bool
  | a, [] => a
  | a, false::b => a.headD false :: addWord a.tail b
  | a, true::b => (incrementWord a).headD false :: addWord (incrementWord a).tail b

    Mentions: OAI.RationalHitting.StackLanguage.incrementWord

  3. theorem OAI.RationalHitting.StackLanguage.addWord_value line 22
  4. lemma OAI.RationalHitting.StackLanguage.incrementWord_tail_length line 38
  5. lemma OAI.RationalHitting.StackLanguage.addWord_length line 43
  6. def OAI.RationalHitting.StackLanguage.emitLow line 60

    Source documentation

    Emits one least-significant bit, supplying zero for an exhausted operand.

    def emitLow (a out : K) : Program K :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  7. lemma OAI.RationalHitting.StackLanguage.eval_emitLow line 63
  8. def OAI.RationalHitting.StackLanguage.addSplit line 82

    Source documentation

    Output invariant for the single pass: a reversed low part is on out.

    def addSplit : List Bool → List Bool → List Bool × List Bool
  | a, [] => ([],a)
  | a, false::b =>
    let r := addSplit a.tail b
…
  9. lemma OAI.RationalHitting.StackLanguage.addSplit_spec line 91
  10. lemma OAI.RationalHitting.StackLanguage.addSplit_first_length line 96
  11. def OAI.RationalHitting.StackLanguage.addBody line 101
  12. def OAI.RationalHitting.StackLanguage.addLoop line 105
  13. lemma OAI.RationalHitting.StackLanguage.eval_addLoop line 107
  14. def OAI.RationalHitting.StackLanguage.add line 196

    Source documentation

    Destructive binary addition. The second operand and all scratch words are cleared; the first register holds the exact sum.

    def add (a b out tmp flag : K) : Program K :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  15. lemma OAI.RationalHitting.StackLanguage.eval_add line 200