OAI/Combinatorics/HoneycombChords/BulkFusionEquation.lean

GitHub source file

305 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.qNumerator line 12
2. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionLeft line 13
3. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionRight line 17
4. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkNumerator_eq_zero_of_sum_ne line 21
5. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionNumerator_eq_zero_of_sum_ne line 27
6. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionLeft_eq_zero_of_sum_ne line 32
7. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionRight_eq_zero_of_sum_ne line 52
8. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionAdd line 64
9. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionMul line 65
10. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionPow line 66
11. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00000 line 70
12. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00001 line 74
13. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00002 line 78
14. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00010 line 82
15. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00011 line 86
16. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00012 line 90
17. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00020 line 94
18. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00021 line 98
19. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00022 line 102
20. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate00100 line 106
21. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00100 line 109
22. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00101 line 115
23. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00102 line 119
24. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00110 line 123
25. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00111 line 127
26. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00112 line 131
27. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00120 line 135
28. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00121 line 139
29. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00122 line 143
30. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00200 line 147
31. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate00201 line 151
32. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00201 line 154
33. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00202 line 160
34. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate00210 line 164
35. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00210 line 167
36. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00211 line 173
37. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00212 line 177
38. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00220 line 181
39. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00221 line 185
40. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent00222 line 189
41. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate01000 line 193
42. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01000 line 196
43. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01001 line 202
44. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01002 line 206
45. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01010 line 210
46. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01011 line 214
47. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01012 line 218
48. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01020 line 222
49. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01021 line 226
50. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01022 line 230
51. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01100 line 234
52. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate01101 line 238
53. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01101 line 241
54. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01102 line 247
55. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate01110 line 251
56. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01110 line 254
57. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01111 line 260
58. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01112 line 264
59. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01120 line 268
60. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01121 line 272
61. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01122 line 276
62. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01200 line 280
63. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01201 line 284
64. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate01202 line 288
65. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01202 line 291
66. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01210 line 297
67. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate01211 line 301
68. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01211 line 304
69. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01212 line 310
70. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate01220 line 314
71. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01220 line 317
72. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01221 line 323
73. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent01222 line 327
74. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02000 line 331
75. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02001 line 335
76. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02001 line 338
77. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02002 line 344
78. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02010 line 348
79. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02010 line 351
80. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02011 line 357
81. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02012 line 361
82. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02020 line 365
83. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02021 line 369
84. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02022 line 373
85. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02100 line 377
86. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02101 line 381
87. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02102 line 385
88. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02102 line 388
89. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02110 line 394
90. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02111 line 398
91. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02111 line 401
92. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02112 line 407
93. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02120 line 411
94. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02120 line 414
95. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02121 line 420
96. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02122 line 424
97. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02200 line 428
98. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02201 line 432
99. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02202 line 436
100. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02210 line 440
101. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02211 line 444
102. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02212 line 448
103. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02212 line 451
104. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02220 line 457
105. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate02221 line 461
106. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02221 line 464
107. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent02222 line 470
108. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate10000 line 474
109. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10000 line 477
110. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10001 line 483
111. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10002 line 487
112. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10010 line 491
113. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10011 line 495
114. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10012 line 499
115. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10020 line 503
116. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10021 line 507
117. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10022 line 511
118. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10100 line 515
119. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate10101 line 519
120. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10101 line 522
121. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10102 line 528
122. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate10110 line 532
123. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10110 line 535
124. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10111 line 541
125. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10112 line 545
126. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10120 line 549
127. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10121 line 553
128. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10122 line 557
129. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10200 line 561
130. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10201 line 565
131. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate10202 line 569
132. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10202 line 572
133. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10210 line 578
134. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate10211 line 582
135. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10211 line 585
136. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10212 line 591
137. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate10220 line 595
138. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10220 line 598
139. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10221 line 604
140. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent10222 line 608
141. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11000 line 612
142. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11001 line 616
143. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11001 line 619
144. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11002 line 625
145. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11010 line 629
146. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11010 line 632
147. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11011 line 638
148. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11012 line 642
149. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11020 line 646
150. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11021 line 650
151. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11022 line 654
152. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11100 line 658
153. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11101 line 662
154. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11102 line 666
155. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11102 line 669
156. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11110 line 675
157. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11111 line 679
158. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11111 line 682
159. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11112 line 688
160. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11120 line 692
161. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11120 line 695
162. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11121 line 701
163. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11122 line 705
164. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11200 line 709
165. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11201 line 713
166. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11202 line 717
167. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11210 line 721
168. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11211 line 725
169. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11212 line 729
170. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11212 line 732
171. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11220 line 738
172. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate11221 line 742
173. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11221 line 745
174. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent11222 line 751
175. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12000 line 755
176. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12001 line 759
177. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate12002 line 763
178. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12002 line 766
179. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12010 line 772
180. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate12011 line 776
181. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12011 line 779
182. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12012 line 785
183. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate12020 line 789
184. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12020 line 792
185. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12021 line 798
186. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12022 line 802
187. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12100 line 806
188. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12101 line 810
189. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12102 line 814
190. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12110 line 818
191. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12111 line 822
192. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate12112 line 826
193. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12112 line 829
194. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12120 line 835
195. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate12121 line 839
196. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12121 line 842
197. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12122 line 848
198. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12200 line 852
199. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12201 line 856
200. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12202 line 860
201. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12210 line 864
202. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12211 line 868
203. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12212 line 872
204. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12220 line 876
205. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12221 line 880
206. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate12222 line 884
207. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent12222 line 887
208. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20000 line 893
209. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20001 line 897
210. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20001 line 900
211. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20002 line 906
212. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20010 line 910
213. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20010 line 913
214. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20011 line 919
215. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20012 line 923
216. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20020 line 927
217. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20021 line 931
218. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20022 line 935
219. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20100 line 939
220. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20101 line 943
221. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20102 line 947
222. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20102 line 950
223. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20110 line 956
224. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20111 line 960
225. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20111 line 963
226. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20112 line 969
227. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20120 line 973
228. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20120 line 976
229. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20121 line 982
230. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20122 line 986
231. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20200 line 990
232. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20201 line 994
233. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20202 line 998
234. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20210 line 1002
235. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20211 line 1006
236. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20212 line 1010
237. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20212 line 1013
238. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20220 line 1019
239. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate20221 line 1023
240. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20221 line 1026
241. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent20222 line 1032
242. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21000 line 1036
243. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21001 line 1040
244. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate21002 line 1044
245. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21002 line 1047
246. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21010 line 1053
247. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate21011 line 1057
248. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21011 line 1060
249. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21012 line 1066
250. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate21020 line 1070
251. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21020 line 1073
252. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21021 line 1079
253. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21022 line 1083
254. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21100 line 1087
255. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21101 line 1091
256. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21102 line 1095
257. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21110 line 1099
258. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21111 line 1103
259. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate21112 line 1107
260. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21112 line 1110
261. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21120 line 1116
262. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate21121 line 1120
263. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21121 line 1123
264. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21122 line 1129
265. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21200 line 1133
266. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21201 line 1137
267. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21202 line 1141
268. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21210 line 1145
269. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21211 line 1149
270. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21212 line 1153
271. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21220 line 1157
272. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21221 line 1161
273. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate21222 line 1165
274. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent21222 line 1168
275. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22000 line 1174
276. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22001 line 1178
277. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22002 line 1182
278. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22010 line 1186
279. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22011 line 1190
280. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate22012 line 1194
281. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22012 line 1197
282. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22020 line 1203
283. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate22021 line 1207
284. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22021 line 1210
285. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22022 line 1216
286. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22100 line 1220
287. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22101 line 1224
288. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22102 line 1228
289. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22110 line 1232
290. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22111 line 1236
291. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22112 line 1240
292. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22120 line 1244
293. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22121 line 1248
294. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkCertificate22122 line 1252
295. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22122 line 1255
296. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22200 line 1261
297. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22201 line 1265
298. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22202 line 1269
299. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22210 line 1273
300. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22211 line 1277
301. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22212 line 1281
302. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22220 line 1285
303. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22221 line 1289
304. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkFusionBulkComponent22222 line 1293
305. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulk_fusion_numerator line 1298