OAI/Computability/SpaceSimulation/Register/Arithmetic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic operators in the bit-space closure. Many are intentionally very slow.

  1. theorem OAI.Fifths.Comp.add line 12
  2. theorem OAI.Fifths.Comp.sub line 19
  3. theorem OAI.Fifths.Comp.mul line 29
  4. theorem OAI.Fifths.Comp.pow line 38
  5. theorem OAI.Fifths.Comp.flip line 58
  6. theorem OAI.Fifths.Comp.both line 62
  7. theorem OAI.Fifths.Comp.either line 67
  8. theorem OAI.Fifths.Comp.lt line 72
  9. theorem OAI.Fifths.Comp.le line 79
  10. theorem OAI.Fifths.Comp.eq line 85
  11. theorem OAI.Fifths.Comp.min line 93
  12. theorem OAI.Fifths.Comp.max line 99
  13. theorem OAI.Fifths.Comp.div_step line 106
  14. theorem OAI.Fifths.Comp.div line 122
  15. theorem OAI.Fifths.Comp.mod line 134
  16. theorem OAI.Fifths.Comp.size line 142