OAI/Combinatorics/Sidorenko/Refinement.lean

GitHub source file

316 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.refineLeft0 line 10
  2. def OAI.SidorenkoCounterexample.refineRight0 line 11
  3. def OAI.SidorenkoCounterexample.refineLeft1 line 12
  4. def OAI.SidorenkoCounterexample.refineRight1 line 13
  5. def OAI.SidorenkoCounterexample.refineLeft2 line 14
  6. def OAI.SidorenkoCounterexample.refineRight2 line 15
  7. def OAI.SidorenkoCounterexample.refineLeft3 line 16
  8. def OAI.SidorenkoCounterexample.refineRight3 line 17
  9. def OAI.SidorenkoCounterexample.refineLeft4 line 18
  10. def OAI.SidorenkoCounterexample.refineRight4 line 19
  11. def OAI.SidorenkoCounterexample.histLeft0 line 20
  12. lemma OAI.SidorenkoCounterexample.histLeft0_0 line 21
  13. lemma OAI.SidorenkoCounterexample.histLeft0_1 line 22
  14. lemma OAI.SidorenkoCounterexample.histLeft0_2 line 23
  15. lemma OAI.SidorenkoCounterexample.histLeft0_3 line 24
  16. lemma OAI.SidorenkoCounterexample.histLeft0_4 line 25
  17. lemma OAI.SidorenkoCounterexample.histLeft0_5 line 26
  18. lemma OAI.SidorenkoCounterexample.histLeft0_6 line 27
  19. lemma OAI.SidorenkoCounterexample.histLeft0_7 line 28
  20. lemma OAI.SidorenkoCounterexample.histLeft0_8 line 29
  21. lemma OAI.SidorenkoCounterexample.histLeft0_9 line 30
  22. lemma OAI.SidorenkoCounterexample.histLeft0_10 line 31
  23. lemma OAI.SidorenkoCounterexample.histLeft0_11 line 32
  24. lemma OAI.SidorenkoCounterexample.histLeft0_12 line 33
  25. lemma OAI.SidorenkoCounterexample.histLeft0_correct line 34
  26. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_0 line 49
  27. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_1 line 50
  28. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_2 line 51
  29. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_3 line 52
  30. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_4 line 53
  31. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_5 line 54
  32. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_6 line 55
  33. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_7 line 56
  34. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_8 line 57
  35. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_9 line 58
  36. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_10 line 59
  37. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_11 line 60
  38. lemma OAI.SidorenkoCounterexample.refineLeft0_iff_12 line 61
  39. lemma OAI.SidorenkoCounterexample.refineLeft0_iff line 62
  40. def OAI.SidorenkoCounterexample.histRight0 line 77
  41. lemma OAI.SidorenkoCounterexample.histRight0_0 line 78
  42. lemma OAI.SidorenkoCounterexample.histRight0_1 line 79
  43. lemma OAI.SidorenkoCounterexample.histRight0_2 line 80
  44. lemma OAI.SidorenkoCounterexample.histRight0_3 line 81
  45. lemma OAI.SidorenkoCounterexample.histRight0_4 line 82
  46. lemma OAI.SidorenkoCounterexample.histRight0_5 line 83
  47. lemma OAI.SidorenkoCounterexample.histRight0_6 line 84
  48. lemma OAI.SidorenkoCounterexample.histRight0_7 line 85
  49. lemma OAI.SidorenkoCounterexample.histRight0_8 line 86
  50. lemma OAI.SidorenkoCounterexample.histRight0_9 line 87
  51. lemma OAI.SidorenkoCounterexample.histRight0_10 line 88
  52. lemma OAI.SidorenkoCounterexample.histRight0_11 line 89
  53. lemma OAI.SidorenkoCounterexample.histRight0_12 line 90
  54. lemma OAI.SidorenkoCounterexample.histRight0_13 line 91
  55. lemma OAI.SidorenkoCounterexample.histRight0_14 line 92
  56. lemma OAI.SidorenkoCounterexample.histRight0_15 line 93
  57. lemma OAI.SidorenkoCounterexample.histRight0_16 line 94
  58. lemma OAI.SidorenkoCounterexample.histRight0_17 line 95
  59. lemma OAI.SidorenkoCounterexample.histRight0_18 line 96
  60. lemma OAI.SidorenkoCounterexample.histRight0_19 line 97
  61. lemma OAI.SidorenkoCounterexample.histRight0_20 line 98
  62. lemma OAI.SidorenkoCounterexample.histRight0_21 line 99
  63. lemma OAI.SidorenkoCounterexample.histRight0_correct line 100
  64. lemma OAI.SidorenkoCounterexample.refineRight0_iff_0 line 124
  65. lemma OAI.SidorenkoCounterexample.refineRight0_iff_1 line 125
  66. lemma OAI.SidorenkoCounterexample.refineRight0_iff_2 line 126
  67. lemma OAI.SidorenkoCounterexample.refineRight0_iff_3 line 127
  68. lemma OAI.SidorenkoCounterexample.refineRight0_iff_4 line 128
  69. lemma OAI.SidorenkoCounterexample.refineRight0_iff_5 line 129
  70. lemma OAI.SidorenkoCounterexample.refineRight0_iff_6 line 130
  71. lemma OAI.SidorenkoCounterexample.refineRight0_iff_7 line 131
  72. lemma OAI.SidorenkoCounterexample.refineRight0_iff_8 line 132
  73. lemma OAI.SidorenkoCounterexample.refineRight0_iff_9 line 133
  74. lemma OAI.SidorenkoCounterexample.refineRight0_iff_10 line 134
  75. lemma OAI.SidorenkoCounterexample.refineRight0_iff_11 line 135
  76. lemma OAI.SidorenkoCounterexample.refineRight0_iff_12 line 136
  77. lemma OAI.SidorenkoCounterexample.refineRight0_iff_13 line 137
  78. lemma OAI.SidorenkoCounterexample.refineRight0_iff_14 line 138
  79. lemma OAI.SidorenkoCounterexample.refineRight0_iff_15 line 139
  80. lemma OAI.SidorenkoCounterexample.refineRight0_iff_16 line 140
  81. lemma OAI.SidorenkoCounterexample.refineRight0_iff_17 line 141
  82. lemma OAI.SidorenkoCounterexample.refineRight0_iff_18 line 142
  83. lemma OAI.SidorenkoCounterexample.refineRight0_iff_19 line 143
  84. lemma OAI.SidorenkoCounterexample.refineRight0_iff_20 line 144
  85. lemma OAI.SidorenkoCounterexample.refineRight0_iff_21 line 145
  86. lemma OAI.SidorenkoCounterexample.refineRight0_iff line 146
  87. def OAI.SidorenkoCounterexample.histLeft1 line 170
  88. lemma OAI.SidorenkoCounterexample.histLeft1_0 line 171
  89. lemma OAI.SidorenkoCounterexample.histLeft1_1 line 172
  90. lemma OAI.SidorenkoCounterexample.histLeft1_2 line 173
  91. lemma OAI.SidorenkoCounterexample.histLeft1_3 line 174
  92. lemma OAI.SidorenkoCounterexample.histLeft1_4 line 175
  93. lemma OAI.SidorenkoCounterexample.histLeft1_5 line 176
  94. lemma OAI.SidorenkoCounterexample.histLeft1_6 line 177
  95. lemma OAI.SidorenkoCounterexample.histLeft1_7 line 178
  96. lemma OAI.SidorenkoCounterexample.histLeft1_8 line 179
  97. lemma OAI.SidorenkoCounterexample.histLeft1_9 line 180
  98. lemma OAI.SidorenkoCounterexample.histLeft1_10 line 181
  99. lemma OAI.SidorenkoCounterexample.histLeft1_11 line 182
  100. lemma OAI.SidorenkoCounterexample.histLeft1_12 line 183
  101. lemma OAI.SidorenkoCounterexample.histLeft1_correct line 184
  102. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_0 line 199
  103. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_1 line 200
  104. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_2 line 201
  105. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_3 line 202
  106. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_4 line 203
  107. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_5 line 204
  108. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_6 line 205
  109. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_7 line 206
  110. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_8 line 207
  111. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_9 line 208
  112. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_10 line 209
  113. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_11 line 210
  114. lemma OAI.SidorenkoCounterexample.refineLeft1_iff_12 line 211
  115. lemma OAI.SidorenkoCounterexample.refineLeft1_iff line 212
  116. def OAI.SidorenkoCounterexample.histRight1 line 227
  117. lemma OAI.SidorenkoCounterexample.histRight1_0 line 228
  118. lemma OAI.SidorenkoCounterexample.histRight1_1 line 229
  119. lemma OAI.SidorenkoCounterexample.histRight1_2 line 230
  120. lemma OAI.SidorenkoCounterexample.histRight1_3 line 231
  121. lemma OAI.SidorenkoCounterexample.histRight1_4 line 232
  122. lemma OAI.SidorenkoCounterexample.histRight1_5 line 233
  123. lemma OAI.SidorenkoCounterexample.histRight1_6 line 234
  124. lemma OAI.SidorenkoCounterexample.histRight1_7 line 235
  125. lemma OAI.SidorenkoCounterexample.histRight1_8 line 236
  126. lemma OAI.SidorenkoCounterexample.histRight1_9 line 237
  127. lemma OAI.SidorenkoCounterexample.histRight1_10 line 238
  128. lemma OAI.SidorenkoCounterexample.histRight1_11 line 239
  129. lemma OAI.SidorenkoCounterexample.histRight1_12 line 240
  130. lemma OAI.SidorenkoCounterexample.histRight1_13 line 241
  131. lemma OAI.SidorenkoCounterexample.histRight1_14 line 242
  132. lemma OAI.SidorenkoCounterexample.histRight1_15 line 243
  133. lemma OAI.SidorenkoCounterexample.histRight1_16 line 244
  134. lemma OAI.SidorenkoCounterexample.histRight1_17 line 245
  135. lemma OAI.SidorenkoCounterexample.histRight1_18 line 246
  136. lemma OAI.SidorenkoCounterexample.histRight1_19 line 247
  137. lemma OAI.SidorenkoCounterexample.histRight1_20 line 248
  138. lemma OAI.SidorenkoCounterexample.histRight1_21 line 249
  139. lemma OAI.SidorenkoCounterexample.histRight1_correct line 250
  140. lemma OAI.SidorenkoCounterexample.refineRight1_iff_0 line 274
  141. lemma OAI.SidorenkoCounterexample.refineRight1_iff_1 line 275
  142. lemma OAI.SidorenkoCounterexample.refineRight1_iff_2 line 276
  143. lemma OAI.SidorenkoCounterexample.refineRight1_iff_3 line 277
  144. lemma OAI.SidorenkoCounterexample.refineRight1_iff_4 line 278
  145. lemma OAI.SidorenkoCounterexample.refineRight1_iff_5 line 279
  146. lemma OAI.SidorenkoCounterexample.refineRight1_iff_6 line 280
  147. lemma OAI.SidorenkoCounterexample.refineRight1_iff_7 line 281
  148. lemma OAI.SidorenkoCounterexample.refineRight1_iff_8 line 282
  149. lemma OAI.SidorenkoCounterexample.refineRight1_iff_9 line 283
  150. lemma OAI.SidorenkoCounterexample.refineRight1_iff_10 line 284
  151. lemma OAI.SidorenkoCounterexample.refineRight1_iff_11 line 285
  152. lemma OAI.SidorenkoCounterexample.refineRight1_iff_12 line 286
  153. lemma OAI.SidorenkoCounterexample.refineRight1_iff_13 line 287
  154. lemma OAI.SidorenkoCounterexample.refineRight1_iff_14 line 288
  155. lemma OAI.SidorenkoCounterexample.refineRight1_iff_15 line 289
  156. lemma OAI.SidorenkoCounterexample.refineRight1_iff_16 line 290
  157. lemma OAI.SidorenkoCounterexample.refineRight1_iff_17 line 291
  158. lemma OAI.SidorenkoCounterexample.refineRight1_iff_18 line 292
  159. lemma OAI.SidorenkoCounterexample.refineRight1_iff_19 line 293
  160. lemma OAI.SidorenkoCounterexample.refineRight1_iff_20 line 294
  161. lemma OAI.SidorenkoCounterexample.refineRight1_iff_21 line 295
  162. lemma OAI.SidorenkoCounterexample.refineRight1_iff line 296
  163. def OAI.SidorenkoCounterexample.histLeft2 line 320
  164. lemma OAI.SidorenkoCounterexample.histLeft2_0 line 321
  165. lemma OAI.SidorenkoCounterexample.histLeft2_1 line 322
  166. lemma OAI.SidorenkoCounterexample.histLeft2_2 line 323
  167. lemma OAI.SidorenkoCounterexample.histLeft2_3 line 324
  168. lemma OAI.SidorenkoCounterexample.histLeft2_4 line 325
  169. lemma OAI.SidorenkoCounterexample.histLeft2_5 line 326
  170. lemma OAI.SidorenkoCounterexample.histLeft2_6 line 327
  171. lemma OAI.SidorenkoCounterexample.histLeft2_7 line 328
  172. lemma OAI.SidorenkoCounterexample.histLeft2_8 line 329
  173. lemma OAI.SidorenkoCounterexample.histLeft2_9 line 330
  174. lemma OAI.SidorenkoCounterexample.histLeft2_10 line 331
  175. lemma OAI.SidorenkoCounterexample.histLeft2_11 line 332
  176. lemma OAI.SidorenkoCounterexample.histLeft2_12 line 333
  177. lemma OAI.SidorenkoCounterexample.histLeft2_correct line 334
  178. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_0 line 349
  179. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_1 line 350
  180. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_2 line 351
  181. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_3 line 352
  182. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_4 line 353
  183. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_5 line 354
  184. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_6 line 355
  185. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_7 line 356
  186. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_8 line 357
  187. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_9 line 358
  188. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_10 line 359
  189. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_11 line 360
  190. lemma OAI.SidorenkoCounterexample.refineLeft2_iff_12 line 361
  191. lemma OAI.SidorenkoCounterexample.refineLeft2_iff line 362
  192. def OAI.SidorenkoCounterexample.histRight2 line 377
  193. lemma OAI.SidorenkoCounterexample.histRight2_0 line 378
  194. lemma OAI.SidorenkoCounterexample.histRight2_1 line 379
  195. lemma OAI.SidorenkoCounterexample.histRight2_2 line 380
  196. lemma OAI.SidorenkoCounterexample.histRight2_3 line 381
  197. lemma OAI.SidorenkoCounterexample.histRight2_4 line 382
  198. lemma OAI.SidorenkoCounterexample.histRight2_5 line 383
  199. lemma OAI.SidorenkoCounterexample.histRight2_6 line 384
  200. lemma OAI.SidorenkoCounterexample.histRight2_7 line 385
  201. lemma OAI.SidorenkoCounterexample.histRight2_8 line 386
  202. lemma OAI.SidorenkoCounterexample.histRight2_9 line 387
  203. lemma OAI.SidorenkoCounterexample.histRight2_10 line 388
  204. lemma OAI.SidorenkoCounterexample.histRight2_11 line 389
  205. lemma OAI.SidorenkoCounterexample.histRight2_12 line 390
  206. lemma OAI.SidorenkoCounterexample.histRight2_13 line 391
  207. lemma OAI.SidorenkoCounterexample.histRight2_14 line 392
  208. lemma OAI.SidorenkoCounterexample.histRight2_15 line 393
  209. lemma OAI.SidorenkoCounterexample.histRight2_16 line 394
  210. lemma OAI.SidorenkoCounterexample.histRight2_17 line 395
  211. lemma OAI.SidorenkoCounterexample.histRight2_18 line 396
  212. lemma OAI.SidorenkoCounterexample.histRight2_19 line 397
  213. lemma OAI.SidorenkoCounterexample.histRight2_20 line 398
  214. lemma OAI.SidorenkoCounterexample.histRight2_21 line 399
  215. lemma OAI.SidorenkoCounterexample.histRight2_correct line 400
  216. lemma OAI.SidorenkoCounterexample.refineRight2_iff_0 line 424
  217. lemma OAI.SidorenkoCounterexample.refineRight2_iff_1 line 425
  218. lemma OAI.SidorenkoCounterexample.refineRight2_iff_2 line 426
  219. lemma OAI.SidorenkoCounterexample.refineRight2_iff_3 line 427
  220. lemma OAI.SidorenkoCounterexample.refineRight2_iff_4 line 428
  221. lemma OAI.SidorenkoCounterexample.refineRight2_iff_5 line 429
  222. lemma OAI.SidorenkoCounterexample.refineRight2_iff_6 line 430
  223. lemma OAI.SidorenkoCounterexample.refineRight2_iff_7 line 431
  224. lemma OAI.SidorenkoCounterexample.refineRight2_iff_8 line 432
  225. lemma OAI.SidorenkoCounterexample.refineRight2_iff_9 line 433
  226. lemma OAI.SidorenkoCounterexample.refineRight2_iff_10 line 434
  227. lemma OAI.SidorenkoCounterexample.refineRight2_iff_11 line 435
  228. lemma OAI.SidorenkoCounterexample.refineRight2_iff_12 line 436
  229. lemma OAI.SidorenkoCounterexample.refineRight2_iff_13 line 437
  230. lemma OAI.SidorenkoCounterexample.refineRight2_iff_14 line 438
  231. lemma OAI.SidorenkoCounterexample.refineRight2_iff_15 line 439
  232. lemma OAI.SidorenkoCounterexample.refineRight2_iff_16 line 440
  233. lemma OAI.SidorenkoCounterexample.refineRight2_iff_17 line 441
  234. lemma OAI.SidorenkoCounterexample.refineRight2_iff_18 line 442
  235. lemma OAI.SidorenkoCounterexample.refineRight2_iff_19 line 443
  236. lemma OAI.SidorenkoCounterexample.refineRight2_iff_20 line 444
  237. lemma OAI.SidorenkoCounterexample.refineRight2_iff_21 line 445
  238. lemma OAI.SidorenkoCounterexample.refineRight2_iff line 446
  239. def OAI.SidorenkoCounterexample.histLeft3 line 470
  240. lemma OAI.SidorenkoCounterexample.histLeft3_0 line 471
  241. lemma OAI.SidorenkoCounterexample.histLeft3_1 line 472
  242. lemma OAI.SidorenkoCounterexample.histLeft3_2 line 473
  243. lemma OAI.SidorenkoCounterexample.histLeft3_3 line 474
  244. lemma OAI.SidorenkoCounterexample.histLeft3_4 line 475
  245. lemma OAI.SidorenkoCounterexample.histLeft3_5 line 476
  246. lemma OAI.SidorenkoCounterexample.histLeft3_6 line 477
  247. lemma OAI.SidorenkoCounterexample.histLeft3_7 line 478
  248. lemma OAI.SidorenkoCounterexample.histLeft3_8 line 479
  249. lemma OAI.SidorenkoCounterexample.histLeft3_9 line 480
  250. lemma OAI.SidorenkoCounterexample.histLeft3_10 line 481
  251. lemma OAI.SidorenkoCounterexample.histLeft3_11 line 482
  252. lemma OAI.SidorenkoCounterexample.histLeft3_12 line 483
  253. lemma OAI.SidorenkoCounterexample.histLeft3_correct line 484
  254. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_0 line 499
  255. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_1 line 500
  256. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_2 line 501
  257. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_3 line 502
  258. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_4 line 503
  259. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_5 line 504
  260. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_6 line 505
  261. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_7 line 506
  262. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_8 line 507
  263. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_9 line 508
  264. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_10 line 509
  265. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_11 line 510
  266. lemma OAI.SidorenkoCounterexample.refineLeft3_iff_12 line 511
  267. lemma OAI.SidorenkoCounterexample.refineLeft3_iff line 512
  268. def OAI.SidorenkoCounterexample.histRight3 line 527
  269. lemma OAI.SidorenkoCounterexample.histRight3_0 line 528
  270. lemma OAI.SidorenkoCounterexample.histRight3_1 line 529
  271. lemma OAI.SidorenkoCounterexample.histRight3_2 line 530
  272. lemma OAI.SidorenkoCounterexample.histRight3_3 line 531
  273. lemma OAI.SidorenkoCounterexample.histRight3_4 line 532
  274. lemma OAI.SidorenkoCounterexample.histRight3_5 line 533
  275. lemma OAI.SidorenkoCounterexample.histRight3_6 line 534
  276. lemma OAI.SidorenkoCounterexample.histRight3_7 line 535
  277. lemma OAI.SidorenkoCounterexample.histRight3_8 line 536
  278. lemma OAI.SidorenkoCounterexample.histRight3_9 line 537
  279. lemma OAI.SidorenkoCounterexample.histRight3_10 line 538
  280. lemma OAI.SidorenkoCounterexample.histRight3_11 line 539
  281. lemma OAI.SidorenkoCounterexample.histRight3_12 line 540
  282. lemma OAI.SidorenkoCounterexample.histRight3_13 line 541
  283. lemma OAI.SidorenkoCounterexample.histRight3_14 line 542
  284. lemma OAI.SidorenkoCounterexample.histRight3_15 line 543
  285. lemma OAI.SidorenkoCounterexample.histRight3_16 line 544
  286. lemma OAI.SidorenkoCounterexample.histRight3_17 line 545
  287. lemma OAI.SidorenkoCounterexample.histRight3_18 line 546
  288. lemma OAI.SidorenkoCounterexample.histRight3_19 line 547
  289. lemma OAI.SidorenkoCounterexample.histRight3_20 line 548
  290. lemma OAI.SidorenkoCounterexample.histRight3_21 line 549
  291. lemma OAI.SidorenkoCounterexample.histRight3_correct line 550
  292. lemma OAI.SidorenkoCounterexample.refineRight3_iff_0 line 574
  293. lemma OAI.SidorenkoCounterexample.refineRight3_iff_1 line 575
  294. lemma OAI.SidorenkoCounterexample.refineRight3_iff_2 line 576
  295. lemma OAI.SidorenkoCounterexample.refineRight3_iff_3 line 577
  296. lemma OAI.SidorenkoCounterexample.refineRight3_iff_4 line 578
  297. lemma OAI.SidorenkoCounterexample.refineRight3_iff_5 line 579
  298. lemma OAI.SidorenkoCounterexample.refineRight3_iff_6 line 580
  299. lemma OAI.SidorenkoCounterexample.refineRight3_iff_7 line 581
  300. lemma OAI.SidorenkoCounterexample.refineRight3_iff_8 line 582
  301. lemma OAI.SidorenkoCounterexample.refineRight3_iff_9 line 583
  302. lemma OAI.SidorenkoCounterexample.refineRight3_iff_10 line 584
  303. lemma OAI.SidorenkoCounterexample.refineRight3_iff_11 line 585
  304. lemma OAI.SidorenkoCounterexample.refineRight3_iff_12 line 586
  305. lemma OAI.SidorenkoCounterexample.refineRight3_iff_13 line 587
  306. lemma OAI.SidorenkoCounterexample.refineRight3_iff_14 line 588
  307. lemma OAI.SidorenkoCounterexample.refineRight3_iff_15 line 589
  308. lemma OAI.SidorenkoCounterexample.refineRight3_iff_16 line 590
  309. lemma OAI.SidorenkoCounterexample.refineRight3_iff_17 line 591
  310. lemma OAI.SidorenkoCounterexample.refineRight3_iff_18 line 592
  311. lemma OAI.SidorenkoCounterexample.refineRight3_iff_19 line 593
  312. lemma OAI.SidorenkoCounterexample.refineRight3_iff_20 line 594
  313. lemma OAI.SidorenkoCounterexample.refineRight3_iff_21 line 595
  314. lemma OAI.SidorenkoCounterexample.refineRight3_iff line 596
  315. lemma OAI.SidorenkoCounterexample.refineLeft_final line 620
  316. lemma OAI.SidorenkoCounterexample.refineRight_final line 621