OAI/GroupTheory/PeriodicGroups/Machines/BinaryRegisters.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.Structured.Binary.clear line 12
  2. def OAI.SourceBurnside.Structured.Binary.move line 13
  3. def OAI.SourceBurnside.Structured.Binary.spread line 14
  4. def OAI.SourceBurnside.Structured.Binary.copy line 16
  5. lemma OAI.SourceBurnside.Structured.Binary.clear_run line 18
  6. lemma OAI.SourceBurnside.Structured.Binary.move_run line 34
  7. lemma OAI.SourceBurnside.Structured.Binary.spread_run line 69
  8. lemma OAI.SourceBurnside.Structured.Binary.copy_run line 117
  9. abbrev OAI.SourceBurnside.Structured.Binary.Add.K line 145
  10. def OAI.SourceBurnside.Structured.Binary.Add.bit line 147
  11. def OAI.SourceBurnside.Structured.Binary.Add.value line 148
  12. def OAI.SourceBurnside.Structured.Binary.Add.low line 150
  13. def OAI.SourceBurnside.Structured.Binary.Add.high line 151
  14. lemma OAI.SourceBurnside.Structured.Binary.Add.adder_equation line 152
  15. lemma OAI.SourceBurnside.Structured.Binary.Add.low_symm line 154
  16. lemma OAI.SourceBurnside.Structured.Binary.Add.high_symm line 155
  17. lemma OAI.SourceBurnside.Structured.Binary.Add.value_append line 157
  18. def OAI.SourceBurnside.Structured.Binary.Add.store line 162
  19. def OAI.SourceBurnside.Structured.Binary.Add.fullAdder line 164
  20. def OAI.SourceBurnside.Structured.Binary.Add.step line 166
  21. def OAI.SourceBurnside.Structured.Binary.Add.firstPass line 167
  22. def OAI.SourceBurnside.Structured.Binary.Add.partialStore line 169
  23. lemma OAI.SourceBurnside.Structured.Binary.Add.pop_carry line 171
  24. lemma OAI.SourceBurnside.Structured.Binary.Add.fullAdder_push line 174
  25. lemma OAI.SourceBurnside.Structured.Binary.Add.fullAdder_run line 179
  26. lemma OAI.SourceBurnside.Structured.Binary.Add.pop_right line 198
  27. lemma OAI.SourceBurnside.Structured.Binary.Add.pop_left line 201
  28. lemma OAI.SourceBurnside.Structured.Binary.Add.step_run line 205
  29. def OAI.SourceBurnside.Structured.Binary.Add.scan line 215
  30. lemma OAI.SourceBurnside.Structured.Binary.Add.scan_length line 221
  31. lemma OAI.SourceBurnside.Structured.Binary.Add.firstPass_run line 226
  32. lemma OAI.SourceBurnside.Structured.Binary.Add.scan_value line 243
  33. lemma OAI.SourceBurnside.Structured.Binary.Add.scan_remaining line 264
  34. lemma OAI.SourceBurnside.Structured.Binary.Add.value_lt line 269
  35. def OAI.SourceBurnside.Structured.Binary.Add.fixedAdd line 274
  36. theorem OAI.SourceBurnside.Structured.Binary.Add.fixedAdd_run line 276
  37. lemma OAI.SourceBurnside.Structured.Binary.Add.scan_sum line 294
  38. lemma OAI.SourceBurnside.Structured.Binary.Add.scan_mod line 299
  39. lemma OAI.SourceBurnside.Structured.Binary.Add.scan_exact line 306
  40. def OAI.SourceBurnside.Structured.Binary.mapMove line 324
  41. def OAI.SourceBurnside.Structured.Binary.mapInPlace line 325
  42. lemma OAI.SourceBurnside.Structured.Binary.mapMove_run line 327
  43. lemma OAI.SourceBurnside.Structured.Binary.mapInPlace_run line 361
  44. def OAI.SourceBurnside.Structured.Program.relabel line 387
  45. def OAI.SourceBurnside.Structured.Agrees line 396
  46. def OAI.SourceBurnside.Structured.Outside line 397
  47. lemma OAI.SourceBurnside.Structured.agrees_update line 399
  48. lemma OAI.SourceBurnside.Structured.outside_update line 408
  49. lemma OAI.SourceBurnside.Structured.outside_refl line 413
  50. lemma OAI.SourceBurnside.Structured.Outside.trans line 415
  51. theorem OAI.SourceBurnside.Structured.Run.relabel line 418
  52. lemma OAI.SourceBurnside.Structured.Binary.Add.complement_value line 454
  53. lemma OAI.SourceBurnside.Structured.Binary.Add.subtract_equation line 461
  54. lemma OAI.SourceBurnside.Structured.Binary.Add.subtract_carry line 471
  55. lemma OAI.SourceBurnside.Structured.Binary.Add.subtract_exact line 479
  56. def OAI.SourceBurnside.Structured.Binary.Add.fixedSubtract line 486
  57. theorem OAI.SourceBurnside.Structured.Binary.Add.fixedSubtract_run line 488
  58. lemma OAI.SourceBurnside.Structured.agrees_outside_unique line 509
  59. lemma OAI.SourceBurnside.Structured.Run.relabel_to line 518
  60. def OAI.SourceBurnside.Structured.Binary.patch4 line 527
  61. lemma OAI.SourceBurnside.Structured.Binary.patch4_agrees line 531
  62. lemma OAI.SourceBurnside.Structured.Binary.patch4_outside line 537
  63. lemma OAI.SourceBurnside.Structured.Binary.patch4_run line 542
  64. lemma OAI.SourceBurnside.Structured.Binary.fixedAdd_call line 547
  65. def OAI.SourceBurnside.Structured.Binary.dropFront line 561
  66. def OAI.SourceBurnside.Structured.Binary.shift line 563
  67. lemma OAI.SourceBurnside.Structured.Binary.dropFront_run line 565
  68. lemma OAI.SourceBurnside.Structured.Binary.shift_run line 591
  69. def OAI.SourceBurnside.Structured.Binary.Add.double line 605
  70. lemma OAI.SourceBurnside.Structured.Binary.Add.double_length line 606
  71. lemma OAI.SourceBurnside.Structured.Binary.Add.double_reverse line 609
  72. lemma OAI.SourceBurnside.Structured.Binary.Add.double_value line 612