OAI/Analysis/MatrixSigning/Arithmetic/BorrowSubtractor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.BorrowSubtractor.borrowState line 11
  2. def OAI.KS.W19.BorrowSubtractor.finishEntry line 13
  3. def OAI.KS.W19.BorrowSubtractor.subEntry line 16
  4. def OAI.KS.W19.BorrowSubtractor.dispatch line 19
  5. def OAI.KS.W19.BorrowSubtractor.machine line 26
  6. def OAI.KS.W19.BorrowSubtractor.cfg line 28
  7. theorem OAI.KS.W19.BorrowSubtractor.table_lookup line 31
  8. theorem OAI.KS.W19.BorrowSubtractor.step_left_cons line 47
  9. theorem OAI.KS.W19.BorrowSubtractor.step_right_cons line 66
  10. theorem OAI.KS.W19.BorrowSubtractor.step_done line 78
  11. theorem OAI.KS.W19.BorrowSubtractor.run_sub line 89
  12. theorem OAI.KS.W19.BorrowSubtractor.run_borrow_flag line 141
  13. theorem OAI.KS.W19.BorrowSubtractor.table_length line 154