OAI/GroupTheory/PeriodicGroups/Machines/RegisterLoops.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SourceBurnside.Structured.Binary.Decrement.K line 10
2. def OAI.SourceBurnside.Structured.Binary.Decrement.store line 12
3. def OAI.SourceBurnside.Structured.Binary.Decrement.partialStore line 13
4. def OAI.SourceBurnside.Structured.Binary.Decrement.low line 14
5. def OAI.SourceBurnside.Structured.Binary.Decrement.borrow line 15
6. lemma OAI.SourceBurnside.Structured.Binary.Decrement.bit_equation line 16
7. def OAI.SourceBurnside.Structured.Binary.Decrement.step line 19
8. def OAI.SourceBurnside.Structured.Binary.Decrement.pass line 21
9. def OAI.SourceBurnside.Structured.Binary.Decrement.program line 22
10. def OAI.SourceBurnside.Structured.Binary.Decrement.scan line 23
11. lemma OAI.SourceBurnside.Structured.Binary.Decrement.step_run line 27
12. lemma OAI.SourceBurnside.Structured.Binary.Decrement.pass_run line 44
13. lemma OAI.SourceBurnside.Structured.Binary.Decrement.scan_length line 60
14. lemma OAI.SourceBurnside.Structured.Binary.Decrement.program_run line 64
15. lemma OAI.SourceBurnside.Structured.Binary.Decrement.scan_equation line 79
16. lemma OAI.SourceBurnside.Structured.Binary.Decrement.scan_borrow line 88
17. lemma OAI.SourceBurnside.Structured.Binary.Decrement.scan_value line 94
18. lemma OAI.SourceBurnside.Structured.Device.last_value line 110
19. abbrev OAI.SourceBurnside.Structured.Device.Branch.Work line 121
20. abbrev OAI.SourceBurnside.Structured.Device.Branch.L line 122
21. def OAI.SourceBurnside.Structured.Device.Branch.flag line 124
22. def OAI.SourceBurnside.Structured.Device.Branch.out line 125
23. def OAI.SourceBurnside.Structured.Device.Branch.cond line 126
24. def OAI.SourceBurnside.Structured.Device.Branch.yes line 127
25. def OAI.SourceBurnside.Structured.Device.Branch.no line 130
26. lemma OAI.SourceBurnside.Structured.Device.Branch.cond_injective line 133
27. lemma OAI.SourceBurnside.Structured.Device.Branch.yes_injective line 136
28. lemma OAI.SourceBurnside.Structured.Device.Branch.no_injective line 144
29. def OAI.SourceBurnside.Structured.Device.Branch.body line 153
30. def OAI.SourceBurnside.Structured.Device.Branch.program line 155
31. def OAI.SourceBurnside.Structured.Device.Branch.pending line 157
32. lemma OAI.SourceBurnside.Structured.Device.Branch.finish_run line 159
33. lemma OAI.SourceBurnside.Structured.Device.Branch.branch_call line 177
34. lemma OAI.SourceBurnside.Structured.Device.Branch.body_run line 190
35. lemma OAI.SourceBurnside.Structured.Device.Branch.program_run line 207
36. def OAI.SourceBurnside.Structured.Device.Branch.realizer line 233
37. abbrev OAI.SourceBurnside.Structured.Binary.Power.K line 249
38. def OAI.SourceBurnside.Structured.Binary.Power.store line 251
39. def OAI.SourceBurnside.Structured.Binary.Power.trial line 252
40. def OAI.SourceBurnside.Structured.Binary.Power.regs line 253
41. lemma OAI.SourceBurnside.Structured.Binary.Power.regs_injective line 254
42. def OAI.SourceBurnside.Structured.Binary.Power.finish line 256
43. def OAI.SourceBurnside.Structured.Binary.Power.step line 257
44. def OAI.SourceBurnside.Structured.Binary.Power.program line 259
45. def OAI.SourceBurnside.Structured.Binary.Power.oneStep line 260
46. def OAI.SourceBurnside.Structured.Binary.Power.iter line 264
47. lemma OAI.SourceBurnside.Structured.Binary.Power.finish_run line 268
48. lemma OAI.SourceBurnside.Structured.Binary.Power.step_run line 286
49. lemma OAI.SourceBurnside.Structured.Binary.Power.oneStep_lengths line 319
50. lemma OAI.SourceBurnside.Structured.Binary.Power.iter_lengths line 326
51. lemma OAI.SourceBurnside.Structured.Binary.Power.program_run line 336
52. lemma OAI.SourceBurnside.Structured.Binary.Power.oneStep_counter line 354
53. lemma OAI.SourceBurnside.Structured.Binary.Power.oneStep_value line 361
54. lemma OAI.SourceBurnside.Structured.Binary.Power.iter_counter line 370
55. lemma OAI.SourceBurnside.Structured.Binary.Power.iter_value line 375
56. def OAI.SourceBurnside.Structured.Binary.one line 397
57. lemma OAI.SourceBurnside.Structured.Binary.one_run line 398
58. abbrev OAI.SourceBurnside.Structured.Device.PowerOperator.L line 419
59. def OAI.SourceBurnside.Structured.Device.PowerOperator.load line 421
60. def OAI.SourceBurnside.Structured.Device.PowerOperator.program line 424
61. def OAI.SourceBurnside.Structured.Device.PowerOperator.loaded line 425
62. lemma OAI.SourceBurnside.Structured.Device.PowerOperator.load_run line 428
63. lemma OAI.SourceBurnside.Structured.Device.PowerOperator.program_correct line 462
64. def OAI.SourceBurnside.Structured.Device.powerTwo line 507
65. def OAI.SourceBurnside.Structured.Device.Realizer.weaken line 524
66. def OAI.SourceBurnside.Structured.Device.Realizer.reinput line 534
67. def OAI.SourceBurnside.Structured.Device.composeUnary line 554
68. abbrev OAI.SourceBurnside.Structured.Binary.Increment.K line 566
69. def OAI.SourceBurnside.Structured.Binary.Increment.store line 568
70. def OAI.SourceBurnside.Structured.Binary.Increment.partialStore line 569
71. def OAI.SourceBurnside.Structured.Binary.Increment.low line 570
72. def OAI.SourceBurnside.Structured.Binary.Increment.carry line 571
73. lemma OAI.SourceBurnside.Structured.Binary.Increment.bit_equation line 572
74. def OAI.SourceBurnside.Structured.Binary.Increment.step line 575
75. def OAI.SourceBurnside.Structured.Binary.Increment.pass line 577
76. def OAI.SourceBurnside.Structured.Binary.Increment.program line 578
77. def OAI.SourceBurnside.Structured.Binary.Increment.scan line 579
78. lemma OAI.SourceBurnside.Structured.Binary.Increment.step_run line 583
79. lemma OAI.SourceBurnside.Structured.Binary.Increment.pass_run line 600
80. lemma OAI.SourceBurnside.Structured.Binary.Increment.scan_length line 616
81. lemma OAI.SourceBurnside.Structured.Binary.Increment.program_run line 620
82. lemma OAI.SourceBurnside.Structured.Binary.Increment.scan_equation line 635
83. lemma OAI.SourceBurnside.Structured.Binary.Increment.scan_value line 644
84. abbrev OAI.SourceBurnside.Structured.Binary.BitSize.K line 657
85. def OAI.SourceBurnside.Structured.Binary.BitSize.store line 659
86. def OAI.SourceBurnside.Structured.Binary.BitSize.trial line 660
87. def OAI.SourceBurnside.Structured.Binary.BitSize.regs line 661
88. lemma OAI.SourceBurnside.Structured.Binary.BitSize.regs_injective line 662
89. def OAI.SourceBurnside.Structured.Binary.BitSize.finish line 664
90. def OAI.SourceBurnside.Structured.Binary.BitSize.step line 665
91. def OAI.SourceBurnside.Structured.Binary.BitSize.program line 667
92. def OAI.SourceBurnside.Structured.Binary.BitSize.oneStep line 669
93. def OAI.SourceBurnside.Structured.Binary.BitSize.iter line 672
94. def OAI.SourceBurnside.Structured.Binary.BitSize.measure line 676
95. lemma OAI.SourceBurnside.Structured.Binary.BitSize.finish_run line 680
96. lemma OAI.SourceBurnside.Structured.Binary.BitSize.step_run line 699
97. lemma OAI.SourceBurnside.Structured.Binary.BitSize.oneStep_lengths line 730
98. lemma OAI.SourceBurnside.Structured.Binary.BitSize.iter_lengths line 733
99. lemma OAI.SourceBurnside.Structured.Binary.BitSize.program_run line 742
100. lemma OAI.SourceBurnside.Structured.Binary.BitSize.iter_value line 758
101. lemma OAI.SourceBurnside.Structured.Binary.BitSize.measure_value line 775
102. abbrev OAI.SourceBurnside.Structured.Device.SizeOperator.L line 796
103. def OAI.SourceBurnside.Structured.Device.SizeOperator.load line 798
104. def OAI.SourceBurnside.Structured.Device.SizeOperator.program line 802
105. def OAI.SourceBurnside.Structured.Device.SizeOperator.loaded line 803
106. lemma OAI.SourceBurnside.Structured.Device.SizeOperator.load_run line 806
107. lemma OAI.SourceBurnside.Structured.Device.SizeOperator.program_correct line 848
108. def OAI.SourceBurnside.Structured.Device.bitLength line 892
109. inductive OAI.SourceBurnside.Structured.Device.Formula line 904
110. def OAI.SourceBurnside.Structured.Device.Formula.eval line 919
111. def OAI.SourceBurnside.Structured.Device.Formula.Safe line 932
112. def OAI.SourceBurnside.Structured.Device.Formula.compile line 944
113. theorem OAI.SourceBurnside.Structured.Device.Formula.operational line 959