OAI/Algebra/FormulaHitting/BitArithmetic.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.BitArithmetic.value line 12
  2. def OAI.NCHitting.BitArithmetic.parity line 16
  3. def OAI.NCHitting.BitArithmetic.carry line 17
  4. def OAI.NCHitting.BitArithmetic.borrow line 18
  5. def OAI.NCHitting.BitArithmetic.equalStep line 19
  6. theorem OAI.NCHitting.BitArithmetic.fullAdder_identity line 21
  7. theorem OAI.NCHitting.BitArithmetic.fullSubtractor_identity line 25
  8. structure OAI.NCHitting.BitArithmetic.WordRun line 29
  9. def OAI.NCHitting.BitArithmetic.trim line 33
  10. def OAI.NCHitting.BitArithmetic.trimSteps line 39
  11. theorem OAI.NCHitting.BitArithmetic.trimSteps_eq line 43
  12. theorem OAI.NCHitting.BitArithmetic.value_trim line 48
  13. theorem OAI.NCHitting.BitArithmetic.bits_value line 59
  14. theorem OAI.NCHitting.BitArithmetic.value_bits line 77
  15. theorem OAI.NCHitting.BitArithmetic.trim_length line 84
  16. def OAI.NCHitting.BitArithmetic.addRaw line 87
  17. theorem OAI.NCHitting.BitArithmetic.addRaw_value line 99
  18. theorem OAI.NCHitting.BitArithmetic.addRaw_length line 122
  19. theorem OAI.NCHitting.BitArithmetic.addRaw_steps line 143
  20. def OAI.NCHitting.BitArithmetic.add line 164
  21. theorem OAI.NCHitting.BitArithmetic.add_value line 168
  22. theorem OAI.NCHitting.BitArithmetic.add_steps line 171
  23. structure OAI.NCHitting.BitArithmetic.BoolRun line 178
  24. def OAI.NCHitting.BitArithmetic.lessRaw line 182
  25. theorem OAI.NCHitting.BitArithmetic.lessRaw_value line 194
  26. theorem OAI.NCHitting.BitArithmetic.lessRaw_steps line 212
  27. def OAI.NCHitting.BitArithmetic.equalRaw line 233
  28. theorem OAI.NCHitting.BitArithmetic.equalRaw_value line 245
  29. theorem OAI.NCHitting.BitArithmetic.equalRaw_steps line 263
  30. structure OAI.NCHitting.BitArithmetic.SubRun line 284
  31. def OAI.NCHitting.BitArithmetic.subRaw line 287
  32. theorem OAI.NCHitting.BitArithmetic.subRaw_borrow line 299
  33. theorem OAI.NCHitting.BitArithmetic.subRaw_value line 309
  34. theorem OAI.NCHitting.BitArithmetic.subRaw_length line 338
  35. theorem OAI.NCHitting.BitArithmetic.subRaw_steps line 347
  36. def OAI.NCHitting.BitArithmetic.sub line 368
  37. theorem OAI.NCHitting.BitArithmetic.sub_value line 373
  38. theorem OAI.NCHitting.BitArithmetic.sub_steps line 386
  39. def OAI.NCHitting.BitArithmetic.mulRaw line 394
  40. theorem OAI.NCHitting.BitArithmetic.mulRaw_value line 403
  41. theorem OAI.NCHitting.BitArithmetic.mulRaw_length line 410
  42. theorem OAI.NCHitting.BitArithmetic.mulRaw_steps line 419
  43. def OAI.NCHitting.BitArithmetic.mul line 429
  44. theorem OAI.NCHitting.BitArithmetic.mul_value line 433
  45. theorem OAI.NCHitting.BitArithmetic.mul_steps line 436
  46. def OAI.NCHitting.BitArithmetic.addNat line 444
  47. def OAI.NCHitting.BitArithmetic.subNat line 445
  48. def OAI.NCHitting.BitArithmetic.mulNat line 446
  49. def OAI.NCHitting.BitArithmetic.lessNat line 447
  50. def OAI.NCHitting.BitArithmetic.equalNat line 448
  51. def OAI.NCHitting.BitArithmetic.oddNat line 449
  52. theorem OAI.NCHitting.BitArithmetic.oddNat_value line 451
  53. theorem OAI.NCHitting.BitArithmetic.oddNat_eq line 457
  54. theorem OAI.NCHitting.BitArithmetic.addNat_value line 461
  55. theorem OAI.NCHitting.BitArithmetic.mulNat_value line 464
  56. theorem OAI.NCHitting.BitArithmetic.subNat_value line 467
  57. theorem OAI.NCHitting.BitArithmetic.lessNat_value line 480
  58. theorem OAI.NCHitting.BitArithmetic.equalNat_value line 484
  59. theorem OAI.NCHitting.BitArithmetic.addNat_steps line 488
  60. theorem OAI.NCHitting.BitArithmetic.subNat_steps line 494
  61. theorem OAI.NCHitting.BitArithmetic.lessNat_steps line 500
  62. theorem OAI.NCHitting.BitArithmetic.equalNat_steps line 506
  63. theorem OAI.NCHitting.BitArithmetic.mulNat_steps line 512