OAI/Computability/RationalHitting/StackWords.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.clear line 9
  2. def OAI.RationalHitting.StackLanguage.reverse line 10
  3. lemma OAI.RationalHitting.StackLanguage.eval_clear line 12
  4. lemma OAI.RationalHitting.StackLanguage.transfer_cons line 27
  5. lemma OAI.RationalHitting.StackLanguage.eval_reverse line 31
  6. def OAI.RationalHitting.StackLanguage.copyHead line 57

    Source documentation

    Copy a nonempty head to another register without consuming it.

    def copyHead (a b : K) : Program K := .branch a .skip (.push b false) (.push b true)

    Mentions: OAI.RationalHitting.StackLanguage.Program

  7. lemma OAI.RationalHitting.StackLanguage.eval_copyHead line 59
  8. def OAI.RationalHitting.StackLanguage.duplicateReverse line 66

    Source documentation

    Two simultaneous reversed copies of a word, consuming the operand.

    def duplicateReverse (a b c : K) : Program K :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  9. lemma OAI.RationalHitting.StackLanguage.eval_duplicateReverse line 69
  10. def OAI.RationalHitting.StackLanguage.copy line 102

    Source documentation

    Copy an arbitrary binary word, restoring the operand and clearing temporary storage; all registers have fixed indices.

    def copy (a b tmp : K) : Program K :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  11. lemma OAI.RationalHitting.StackLanguage.eval_copy line 105
  12. def OAI.RationalHitting.StackLanguage.wordValue line 137

    Source documentation

    Little-endian binary words; zero has the empty word.

    def wordValue : List Bool → ℕ
  | [] => 0
  | b::l => (if b then 1 else 0)+2*wordValue l
  13. def OAI.RationalHitting.StackLanguage.incrementWord line 141
  14. theorem OAI.RationalHitting.StackLanguage.incrementWord_value line 146
  15. def OAI.RationalHitting.StackLanguage.carrySplit line 151
  16. theorem OAI.RationalHitting.StackLanguage.carrySplit_spec line 156
  17. theorem OAI.RationalHitting.StackLanguage.carrySplit_length line 165
  18. theorem OAI.RationalHitting.StackLanguage.incrementWord_length line 170
  19. def OAI.RationalHitting.StackLanguage.incrementBody line 175
  20. def OAI.RationalHitting.StackLanguage.incrementLoop line 180
  21. lemma OAI.RationalHitting.StackLanguage.eval_incrementLoop line 182
  22. def OAI.RationalHitting.StackLanguage.increment line 248
  23. lemma OAI.RationalHitting.StackLanguage.eval_increment line 252