OAI/Analysis/MatrixSigning/Arithmetic/BisectionArithmetic.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KS.W28.Workspace line 10
  2. abbrev OAI.KS.W28.BisectionArithmetic.Workspace line 16
  3. def OAI.KS.W28.BisectionArithmetic.clearAfter line 18
  4. theorem OAI.KS.W28.BisectionArithmetic.clear_spec line 21
  5. def OAI.KS.W28.BisectionArithmetic.moveAfter line 33
  6. theorem OAI.KS.W28.BisectionArithmetic.move_spec line 37
  7. theorem OAI.KS.W28.BisectionArithmetic.copy_spec line 44
  8. def OAI.KS.W28.BisectionArithmetic.addEmitProgram line 53
  9. def OAI.KS.W28.BisectionArithmetic.addProgram line 56
  10. def OAI.KS.W28.BisectionArithmetic.sumBits line 59
  11. theorem OAI.KS.W28.BisectionArithmetic.sumBits_value line 61
  12. theorem OAI.KS.W28.BisectionArithmetic.sumBits_length_le line 65
  13. theorem OAI.KS.W28.BisectionArithmetic.add_emit_spec line 69
  14. theorem OAI.KS.W28.BisectionArithmetic.add_spec line 95
  15. def OAI.KS.W28.BisectionArithmetic.shiftDispatch line 106
  16. def OAI.KS.W28.BisectionArithmetic.shiftProgram line 110
  17. def OAI.KS.W28.BisectionArithmetic.shiftAfter line 113
  18. theorem OAI.KS.W28.BisectionArithmetic.shift_spec line 116
  19. def OAI.KS.W28.BisectionArithmetic.productRawAfter line 131
  20. def OAI.KS.W28.BisectionArithmetic.productAfter line 137
  21. def OAI.KS.W28.BisectionArithmetic.productProgram line 140
  22. theorem OAI.KS.W28.BisectionArithmetic.product_spec line 144
  23. theorem OAI.KS.W28.BisectionArithmetic.registers_self line 173
  24. def OAI.KS.W28.BisectionArithmetic.addAfter line 185
  25. theorem OAI.KS.W28.BisectionArithmetic.add_spec_stacks line 188
  26. theorem OAI.KS.W28.BisectionArithmetic.productAfter_on line 196
  27. theorem OAI.KS.W28.BisectionArithmetic.productAfter_off line 206