OAI/Computability/SpaceSimulation/Stack/Count.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Unbounded binary increment and decrement. Simple stack algorithms.

  1. def OAI.Fifths.Bin.lastDigit line 11

    Source documentation

    Write at most one bit before the uncopied high bits.

    def lastDigit (inc more : Bool) : List Bool :=
…
  2. def OAI.Fifths.Bin.tick line 14
  3. theorem OAI.Fifths.Bin.tick_inc line 20
  4. theorem OAI.Fifths.Bin.tick_dec line 34
  5. def OAI.Fifths.SM.finishDigit line 61
  6. def OAI.Fifths.SM.finish line 64
  7. def OAI.Fifths.SM.continueCarry line 67
  8. def OAI.Fifths.SM.carry line 73
  9. theorem OAI.Fifths.SM.exec_finish line 76
  10. def OAI.Fifths.SM.carried line 94
  11. theorem OAI.Fifths.SM.exec_carry line 97