OAI/Combinatorics/HoneycombChords/YangBaxterPolynomialsZero.lean

GitHub source file

254 declarations, 0 contain sorry, 0 declared as axioms

Yang–Baxter polynomial reductions with first spin zero.

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_101002_0 line 19
  2. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_1 line 22
  3. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_2 line 25
  4. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101002_3 line 29
  5. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_3 line 36
  6. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_4 line 39
  7. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101002_4 line 43
  8. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_5 line 50
  9. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_6 line 53
  10. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101002_0 line 57
  11. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_7 line 64
  12. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_8 line 67
  13. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101002_1 line 71
  14. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101002_9 line 78
  15. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101002_2 line 82
  16. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_101002 line 90
  17. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_0 line 98
  18. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_1 line 101
  19. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_2 line 104
  20. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101020_3 line 108
  21. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_3 line 115
  22. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_4 line 118
  23. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101020_4 line 122
  24. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_5 line 129
  25. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_6 line 132
  26. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101020_5 line 136
  27. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_7 line 143
  28. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_8 line 146
  29. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101020_0 line 150
  30. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_9 line 157
  31. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_10 line 160
  32. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101020_1 line 164
  33. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101020_11 line 171
  34. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101020_2 line 175
  35. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_101020 line 183
  36. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_0 line 192
  37. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_1 line 195
  38. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_2 line 198
  39. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101110_3 line 202
  40. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_3 line 209
  41. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_4 line 212
  42. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101110_4 line 216
  43. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_5 line 223
  44. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_6 line 226
  45. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101110_5 line 230
  46. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_7 line 237
  47. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_8 line 240
  48. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101110_0 line 244
  49. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_9 line 251
  50. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_10 line 254
  51. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101110_1 line 258
  52. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_101110_11 line 265
  53. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_101110_2 line 269
  54. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_101110 line 277
  55. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_0 line 286
  56. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_1 line 289
  57. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_2 line 292
  58. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_102111_3 line 296
  59. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_3 line 303
  60. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_4 line 306
  61. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_102111_4 line 310
  62. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_5 line 317
  63. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_6 line 320
  64. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_102111_5 line 324
  65. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_7 line 331
  66. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_8 line 334
  67. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_102111_0 line 338
  68. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_9 line 345
  69. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_10 line 348
  70. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_102111_1 line 352
  71. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_102111_11 line 359
  72. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_102111_2 line 363
  73. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_102111 line 371
  74. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_0 line 380
  75. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_1 line 383
  76. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_2 line 386
  77. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110002_3 line 390
  78. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_3 line 397
  79. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_4 line 400
  80. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110002_4 line 404
  81. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_5 line 411
  82. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_6 line 414
  83. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110002_5 line 418
  84. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_7 line 425
  85. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_8 line 428
  86. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110002_0 line 432
  87. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_9 line 439
  88. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_10 line 442
  89. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110002_1 line 446
  90. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110002_11 line 453
  91. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110002_2 line 457
  92. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_110002 line 465
  93. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_0 line 474
  94. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_1 line 477
  95. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_2 line 480
  96. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110011_3 line 484
  97. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_3 line 491
  98. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_4 line 494
  99. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110011_4 line 498
  100. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_5 line 505
  101. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_6 line 508
  102. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110011_5 line 512
  103. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_7 line 519
  104. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_8 line 522
  105. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110011_0 line 526
  106. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_9 line 533
  107. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_10 line 536
  108. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110011_1 line 540
  109. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110011_11 line 547
  110. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110011_2 line 551
  111. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_110011 line 559
  112. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_0 line 568
  113. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_1 line 571
  114. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_2 line 574
  115. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110020_3 line 578
  116. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_3 line 585
  117. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_4 line 588
  118. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110020_4 line 592
  119. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_5 line 599
  120. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_6 line 602
  121. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110020_5 line 606
  122. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_7 line 613
  123. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_8 line 616
  124. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110020_0 line 620
  125. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_9 line 627
  126. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_10 line 630
  127. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110020_1 line 634
  128. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_110020_11 line 641
  129. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_110020_2 line 645
  130. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_110020 line 653
  131. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_0 line 662
  132. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_1 line 665
  133. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_2 line 668
  134. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111012_3 line 672
  135. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_3 line 679
  136. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_4 line 682
  137. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111012_4 line 686
  138. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_5 line 693
  139. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_6 line 696
  140. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111012_0 line 700
  141. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_7 line 707
  142. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_8 line 710
  143. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111012_1 line 714
  144. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111012_9 line 721
  145. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111012_2 line 725
  146. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_111012 line 733
  147. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_0 line 741
  148. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_1 line 744
  149. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_2 line 747
  150. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111021_3 line 751
  151. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_3 line 758
  152. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_4 line 761
  153. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111021_4 line 765
  154. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_5 line 772
  155. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_6 line 775
  156. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111021_5 line 779
  157. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_7 line 786
  158. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_8 line 789
  159. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111021_0 line 793
  160. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_9 line 800
  161. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_10 line 803
  162. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111021_1 line 807
  163. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111021_11 line 814
  164. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111021_2 line 818
  165. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_111021 line 826
  166. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_0 line 835
  167. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_1 line 838
  168. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_2 line 841
  169. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111102_3 line 845
  170. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_3 line 852
  171. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_4 line 855
  172. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111102_4 line 859
  173. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_5 line 866
  174. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_6 line 869
  175. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111102_5 line 873
  176. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_7 line 880
  177. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_8 line 883
  178. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111102_0 line 887
  179. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_9 line 894
  180. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_10 line 897
  181. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111102_1 line 901
  182. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_111102_11 line 908
  183. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_111102_2 line 912
  184. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_111102 line 920
  185. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_0 line 929
  186. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_1 line 932
  187. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_2 line 935
  188. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_112022_3 line 939
  189. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_3 line 946
  190. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_4 line 949
  191. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_112022_4 line 953
  192. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_5 line 960
  193. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_6 line 963
  194. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_112022_0 line 967
  195. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_7 line 974
  196. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_8 line 977
  197. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_112022_1 line 981
  198. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_112022_9 line 988
  199. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_112022_2 line 992
  200. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_112022 line 1000
  201. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_0 line 1008
  202. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_1 line 1011
  203. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_2 line 1014
  204. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120012_3 line 1018
  205. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_3 line 1025
  206. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_4 line 1028
  207. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120012_4 line 1032
  208. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_5 line 1039
  209. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_6 line 1042
  210. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120012_5 line 1046
  211. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_7 line 1053
  212. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_8 line 1056
  213. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120012_0 line 1060
  214. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_9 line 1067
  215. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_10 line 1070
  216. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120012_1 line 1074
  217. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120012_11 line 1081
  218. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120012_2 line 1085
  219. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_120012 line 1093
  220. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_0 line 1102
  221. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_1 line 1105
  222. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_2 line 1108
  223. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120021_3 line 1112
  224. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_3 line 1119
  225. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_4 line 1122
  226. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120021_4 line 1126
  227. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_5 line 1133
  228. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_6 line 1136
  229. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120021_5 line 1140
  230. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_7 line 1147
  231. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_8 line 1150
  232. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120021_0 line 1154
  233. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_9 line 1161
  234. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_10 line 1164
  235. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120021_1 line 1168
  236. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_120021_11 line 1175
  237. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_120021_2 line 1179
  238. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_120021 line 1187
  239. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_0 line 1196
  240. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_1 line 1199
  241. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_2 line 1202
  242. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_121022_3 line 1206
  243. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_3 line 1213
  244. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_4 line 1216
  245. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_121022_4 line 1220
  246. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_5 line 1227
  247. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_6 line 1230
  248. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_121022_0 line 1234
  249. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_7 line 1241
  250. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_8 line 1244
  251. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_121022_1 line 1248
  252. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_121022_9 line 1255
  253. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_121022_2 line 1259
  254. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_121022 line 1267