OAI/Combinatorics/HoneycombChords/YangBaxterPolynomialsPositive.lean

GitHub source file

458 declarations, 0 contain sorry, 0 declared as axioms

Yang–Baxter polynomial reductions with first spin positive.

This development follows the finite strip transfer calculation for critical honeycomb walks in the companion paper on uniform marked polygon estimates.

  1. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001010_0 line 19
  2. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001010_1 line 22
  3. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_001010_3 line 26
  4. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_001010 line 34
  5. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_0 line 38
  6. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_1 line 41
  7. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_2 line 44
  8. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_001100_3 line 48
  9. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_3 line 55
  10. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_4 line 58
  11. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_001100_4 line 62
  12. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_5 line 69
  13. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_6 line 72
  14. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_001100_0 line 76
  15. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_7 line 83
  16. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_8 line 86
  17. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_001100_1 line 90
  18. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_001100_9 line 97
  19. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_001100_2 line 101
  20. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_001100 line 109
  21. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_0 line 117
  22. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_1 line 120
  23. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_2 line 123
  24. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002011_3 line 127
  25. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_3 line 134
  26. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_4 line 137
  27. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002011_4 line 141
  28. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_5 line 148
  29. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_6 line 151
  30. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002011_0 line 155
  31. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_7 line 162
  32. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_8 line 165
  33. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002011_1 line 169
  34. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002011_9 line 176
  35. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002011_2 line 180
  36. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_002011 line 188
  37. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_0 line 196
  38. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_1 line 199
  39. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_2 line 202
  40. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002020_3 line 206
  41. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_3 line 213
  42. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_4 line 216
  43. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002020_4 line 220
  44. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_5 line 227
  45. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_6 line 230
  46. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002020_5 line 234
  47. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_7 line 241
  48. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_8 line 244
  49. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002020_0 line 248
  50. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_9 line 255
  51. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_10 line 258
  52. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002020_1 line 262
  53. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002020_11 line 269
  54. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002020_2 line 273
  55. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_002020 line 281
  56. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_0 line 290
  57. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_1 line 293
  58. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_2 line 296
  59. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002101_3 line 300
  60. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_3 line 307
  61. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_4 line 310
  62. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002101_4 line 314
  63. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_5 line 321
  64. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_6 line 324
  65. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002101_0 line 328
  66. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_7 line 335
  67. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_8 line 338
  68. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002101_1 line 342
  69. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002101_9 line 349
  70. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002101_2 line 353
  71. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_002101 line 361
  72. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_0 line 369
  73. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_1 line 372
  74. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_2 line 375
  75. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002110_3 line 379
  76. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_3 line 386
  77. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_4 line 389
  78. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002110_4 line 393
  79. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_5 line 400
  80. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_6 line 403
  81. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002110_5 line 407
  82. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_7 line 414
  83. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_8 line 417
  84. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002110_0 line 421
  85. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_9 line 428
  86. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_10 line 431
  87. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002110_1 line 435
  88. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002110_11 line 442
  89. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002110_2 line 446
  90. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_002110 line 454
  91. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_0 line 463
  92. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_1 line 466
  93. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_2 line 469
  94. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002200_3 line 473
  95. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_3 line 480
  96. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_4 line 483
  97. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002200_4 line 487
  98. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_5 line 494
  99. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_6 line 497
  100. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002200_5 line 501
  101. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_7 line 508
  102. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_8 line 511
  103. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002200_0 line 515
  104. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_9 line 522
  105. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_10 line 525
  106. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002200_1 line 529
  107. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_002200_11 line 536
  108. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_002200_2 line 540
  109. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_002200 line 548
  110. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_0 line 557
  111. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_1 line 560
  112. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_2 line 563
  113. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011002_3 line 567
  114. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_3 line 574
  115. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_4 line 577
  116. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011002_4 line 581
  117. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_5 line 588
  118. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_6 line 591
  119. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011002_0 line 595
  120. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_7 line 602
  121. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_8 line 605
  122. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011002_1 line 609
  123. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011002_9 line 616
  124. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011002_2 line 620
  125. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_011002 line 628
  126. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_0 line 636
  127. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_1 line 639
  128. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_2 line 642
  129. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011020_3 line 646
  130. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_3 line 653
  131. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_4 line 656
  132. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011020_4 line 660
  133. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_5 line 667
  134. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_6 line 670
  135. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011020_5 line 674
  136. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_7 line 681
  137. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_8 line 684
  138. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011020_0 line 688
  139. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_9 line 695
  140. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_10 line 698
  141. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011020_1 line 702
  142. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011020_11 line 709
  143. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011020_2 line 713
  144. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_011020 line 721
  145. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_0 line 730
  146. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_1 line 733
  147. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_2 line 736
  148. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011101_3 line 740
  149. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_3 line 747
  150. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_4 line 750
  151. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011101_4 line 754
  152. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_5 line 761
  153. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_6 line 764
  154. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011101_5 line 768
  155. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_7 line 775
  156. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_8 line 778
  157. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011101_0 line 782
  158. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_9 line 789
  159. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_10 line 792
  160. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011101_1 line 796
  161. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011101_11 line 803
  162. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011101_2 line 807
  163. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_011101 line 815
  164. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_0 line 824
  165. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_1 line 827
  166. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_2 line 830
  167. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011110_3 line 834
  168. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_3 line 841
  169. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_4 line 844
  170. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011110_4 line 848
  171. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_5 line 855
  172. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_6 line 858
  173. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011110_5 line 862
  174. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_7 line 869
  175. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_8 line 872
  176. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011110_0 line 876
  177. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_9 line 883
  178. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_10 line 886
  179. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011110_1 line 890
  180. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011110_11 line 897
  181. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011110_2 line 901
  182. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_011110 line 909
  183. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_0 line 918
  184. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_1 line 921
  185. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_2 line 924
  186. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011200_3 line 928
  187. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_3 line 935
  188. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_4 line 938
  189. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011200_4 line 942
  190. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_5 line 949
  191. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_6 line 952
  192. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011200_5 line 956
  193. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_7 line 963
  194. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_8 line 966
  195. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011200_0 line 970
  196. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_9 line 977
  197. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_10 line 980
  198. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011200_1 line 984
  199. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_011200_11 line 991
  200. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_011200_2 line 995
  201. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_011200 line 1003
  202. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_0 line 1012
  203. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_1 line 1015
  204. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_2 line 1018
  205. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012021_3 line 1022
  206. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_3 line 1029
  207. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_4 line 1032
  208. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012021_4 line 1036
  209. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_5 line 1043
  210. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_6 line 1046
  211. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012021_5 line 1050
  212. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_7 line 1057
  213. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_8 line 1060
  214. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012021_0 line 1064
  215. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_9 line 1071
  216. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_10 line 1074
  217. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012021_1 line 1078
  218. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012021_11 line 1085
  219. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012021_2 line 1089
  220. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_012021 line 1097
  221. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_0 line 1106
  222. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_1 line 1109
  223. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_2 line 1112
  224. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012102_3 line 1116
  225. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_3 line 1123
  226. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_4 line 1126
  227. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012102_4 line 1130
  228. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_5 line 1137
  229. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_6 line 1140
  230. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012102_5 line 1144
  231. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_7 line 1151
  232. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_8 line 1154
  233. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012102_0 line 1158
  234. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_9 line 1165
  235. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_10 line 1168
  236. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012102_1 line 1172
  237. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012102_11 line 1179
  238. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012102_2 line 1183
  239. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_012102 line 1191
  240. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_0 line 1200
  241. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_1 line 1203
  242. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_2 line 1206
  243. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012111_3 line 1210
  244. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_3 line 1217
  245. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_4 line 1220
  246. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012111_4 line 1224
  247. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_5 line 1231
  248. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_6 line 1234
  249. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012111_0 line 1238
  250. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_7 line 1245
  251. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_8 line 1248
  252. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012111_1 line 1252
  253. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012111_9 line 1259
  254. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012111_2 line 1263
  255. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_012111 line 1271
  256. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_0 line 1279
  257. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_1 line 1282
  258. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_2 line 1285
  259. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012120_3 line 1289
  260. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_3 line 1296
  261. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_4 line 1299
  262. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012120_4 line 1303
  263. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_5 line 1310
  264. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_6 line 1313
  265. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012120_5 line 1317
  266. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_7 line 1324
  267. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_8 line 1327
  268. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012120_0 line 1331
  269. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_9 line 1338
  270. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_10 line 1341
  271. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012120_1 line 1345
  272. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012120_11 line 1352
  273. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012120_2 line 1356
  274. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_012120 line 1364
  275. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_0 line 1373
  276. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_1 line 1376
  277. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_2 line 1379
  278. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012201_3 line 1383
  279. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_3 line 1390
  280. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_4 line 1393
  281. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012201_4 line 1397
  282. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_5 line 1404
  283. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_6 line 1407
  284. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012201_5 line 1411
  285. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_7 line 1418
  286. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_8 line 1421
  287. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012201_0 line 1425
  288. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_9 line 1432
  289. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_10 line 1435
  290. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012201_1 line 1439
  291. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_012201_11 line 1446
  292. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_012201_2 line 1450
  293. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_012201 line 1458
  294. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_0 line 1467
  295. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_1 line 1470
  296. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_2 line 1473
  297. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020011_3 line 1477
  298. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_3 line 1484
  299. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_4 line 1487
  300. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020011_4 line 1491
  301. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_5 line 1498
  302. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_6 line 1501
  303. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020011_5 line 1505
  304. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_7 line 1512
  305. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_8 line 1515
  306. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020011_0 line 1519
  307. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_9 line 1526
  308. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_10 line 1529
  309. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020011_1 line 1533
  310. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020011_11 line 1540
  311. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020011_2 line 1544
  312. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_020011 line 1552
  313. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_0 line 1561
  314. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_1 line 1564
  315. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_2 line 1567
  316. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020020_3 line 1571
  317. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_3 line 1578
  318. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_4 line 1581
  319. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020020_4 line 1585
  320. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_5 line 1592
  321. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_6 line 1595
  322. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020020_5 line 1599
  323. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_7 line 1606
  324. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_8 line 1609
  325. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020020_0 line 1613
  326. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_9 line 1620
  327. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_10 line 1623
  328. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020020_1 line 1627
  329. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020020_11 line 1634
  330. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020020_2 line 1638
  331. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_020020 line 1646
  332. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_0 line 1655
  333. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_1 line 1658
  334. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_2 line 1661
  335. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020101_3 line 1665
  336. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_3 line 1672
  337. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_4 line 1675
  338. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020101_4 line 1679
  339. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_5 line 1686
  340. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_6 line 1689
  341. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020101_5 line 1693
  342. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_7 line 1700
  343. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_8 line 1703
  344. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020101_0 line 1707
  345. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_9 line 1714
  346. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_10 line 1717
  347. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020101_1 line 1721
  348. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020101_11 line 1728
  349. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020101_2 line 1732
  350. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_020101 line 1740
  351. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_0 line 1749
  352. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_1 line 1752
  353. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_2 line 1755
  354. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020110_3 line 1759
  355. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_3 line 1766
  356. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_4 line 1769
  357. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020110_4 line 1773
  358. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_5 line 1780
  359. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_6 line 1783
  360. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020110_5 line 1787
  361. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_7 line 1794
  362. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_8 line 1797
  363. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020110_0 line 1801
  364. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_9 line 1808
  365. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_10 line 1811
  366. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020110_1 line 1815
  367. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_020110_11 line 1822
  368. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_020110_2 line 1826
  369. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_020110 line 1834
  370. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_0 line 1843
  371. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_1 line 1846
  372. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_2 line 1849
  373. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021102_3 line 1853
  374. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_3 line 1860
  375. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_4 line 1863
  376. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021102_4 line 1867
  377. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_5 line 1874
  378. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_6 line 1877
  379. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021102_5 line 1881
  380. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_7 line 1888
  381. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_8 line 1891
  382. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021102_0 line 1895
  383. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_9 line 1902
  384. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_10 line 1905
  385. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021102_1 line 1909
  386. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021102_11 line 1916
  387. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021102_2 line 1920
  388. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_021102 line 1928
  389. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_0 line 1937
  390. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_1 line 1940
  391. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_2 line 1943
  392. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021111_3 line 1947
  393. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_3 line 1954
  394. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_4 line 1957
  395. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021111_4 line 1961
  396. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_5 line 1968
  397. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_6 line 1971
  398. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021111_5 line 1975
  399. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_7 line 1982
  400. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_8 line 1985
  401. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021111_0 line 1989
  402. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_9 line 1996
  403. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_10 line 1999
  404. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021111_1 line 2003
  405. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021111_11 line 2010
  406. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021111_2 line 2014
  407. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_021111 line 2022
  408. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_0 line 2031
  409. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_1 line 2034
  410. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_2 line 2037
  411. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021120_3 line 2041
  412. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_3 line 2048
  413. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_4 line 2051
  414. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021120_4 line 2055
  415. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_5 line 2062
  416. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_6 line 2065
  417. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021120_5 line 2069
  418. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_7 line 2076
  419. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_8 line 2079
  420. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021120_0 line 2083
  421. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_9 line 2090
  422. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_10 line 2093
  423. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021120_1 line 2097
  424. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_021120_11 line 2104
  425. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_021120_2 line 2108
  426. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_021120 line 2116
  427. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_0 line 2125
  428. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_1 line 2128
  429. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_2 line 2131
  430. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022112_3 line 2135
  431. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_3 line 2142
  432. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_4 line 2145
  433. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022112_4 line 2149
  434. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_5 line 2156
  435. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_6 line 2159
  436. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022112_0 line 2163
  437. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_7 line 2170
  438. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_8 line 2173
  439. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022112_1 line 2177
  440. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022112_9 line 2184
  441. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022112_2 line 2188
  442. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_022112 line 2196
  443. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_0 line 2204
  444. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_1 line 2207
  445. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_2 line 2210
  446. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022121_3 line 2214
  447. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_3 line 2221
  448. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_4 line 2224
  449. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022121_4 line 2228
  450. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_5 line 2235
  451. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_6 line 2238
  452. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022121_0 line 2242
  453. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_7 line 2249
  454. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_8 line 2252
  455. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022121_1 line 2256
  456. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_022121_9 line 2263
  457. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_022121_2 line 2267
  458. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_022121 line 2275