OAI/Analysis/MatrixSigning/Machines/BinaryToUnaryMachine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W03.BinaryToUnary.doubleState line 11
  2. def OAI.KS.W03.BinaryToUnary.secondState line 12
  3. def OAI.KS.W03.BinaryToUnary.restoreState line 13
  4. def OAI.KS.W03.BinaryToUnary.instruction line 15
  5. def OAI.KS.W03.BinaryToUnary.dispatch line 19
  6. def OAI.KS.W03.BinaryToUnary.machine line 39
  7. def OAI.KS.W03.BinaryToUnary.cfg line 41
  8. theorem OAI.KS.W03.BinaryToUnary.init_eq line 44
  9. theorem OAI.KS.W03.BinaryToUnary.reverse_step line 51
  10. theorem OAI.KS.W03.BinaryToUnary.reverse_done line 62
  11. theorem OAI.KS.W03.BinaryToUnary.guard_done line 71
  12. theorem OAI.KS.W03.BinaryToUnary.guard_step line 80
  13. theorem OAI.KS.W03.BinaryToUnary.double_step line 91
  14. theorem OAI.KS.W03.BinaryToUnary.second_step line 102
  15. theorem OAI.KS.W03.BinaryToUnary.double_done line 113
  16. theorem OAI.KS.W03.BinaryToUnary.restore_step line 124
  17. theorem OAI.KS.W03.BinaryToUnary.restore_done line 135