OAI/GroupTheory/PeriodicGroups/Formulas/BooleanCircuits.lean

GitHub source file

196 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourceBurnside.Structured.Device.Formula.equal line 13
2. def OAI.SourceBurnside.Structured.Device.Formula.less line 14
3. def OAI.SourceBurnside.Structured.Device.Formula.neg line 15
4. def OAI.SourceBurnside.Structured.Device.Formula.and line 16
5. def OAI.SourceBurnside.Structured.Device.Formula.or line 17
6. def OAI.SourceBurnside.Structured.Device.Formula.all line 18
7. def OAI.SourceBurnside.Structured.Device.Formula.any line 19
8. def OAI.SourceBurnside.Structured.Device.Formula.satSub line 21
9. def OAI.SourceBurnside.Structured.Device.Formula.field line 22
10. def OAI.SourceBurnside.Structured.Device.Formula.bitAt line 24
11. lemma OAI.SourceBurnside.Structured.Device.Formula.equal_eval line 26
12. lemma OAI.SourceBurnside.Structured.Device.Formula.less_eval line 33
13. lemma OAI.SourceBurnside.Structured.Device.Formula.neg_eval line 36
14. lemma OAI.SourceBurnside.Structured.Device.Formula.and_eval line 38
15. lemma OAI.SourceBurnside.Structured.Device.Formula.or_eval line 40
16. lemma OAI.SourceBurnside.Structured.Device.Formula.all_eval line 42
17. lemma OAI.SourceBurnside.Structured.Device.Formula.any_eval line 50
18. lemma OAI.SourceBurnside.Structured.Device.Formula.satSub_eval line 58
19. lemma OAI.SourceBurnside.Structured.Device.Formula.field_eval line 62
20. lemma OAI.SourceBurnside.Structured.Device.Formula.bool_all line 65
21. lemma OAI.SourceBurnside.Structured.Device.Formula.bool_any line 66
22. lemma OAI.SourceBurnside.Structured.Device.Formula.bool_equal line 67
23. lemma OAI.SourceBurnside.Structured.Device.Formula.bool_less line 68
24. lemma OAI.SourceBurnside.Structured.Device.Formula.bool_neg line 69
25. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_equal line 71
26. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_less line 77
27. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_neg line 84
28. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_and line 90
29. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_or line 94
30. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_all line 100
31. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_any line 106
32. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_satSub line 112
33. def OAI.SourceBurnside.Structured.Device.Formula.implies line 122
34. lemma OAI.SourceBurnside.Structured.Device.Formula.implies_eval line 123
35. lemma OAI.SourceBurnside.Structured.Device.Formula.implies_ne_zero line 125
36. lemma OAI.SourceBurnside.Structured.Device.Formula.bool_implies line 128
37. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_implies line 130
38. lemma OAI.SourceBurnside.Structured.Device.Formula.safe_field line 137
39. instance OAI.SourceBurnside.RawFormula.(instance at line 148) line 148
40. abbrev OAI.SourceBurnside.RawFormula.F line 149
41. def OAI.SourceBurnside.RawFormula.height line 150
42. def OAI.SourceBurnside.RawFormula.word line 151
43. def OAI.SourceBurnside.RawFormula.scale line 152
44. def OAI.SourceBurnside.RawFormula.slot line 153
45. def OAI.SourceBurnside.RawFormula.flag line 154
46. def OAI.SourceBurnside.RawFormula.bound line 155
47. def OAI.SourceBurnside.RawFormula.ranges line 157
48. def OAI.SourceBurnside.RawFormula.reservation line 164
49. def OAI.SourceBurnside.RawFormula.valid line 167
50. def OAI.SourceBurnside.RawFormula.inputs line 169
51. lemma OAI.SourceBurnside.RawFormula.height_eval line 170
52. lemma OAI.SourceBurnside.RawFormula.word_eval line 171
53. lemma OAI.SourceBurnside.RawFormula.scale_eval line 172
54. lemma OAI.SourceBurnside.RawFormula.slot_eval line 173
55. lemma OAI.SourceBurnside.RawFormula.bound_eval line 176
56. lemma OAI.SourceBurnside.RawFormula.ranges_eval line 178
57. lemma OAI.SourceBurnside.RawFormula.reservation_eval line 182
58. lemma OAI.SourceBurnside.RawFormula.valid_eval line 188
59. theorem OAI.SourceBurnside.RawFormula.accepts_iff_decode line 194
60. lemma OAI.SourceBurnside.RawFormula.valid_boolean line 199
61. lemma OAI.SourceBurnside.RawFormula.safe_constant line 201
62. lemma OAI.SourceBurnside.RawFormula.scale_safe line 208
63. lemma OAI.SourceBurnside.RawFormula.slots_safe line 214
64. lemma OAI.SourceBurnside.RawFormula.bound_safe line 223
65. lemma OAI.SourceBurnside.RawFormula.ranges_safe line 226
66. lemma OAI.SourceBurnside.RawFormula.reservation_safe line 246
67. theorem OAI.SourceBurnside.RawFormula.valid_safe line 264
68. def OAI.SourceBurnside.CellRepr.boolean line 272
69. lemma OAI.SourceBurnside.CellRepr.boolean_false line 273
70. lemma OAI.SourceBurnside.CellRepr.boolean_true line 274
71. lemma OAI.SourceBurnside.CellRepr.boolean_injective line 275
72. lemma OAI.SourceBurnside.CellRepr.boolean_eq_zero line 276
73. lemma OAI.SourceBurnside.CellRepr.boolean_eq_one line 277
74. lemma OAI.SourceBurnside.CellRepr.boolean_bit_zero line 278
75. lemma OAI.SourceBurnside.CellRepr.boolean_lt_two line 279
76. abbrev OAI.SourceBurnside.CellRepr.Record line 281
77. def OAI.SourceBurnside.CellRepr.cellRecord line 282
78. lemma OAI.SourceBurnside.CellRepr.repr_injective line 286
79. lemma OAI.SourceBurnside.CellRepr.repr_integer line 302
80. lemma OAI.SourceBurnside.CellRepr.repr_flag line 304
81. abbrev OAI.SourceBurnside.CellFormula.Expr line 312
82. def OAI.SourceBurnside.CellFormula.evaluate line 314
83. def OAI.SourceBurnside.CellFormula.ofRaw line 317
84. lemma OAI.SourceBurnside.CellFormula.ofRaw_represents line 322
85. def OAI.SourceBurnside.CellFormula.equalCells line 335
86. lemma OAI.SourceBurnside.CellFormula.equalCells_eval line 339
87. lemma OAI.SourceBurnside.CellFormula.equality_exact line 350
88. lemma OAI.SourceBurnside.CellFormula.equalCells_bool line 356
89. def OAI.SourceBurnside.CellFormula.wing line 359
90. def OAI.SourceBurnside.CellFormula.boundary line 362
91. def OAI.SourceBurnside.CellFormula.full line 365
92. def OAI.SourceBurnside.CellFormula.idle line 369
93. def OAI.SourceBurnside.CellFormula.setChecker line 372
94. def OAI.SourceBurnside.CellFormula.setColor line 374
95. lemma OAI.SourceBurnside.CellFormula.represent_int line 379
96. lemma OAI.SourceBurnside.CellFormula.represent_flag line 381
97. lemma OAI.SourceBurnside.CellFormula.wing_represents line 388
98. lemma OAI.SourceBurnside.CellFormula.boundary_represents line 393
99. lemma OAI.SourceBurnside.CellFormula.full_represents line 400
100. lemma OAI.SourceBurnside.CellFormula.idle_represents line 408
101. lemma OAI.SourceBurnside.CellFormula.setChecker_represents line 417
102. lemma OAI.SourceBurnside.CellFormula.setColor_represents line 425
103. lemma OAI.SourceBurnside.Structured.Device.Formula.constant_eval line 435
104. lemma OAI.SourceBurnside.Structured.Device.Formula.add_eval line 436
105. lemma OAI.SourceBurnside.Structured.Device.Formula.equal_ne_zero line 437
106. lemma OAI.SourceBurnside.Structured.Device.Formula.all_ne_zero line 439
107. lemma OAI.SourceBurnside.Structured.Device.Formula.any_ne_zero line 441
108. lemma OAI.SourceBurnside.Structured.Device.Formula.and_ne_zero line 443
109. lemma OAI.SourceBurnside.Structured.Device.Formula.or_ne_zero line 446
110. lemma OAI.SourceBurnside.Structured.Device.Formula.neg_ne_zero line 449
111. def OAI.SourceBurnside.CellFormula.first line 457
112. def OAI.SourceBurnside.CellFormula.last line 459
113. def OAI.SourceBurnside.CellFormula.hasMarker line 461
114. def OAI.SourceBurnside.CellFormula.hasPhase line 462
115. def OAI.SourceBurnside.CellFormula.isCore line 463
116. def OAI.SourceBurnside.CellFormula.isPalette line 464
117. def OAI.SourceBurnside.CellFormula.isStop line 465
118. def OAI.SourceBurnside.CellFormula.hasHead line 466
119. def OAI.SourceBurnside.CellFormula.endpoint line 467
120. def OAI.SourceBurnside.CellFormula.admissible line 469
121. def OAI.SourceBurnside.CellFormula.leftExternal line 472
122. def OAI.SourceBurnside.CellFormula.rightExternal line 474
123. def OAI.SourceBurnside.CellFormula.acceptsLeft line 476
124. def OAI.SourceBurnside.CellFormula.acceptsRight line 478
125. def OAI.SourceBurnside.CellFormula.structural line 480
126. def OAI.SourceBurnside.CellFormula.internal line 485
127. def OAI.SourceBurnside.CellFormula.skeletonPair line 489
128. lemma OAI.SourceBurnside.CellFormula.markerTag_injective line 493
129. lemma OAI.SourceBurnside.CellFormula.phaseTag_injective line 494
130. lemma OAI.SourceBurnside.CellFormula.first_exact line 499
131. lemma OAI.SourceBurnside.CellFormula.last_exact line 504
132. lemma OAI.SourceBurnside.CellFormula.marker_exact line 509
133. lemma OAI.SourceBurnside.CellFormula.phase_exact line 512
134. lemma OAI.SourceBurnside.CellFormula.core_exact line 515
135. lemma OAI.SourceBurnside.CellFormula.palette_exact line 518
136. lemma OAI.SourceBurnside.CellFormula.stop_exact line 521
137. lemma OAI.SourceBurnside.CellFormula.head_exact line 524
138. lemma OAI.SourceBurnside.CellFormula.endpoint_exact line 527
139. lemma OAI.SourceBurnside.CellFormula.admissible_exact line 529
140. lemma OAI.SourceBurnside.CellFormula.leftExternal_exact line 531
141. lemma OAI.SourceBurnside.CellFormula.rightExternal_exact line 534
142. lemma OAI.SourceBurnside.CellFormula.acceptsLeft_exact line 538
143. lemma OAI.SourceBurnside.CellFormula.acceptsRight_exact line 547
144. lemma OAI.SourceBurnside.CellFormula.structural_exact line 555
145. lemma OAI.SourceBurnside.CellFormula.internal_exact line 563
146. lemma OAI.SourceBurnside.CellFormula.skeletonPair_exact line 581
147. lemma OAI.SourceBurnside.CellRepr.bit_false_iff line 589
148. lemma OAI.SourceBurnside.CellRepr.bit_true_iff line 596
149. lemma OAI.SourceBurnside.CellRepr.boolean_bit_zero_iff line 603
150. lemma OAI.SourceBurnside.CellRepr.boolean_bit_one_iff line 604
151. lemma OAI.SourceBurnside.CellRepr.boolean_bit_add line 605
152. lemma OAI.SourceBurnside.Structured.Device.Formula.le_ne_zero line 612
153. lemma OAI.SourceBurnside.Structured.Device.Formula.less_ne_zero line 614
154. def OAI.SourceBurnside.CellFormula.regZero line 623
155. def OAI.SourceBurnside.CellFormula.headZero line 625
156. def OAI.SourceBurnside.CellFormula.metaZero line 627
157. def OAI.SourceBurnside.CellFormula.dataZero line 629
158. def OAI.SourceBurnside.CellFormula.checkerIdle line 631
159. def OAI.SourceBurnside.CellFormula.checkerPassed line 632
160. def OAI.SourceBurnside.CellFormula.checkerHead line 633
161. def OAI.SourceBurnside.CellFormula.headFree line 634
162. def OAI.SourceBurnside.CellFormula.coreLimit line 635
163. def OAI.SourceBurnside.CellFormula.formats line 637
164. def OAI.SourceBurnside.CellFormula.palettePair line 649
165. def OAI.SourceBurnside.CellFormula.checkerPair line 654
166. def OAI.SourceBurnside.CellFormula.pair line 657
167. lemma OAI.SourceBurnside.CellFormula.reg_zero_iff line 659
168. lemma OAI.SourceBurnside.CellFormula.data_zero_iff line 663
169. lemma OAI.SourceBurnside.CellFormula.meta_zero_iff line 667
170. lemma OAI.SourceBurnside.CellFormula.head_zero_iff line 677
171. lemma OAI.SourceBurnside.CellFormula.regZero_exact line 685
172. lemma OAI.SourceBurnside.CellFormula.dataZero_exact line 690
173. lemma OAI.SourceBurnside.CellFormula.metaZero_exact line 694
174. lemma OAI.SourceBurnside.CellFormula.headZero_exact line 697
175. lemma OAI.SourceBurnside.CellFormula.checkerIdle_exact line 702
176. lemma OAI.SourceBurnside.CellFormula.checkerPassed_exact line 705
177. lemma OAI.SourceBurnside.CellFormula.checkerHead_exact line 708
178. lemma OAI.SourceBurnside.CellFormula.headFree_exact line 711
179. lemma OAI.SourceBurnside.CellFormula.coreLimit_exact line 715
180. lemma OAI.SourceBurnside.CellFormula.formats_exact line 720
181. lemma OAI.SourceBurnside.CellFormula.check_pair_iff line 735
182. def OAI.SourceBurnside.CellFormula.passedOwn line 746
183. def OAI.SourceBurnside.CellFormula.duplicate line 748
184. def OAI.SourceBurnside.CellFormula.missing line 750
185. def OAI.SourceBurnside.CellFormula.semanticZero line 752
186. def OAI.SourceBurnside.CellFormula.unaryZero line 757
187. def OAI.SourceBurnside.CellFormula.binaryZero line 759
188. lemma OAI.SourceBurnside.CellFormula.palettePair_exact line 765
189. lemma OAI.SourceBurnside.CellFormula.checkerPair_exact line 775
190. lemma OAI.SourceBurnside.CellFormula.pair_exact line 780
191. lemma OAI.SourceBurnside.CellFormula.passedOwn_exact line 784
192. lemma OAI.SourceBurnside.CellFormula.duplicate_exact line 791
193. lemma OAI.SourceBurnside.CellFormula.missing_exact line 798
194. lemma OAI.SourceBurnside.CellFormula.semanticZero_exact line 807
195. lemma OAI.SourceBurnside.CellFormula.unaryZero_exact line 815
196. lemma OAI.SourceBurnside.CellFormula.binaryZero_exact line 822