OAI/Analysis/MatrixSigning/Arithmetic/BinaryDivision.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.digit line 10
  2. theorem OAI.KS.W19.digit_false line 12
  3. theorem OAI.KS.W19.digit_true line 13
  4. def OAI.KS.W19.bitsValue line 15
  5. theorem OAI.KS.W19.digit_le_one line 19
  6. def OAI.KS.W19.compareDigit line 21
  7. def OAI.KS.W19.compareBits line 24
  8. def OAI.KS.W19.OrderingCorrect line 38
  9. theorem OAI.KS.W19.compareBits_correct line 44
  10. theorem OAI.KS.W19.compareBits_lt_iff line 68
  11. def OAI.KS.W19.differenceDigit line 73
  12. def OAI.KS.W19.nextBorrow line 75
  13. theorem OAI.KS.W19.subtraction_column line 78
  14. def OAI.KS.W19.subtractBits line 83
  15. theorem OAI.KS.W19.tail_borrow_le line 91
  16. theorem OAI.KS.W19.subtraction_lift line 98
  17. theorem OAI.KS.W19.subtractBits_correct line 105
  18. theorem OAI.KS.W19.subtractBits_length line 135
  19. def OAI.KS.W19.divideBits line 147
  20. theorem OAI.KS.W19.divideBits_correct line 157
  21. theorem OAI.KS.W19.divideBits_quotient_length line 183
  22. theorem OAI.KS.W19.divideBits_remainder_length line 189
  23. theorem OAI.KS.W19.bitsValue_encodePosNum line 201
  24. theorem OAI.KS.W19.bitsValue_encodeNum line 206
  25. theorem OAI.KS.W19.bitsValue_encodeNat line 212
  26. theorem OAI.KS.W19.divideBits_encodeNat_correct line 216
  27. def OAI.KS.W19.bitScanCost line 223
  28. theorem OAI.KS.W19.bitScanCost_eq line 231
  29. def OAI.KS.W19.divisionIterations line 243
  30. theorem OAI.KS.W19.divisionIterations_eq_length line 247
  31. def OAI.KS.W19.divisionBitCost line 250
  32. theorem OAI.KS.W19.divisionBitCost_le line 258
  33. theorem OAI.KS.W19.divideBits_output_length_le line 273
  34. theorem OAI.KS.W19.encodeNat_length_eq_size line 280
  35. theorem OAI.KS.W19.divisionBitCost_encodeNat_le line 283
  36. def OAI.KS.W19.signedBitsValue line 289
  37. def OAI.KS.W19.divideSignedBits line 292
  38. theorem OAI.KS.W19.divideSignedBits_correct line 298
  39. theorem OAI.KS.W19.divideSignedBits_output_length_le line 335
  40. theorem OAI.KS.W19.divideSignedBits_quotient line 347
  41. def OAI.KS.W19.signedDivisionBitCost line 360
  42. theorem OAI.KS.W19.signedDivisionBitCost_le line 366
  43. theorem OAI.KS.W19.signedDivisionBitCost_quadratic line 382
  44. def OAI.KS.W19.negativeOfInt line 387
  45. theorem OAI.KS.W19.signedBitsValue_intPayload line 391
  46. theorem OAI.KS.W19.divideSignedBits_intPayload_quotient line 395