OAI/Analysis/MatrixSigning/Arithmetic/BinaryMultiply.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W03.BinaryMultiply.shift line 14
  2. theorem OAI.KS.W03.BinaryMultiply.shift_value line 16
  3. theorem OAI.KS.W03.BinaryMultiply.shift_length line 19
  4. def OAI.KS.W03.BinaryMultiply.multiplyRaw line 21
  5. theorem OAI.KS.W03.BinaryMultiply.multiplyRaw_correct line 26
  6. theorem OAI.KS.W03.BinaryMultiply.multiplyRaw_length_le line 33
  7. def OAI.KS.W03.BinaryMultiply.multiply line 44
  8. theorem OAI.KS.W03.BinaryMultiply.multiply_correct line 46
  9. theorem OAI.KS.W03.BinaryMultiply.multiply_length_le line 50
  10. theorem OAI.KS.W03.BinaryMultiply.multiply_encodeNat line 60
  11. def OAI.KS.W03.BinaryMultiply.rippleVisits line 65
  12. theorem OAI.KS.W03.BinaryMultiply.rippleVisits_eq line 72
  13. theorem OAI.KS.W03.BinaryMultiply.rippleVisits_machine_correct line 90
  14. def OAI.KS.W03.BinaryMultiply.multiplyRawVisits line 98
  15. theorem OAI.KS.W03.BinaryMultiply.multiplyRawVisits_le line 103
  16. def OAI.KS.W03.BinaryMultiply.multiplyVisits line 118
  17. theorem OAI.KS.W03.BinaryMultiply.multiplyVisits_le line 121
  18. def OAI.KS.W03.BinaryMultiply.primitiveCharge line 129
  19. theorem OAI.KS.W03.BinaryMultiply.primitiveCharge_le line 131