OAI/GroupTheory/PeriodicGroups/Machines/ArithmeticDevices.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SourceBurnside.Structured.Binary.Multiply.K line 10
2. def OAI.SourceBurnside.Structured.Binary.Multiply.store line 12
3. def OAI.SourceBurnside.Structured.Binary.Multiply.regs line 13
4. lemma OAI.SourceBurnside.Structured.Binary.Multiply.regs_injective line 14
5. def OAI.SourceBurnside.Structured.Binary.Multiply.addX line 16
6. def OAI.SourceBurnside.Structured.Binary.Multiply.addStore line 19
7. def OAI.SourceBurnside.Structured.Binary.Multiply.carryStore line 20
8. lemma OAI.SourceBurnside.Structured.Binary.Multiply.addX_run line 22
9. def OAI.SourceBurnside.Structured.Binary.Multiply.plusIf line 51
10. def OAI.SourceBurnside.Structured.Binary.Multiply.step line 53
11. def OAI.SourceBurnside.Structured.Binary.Multiply.stepCost line 54
12. lemma OAI.SourceBurnside.Structured.Binary.Multiply.step_run line 56
13. def OAI.SourceBurnside.Structured.Binary.Multiply.scan line 74
14. def OAI.SourceBurnside.Structured.Binary.Multiply.time line 78
15. def OAI.SourceBurnside.Structured.Binary.Multiply.program line 82
16. lemma OAI.SourceBurnside.Structured.Binary.Multiply.plusIf_length line 84
17. lemma OAI.SourceBurnside.Structured.Binary.Multiply.scan_length line 87
18. lemma OAI.SourceBurnside.Structured.Binary.Multiply.program_run line 99
19. lemma OAI.SourceBurnside.Structured.Binary.Multiply.time_bound line 117
20. lemma OAI.SourceBurnside.Structured.Binary.Multiply.plusIf_modEq line 122
21. lemma OAI.SourceBurnside.Structured.Binary.Multiply.scan_modEq line 132
22. lemma OAI.SourceBurnside.Structured.Binary.Multiply.scan_value line 149
23. def OAI.SourceBurnside.Structured.Binary.roll line 162
24. def OAI.SourceBurnside.Structured.Binary.rollBits line 163
25. lemma OAI.SourceBurnside.Structured.Binary.rollBits_length line 164
26. lemma OAI.SourceBurnside.Structured.Binary.rollBits_reverse line 167
27. lemma OAI.SourceBurnside.Structured.Binary.roll_run line 169
28. lemma OAI.SourceBurnside.Structured.Binary.rollBits_value line 181
29. abbrev OAI.SourceBurnside.Structured.Binary.Divide.K line 199
30. def OAI.SourceBurnside.Structured.Binary.Divide.store line 201
31. def OAI.SourceBurnside.Structured.Binary.Divide.scratchStore line 202
32. def OAI.SourceBurnside.Structured.Binary.Divide.trialStore line 204
33. def OAI.SourceBurnside.Structured.Binary.Divide.regs line 206
34. lemma OAI.SourceBurnside.Structured.Binary.Divide.regs_injective line 207
35. def OAI.SourceBurnside.Structured.Binary.Divide.choose line 209
36. def OAI.SourceBurnside.Structured.Binary.Divide.chooseTime line 212
37. lemma OAI.SourceBurnside.Structured.Binary.Divide.choose_run line 214
38. def OAI.SourceBurnside.Structured.Binary.Divide.trial line 259
39. def OAI.SourceBurnside.Structured.Binary.Divide.carry line 260
40. def OAI.SourceBurnside.Structured.Binary.Divide.makeTrial line 262
41. lemma OAI.SourceBurnside.Structured.Binary.Divide.makeTrial_run line 265
42. def OAI.SourceBurnside.Structured.Binary.Divide.oneStep line 299
43. def OAI.SourceBurnside.Structured.Binary.Divide.step line 303
44. def OAI.SourceBurnside.Structured.Binary.Divide.stepTime line 305
45. lemma OAI.SourceBurnside.Structured.Binary.Divide.oneStep_lengths line 308
46. lemma OAI.SourceBurnside.Structured.Binary.Divide.step_run line 317
47. def OAI.SourceBurnside.Structured.Binary.Divide.scan line 349
48. def OAI.SourceBurnside.Structured.Binary.Divide.time line 353
49. def OAI.SourceBurnside.Structured.Binary.Divide.program line 357
50. lemma OAI.SourceBurnside.Structured.Binary.Divide.scan_lengths line 359
51. lemma OAI.SourceBurnside.Structured.Binary.Divide.program_run line 370
52. lemma OAI.SourceBurnside.Structured.Binary.Divide.time_bound line 389
53. lemma OAI.SourceBurnside.Structured.Binary.Divide.oneStep_value line 404
54. def OAI.SourceBurnside.Structured.Binary.Divide.feed line 444
55. lemma OAI.SourceBurnside.Structured.Binary.Divide.feed_le line 448
56. lemma OAI.SourceBurnside.Structured.Binary.Divide.feed_value line 453
57. lemma OAI.SourceBurnside.Structured.Binary.Divide.scan_value line 459
58. lemma OAI.SourceBurnside.Structured.Binary.Divide.zero_value line 481
59. theorem OAI.SourceBurnside.Structured.Binary.Divide.division line 486
60. def OAI.SourceBurnside.Structured.Device.input line 521
61. def OAI.SourceBurnside.Structured.Device.values line 522
62. def OAI.SourceBurnside.Structured.Device.result line 524
63. structure OAI.SourceBurnside.Structured.Device.Realizer line 527
64. lemma OAI.SourceBurnside.Structured.Device.Realizer.transport line 542
65. abbrev OAI.SourceBurnside.Structured.Device.Compose.Work line 559
66. def OAI.SourceBurnside.Structured.Device.Compose.left line 561
67. def OAI.SourceBurnside.Structured.Device.Compose.right line 562
68. def OAI.SourceBurnside.Structured.Device.Compose.call line 563
69. lemma OAI.SourceBurnside.Structured.Device.Compose.left_injective line 567
70. lemma OAI.SourceBurnside.Structured.Device.Compose.right_injective line 571
71. lemma OAI.SourceBurnside.Structured.Device.Compose.call_injective line 575
72. def OAI.SourceBurnside.Structured.Device.Compose.body line 585
73. lemma OAI.SourceBurnside.Structured.Device.Compose.body_run line 590
74. def OAI.SourceBurnside.Structured.Device.Compose.realizer line 641
75. def OAI.SourceBurnside.Structured.Device.read line 655