OAI/Analysis/MatrixSigning/Arithmetic/BinarySubtractor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.BinarySubtractor.borrowState line 11
  2. def OAI.KS.W19.BinarySubtractor.finishEntry line 13
  3. def OAI.KS.W19.BinarySubtractor.subEntry line 16
  4. def OAI.KS.W19.BinarySubtractor.dispatch line 19
  5. def OAI.KS.W19.BinarySubtractor.machine line 26
  6. def OAI.KS.W19.BinarySubtractor.cfg line 28
  7. theorem OAI.KS.W19.BinarySubtractor.table_lookup line 31
  8. theorem OAI.KS.W19.BinarySubtractor.step_left_cons line 47
  9. theorem OAI.KS.W19.BinarySubtractor.step_right_cons line 66
  10. theorem OAI.KS.W19.BinarySubtractor.step_done line 78
  11. theorem OAI.KS.W19.BinarySubtractor.run_sub line 89
  12. theorem OAI.KS.W19.BinarySubtractor.run_correct line 141
  13. theorem OAI.KS.W19.BinarySubtractor.run_encodedNat_correct line 155
  14. theorem OAI.KS.W19.BinarySubtractor.transition_bound line 168
  15. theorem OAI.KS.W19.BinarySubtractor.table_length line 171