OAI/Combinatorics/HoneycombChords/YangBaxterNegative.lean

GitHub source file

252 declarations, 0 contain sorry, 0 declared as axioms

Yang–Baxter components with first spin negative.

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

  1. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200002 line 24
  2. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200011 line 33
  3. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201012 line 42
  4. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200020 line 51
  5. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200101 line 60
  6. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200110 line 69
  7. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201102 line 78
  8. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201111 line 87
  9. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201120 line 96
  10. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201210 line 105
  11. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202022 line 114
  12. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202112 line 123
  13. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202121 line 132
  14. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202202 line 141
  15. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202211 line 150
  16. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202220 line 159
  17. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210021 line 168
  18. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210102 line 177
  19. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210111 line 186
  20. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210120 line 195
  21. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210201 line 204
  22. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211022 line 213
  23. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211112 line 222
  24. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211121 line 231
  25. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211202 line 240
  26. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211220 line 249
  27. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212221 line 258
  28. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220022 line 267
  29. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220112 line 276
  30. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220121 line 285
  31. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220202 line 294
  32. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220211 line 303
  33. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221122 line 312
  34. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221212 line 321
  35. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200000 line 329
  36. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200001 line 335
  37. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200010 line 341
  38. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200012 line 347
  39. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200021 line 353
  40. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200022 line 359
  41. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200100 line 365
  42. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200102 line 371
  43. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200111 line 377
  44. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200112 line 383
  45. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200120 line 389
  46. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200121 line 395
  47. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200122 line 401
  48. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200200 line 407
  49. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200201 line 413
  50. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200202 line 419
  51. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200210 line 425
  52. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200211 line 431
  53. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200212 line 437
  54. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200220 line 443
  55. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200221 line 449
  56. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_200222 line 455
  57. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201000 line 461
  58. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201001 line 467
  59. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201002 line 473
  60. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201010 line 479
  61. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201011 line 485
  62. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201020 line 491
  63. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201021 line 497
  64. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201022 line 503
  65. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201100 line 509
  66. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201101 line 515
  67. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201110 line 521
  68. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201112 line 527
  69. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201121 line 533
  70. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201122 line 539
  71. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201200 line 545
  72. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201201 line 551
  73. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201202 line 557
  74. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201211 line 563
  75. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201212 line 569
  76. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201220 line 575
  77. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201221 line 581
  78. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_201222 line 587
  79. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202000 line 593
  80. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202001 line 599
  81. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202002 line 605
  82. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202010 line 611
  83. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202011 line 617
  84. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202012 line 623
  85. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202020 line 629
  86. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202021 line 635
  87. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202100 line 641
  88. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202101 line 647
  89. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202102 line 653
  90. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202110 line 659
  91. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202111 line 665
  92. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202120 line 671
  93. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202122 line 677
  94. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202200 line 683
  95. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202201 line 689
  96. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202210 line 695
  97. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202212 line 701
  98. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202221 line 707
  99. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_202222 line 713
  100. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210000 line 719
  101. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210001 line 725
  102. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210002 line 731
  103. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210010 line 737
  104. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210011 line 743
  105. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210012 line 749
  106. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210020 line 755
  107. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210022 line 761
  108. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210100 line 767
  109. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210101 line 773
  110. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210110 line 779
  111. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210112 line 785
  112. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210121 line 791
  113. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210122 line 797
  114. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210200 line 803
  115. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210202 line 809
  116. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210210 line 815
  117. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210211 line 821
  118. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210212 line 827
  119. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210220 line 833
  120. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210221 line 839
  121. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_210222 line 845
  122. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211000 line 851
  123. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211001 line 857
  124. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211002 line 863
  125. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211010 line 869
  126. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211011 line 875
  127. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211012 line 881
  128. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211020 line 887
  129. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211021 line 893
  130. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211100 line 899
  131. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211101 line 905
  132. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211102 line 911
  133. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211110 line 917
  134. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211111 line 923
  135. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211120 line 929
  136. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211122 line 935
  137. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211200 line 941
  138. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211201 line 947
  139. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211210 line 953
  140. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211211 line 959
  141. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211212 line 965
  142. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211221 line 971
  143. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_211222 line 977
  144. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212000 line 983
  145. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212001 line 989
  146. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212002 line 995
  147. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212010 line 1001
  148. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212011 line 1007
  149. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212012 line 1013
  150. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212020 line 1019
  151. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212021 line 1025
  152. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212022 line 1031
  153. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212100 line 1037
  154. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212101 line 1043
  155. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212102 line 1049
  156. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212110 line 1055
  157. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212111 line 1061
  158. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212112 line 1067
  159. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212120 line 1073
  160. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212121 line 1079
  161. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212122 line 1085
  162. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212200 line 1091
  163. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212201 line 1097
  164. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212202 line 1103
  165. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212210 line 1109
  166. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212211 line 1115
  167. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212212 line 1121
  168. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212220 line 1127
  169. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_212222 line 1133
  170. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220000 line 1139
  171. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220001 line 1145
  172. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220002 line 1151
  173. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220010 line 1157
  174. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220011 line 1163
  175. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220012 line 1169
  176. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220020 line 1175
  177. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220021 line 1181
  178. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220100 line 1187
  179. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220101 line 1193
  180. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220102 line 1199
  181. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220110 line 1205
  182. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220111 line 1211
  183. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220120 line 1217
  184. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220122 line 1223
  185. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220200 line 1229
  186. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220201 line 1235
  187. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220210 line 1241
  188. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220212 line 1247
  189. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220220 line 1253
  190. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220221 line 1259
  191. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_220222 line 1265
  192. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221000 line 1271
  193. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221001 line 1277
  194. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221002 line 1283
  195. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221010 line 1289
  196. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221011 line 1295
  197. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221012 line 1301
  198. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221020 line 1307
  199. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221021 line 1313
  200. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221022 line 1319
  201. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221100 line 1325
  202. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221101 line 1331
  203. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221102 line 1337
  204. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221110 line 1343
  205. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221111 line 1349
  206. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221112 line 1355
  207. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221120 line 1361
  208. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221121 line 1367
  209. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221200 line 1373
  210. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221201 line 1379
  211. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221202 line 1385
  212. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221210 line 1391
  213. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221211 line 1397
  214. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221220 line 1403
  215. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221221 line 1409
  216. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_221222 line 1415
  217. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222000 line 1421
  218. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222001 line 1427
  219. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222002 line 1433
  220. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222010 line 1439
  221. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222011 line 1445
  222. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222012 line 1451
  223. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222020 line 1457
  224. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222021 line 1463
  225. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222022 line 1469
  226. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222100 line 1475
  227. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222101 line 1481
  228. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222102 line 1487
  229. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222110 line 1493
  230. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222111 line 1499
  231. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222112 line 1505
  232. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222120 line 1511
  233. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222121 line 1517
  234. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222122 line 1523
  235. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222200 line 1529
  236. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222201 line 1535
  237. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222202 line 1541
  238. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222210 line 1547
  239. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222211 line 1553
  240. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222212 line 1559
  241. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222220 line 1565
  242. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222221 line 1571
  243. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_222222 line 1577
  244. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_200 line 1584
  245. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_201 line 1617
  246. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_202 line 1650
  247. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_210 line 1683
  248. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_211 line 1716
  249. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_212 line 1749
  250. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_220 line 1782
  251. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_221 line 1815
  252. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_222 line 1847