OAI/GameTheory/SnakyConditional/Opening/Opening.lean

GitHub source file

423 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.nearBlock line 8
2. def OAI.SnakyConditional.nearPoint line 9
3. theorem OAI.SnakyConditional.nearPoint_cover line 10
4. def OAI.SnakyConditional.distantEnvelopes line 11
5. theorem OAI.SnakyConditional.distant_required_0 line 12
6. theorem OAI.SnakyConditional.distant_required_1 line 13
7. theorem OAI.SnakyConditional.distant_required_2 line 14
8. theorem OAI.SnakyConditional.distant_required_3 line 15
9. theorem OAI.SnakyConditional.distant_required_4 line 16
10. theorem OAI.SnakyConditional.distant_required_5 line 17
11. theorem OAI.SnakyConditional.distant_required_6 line 18
12. theorem OAI.SnakyConditional.distant_required_7 line 19
13. theorem OAI.SnakyConditional.distant_required_8 line 20
14. theorem OAI.SnakyConditional.distant_required_9 line 21
15. theorem OAI.SnakyConditional.distant_required_10 line 22
16. theorem OAI.SnakyConditional.distant_required_11 line 23
17. theorem OAI.SnakyConditional.distant_required_12 line 24
18. theorem OAI.SnakyConditional.distant_required_13 line 25
19. theorem OAI.SnakyConditional.distant_required_14 line 26
20. theorem OAI.SnakyConditional.distant_required_15 line 27
21. theorem OAI.SnakyConditional.distant_required_16 line 28
22. theorem OAI.SnakyConditional.distant_required_17 line 29
23. theorem OAI.SnakyConditional.distant_required_18 line 30
24. theorem OAI.SnakyConditional.distant_required_19 line 31
25. theorem OAI.SnakyConditional.distant_required_20 line 32
26. theorem OAI.SnakyConditional.distant_required_21 line 33
27. theorem OAI.SnakyConditional.distant_required_22 line 34
28. theorem OAI.SnakyConditional.distant_required_23 line 35
29. theorem OAI.SnakyConditional.distant_works line 36
30. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_commonEnvelope_subset_of_escape line 111
31. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_commonEnvelope_subset_of_placed_escape line 120
32. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_000 line 133
33. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_001 line 136
34. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_002 line 139
35. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_003 line 142
36. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_004 line 145
37. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_005 line 148
38. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_006 line 151
39. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_007 line 154
40. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_008 line 157
41. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_009 line 160
42. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_010 line 163
43. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_011 line 166
44. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_012 line 169
45. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_013 line 172
46. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_014 line 175
47. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_015 line 178
48. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_016 line 181
49. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_017 line 184
50. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_018 line 187
51. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_019 line 190
52. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_020 line 193
53. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_021 line 196
54. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_022 line 199
55. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_023 line 202
56. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_024 line 205
57. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_025 line 208
58. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_026 line 211
59. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_027 line 214
60. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_028 line 217
61. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_029 line 220
62. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_030 line 223
63. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_031 line 226
64. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_032 line 229
65. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_033 line 232
66. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_034 line 235
67. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_035 line 238
68. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_036 line 241
69. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_037 line 244
70. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_038 line 247
71. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_039 line 250
72. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_040 line 253
73. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_041 line 256
74. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_042 line 259
75. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_043 line 262
76. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_044 line 265
77. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_045 line 268
78. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_046 line 271
79. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_047 line 274
80. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_048 line 277
81. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_049 line 280
82. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_050 line 283
83. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_051 line 286
84. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_052 line 289
85. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_053 line 292
86. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_054 line 295
87. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_055 line 298
88. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_056 line 301
89. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_057 line 304
90. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_058 line 307
91. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_059 line 310
92. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_060 line 313
93. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_061 line 316
94. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_062 line 319
95. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_063 line 322
96. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_064 line 325
97. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_065 line 328
98. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_066 line 331
99. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_067 line 334
100. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_068 line 337
101. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_069 line 340
102. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_070 line 343
103. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_071 line 346
104. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_072 line 349
105. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_073 line 352
106. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_074 line 355
107. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_075 line 358
108. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_076 line 361
109. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_077 line 364
110. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_078 line 367
111. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_079 line 370
112. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_080 line 373
113. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_081 line 376
114. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_082 line 379
115. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_083 line 382
116. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_084 line 385
117. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_085 line 388
118. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_086 line 391
119. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_087 line 394
120. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_088 line 397
121. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_089 line 400
122. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_090 line 403
123. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_091 line 406
124. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_092 line 409
125. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_093 line 412
126. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_094 line 415
127. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_095 line 418
128. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_096 line 421
129. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_097 line 424
130. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_098 line 427
131. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_099 line 430
132. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_100 line 433
133. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_101 line 436
134. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_102 line 439
135. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_103 line 442
136. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_104 line 445
137. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_105 line 448
138. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_106 line 451
139. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_107 line 454
140. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_108 line 457
141. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_109 line 460
142. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_110 line 463
143. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_111 line 466
144. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_112 line 469
145. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_113 line 472
146. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_114 line 475
147. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_115 line 478
148. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_116 line 481
149. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_point_117 line 484
150. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_000 line 487
151. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_001 line 490
152. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_002 line 493
153. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_003 line 496
154. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_004 line 499
155. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_005 line 502
156. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_006 line 505
157. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_chunk_007 line 508
158. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_escape_source line 511
159. theorem OAI.SnakyConditional.distant_common_sub line 515
160. def OAI.SnakyConditional.localPair line 518
161. theorem OAI.SnakyConditional.row615_owned line 519
162. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_6 line 520
163. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_6_not_mem line 521
164. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_7 line 522
165. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_7_not_mem line 523
166. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_5 line 524
167. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_5_not_mem line 525
168. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_9 line 528
169. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_9_not_mem line 529
170. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_10 line 530
171. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_10_not_mem line 531
172. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_8 line 532
173. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_8_not_mem line 533
174. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_4 line 536
175. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_4_not_mem line 537
176. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_13 line 540
177. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_13_not_mem line 541
178. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_14 line 542
179. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_14_not_mem line 543
180. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_12 line 544
181. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_12_not_mem line 545
182. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_16 line 548
183. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_16_not_mem line 549
184. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_17 line 550
185. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_17_not_mem line 551
186. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_15 line 552
187. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_15_not_mem line 553
188. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_11 line 556
189. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_11_not_mem line 557
190. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_3 line 560
191. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_3_not_mem line 561
192. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_21 line 564
193. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_21_not_mem line 565
194. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_22 line 566
195. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_22_not_mem line 567
196. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_20 line 568
197. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_20_not_mem line 569
198. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_24 line 572
199. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_24_not_mem line 573
200. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_25 line 574
201. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_25_not_mem line 575
202. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_23 line 576
203. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_23_not_mem line 577
204. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_19 line 580
205. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_19_not_mem line 581
206. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_28 line 584
207. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_28_not_mem line 585
208. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_29 line 586
209. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_29_not_mem line 587
210. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_27 line 588
211. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_27_not_mem line 589
212. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_31 line 592
213. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_31_not_mem line 593
214. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_32 line 594
215. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_32_not_mem line 595
216. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_30 line 596
217. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_30_not_mem line 597
218. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_26 line 600
219. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_26_not_mem line 601
220. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_18 line 604
221. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_18_not_mem line 605
222. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_2 line 608
223. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_2_not_mem line 609
224. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_37 line 612
225. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_37_not_mem line 613
226. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_38 line 614
227. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_38_not_mem line 615
228. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_36 line 616
229. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_36_not_mem line 617
230. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_40 line 620
231. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_40_not_mem line 621
232. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_41 line 622
233. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_41_not_mem line 623
234. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_39 line 624
235. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_39_not_mem line 625
236. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_35 line 628
237. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_35_not_mem line 629
238. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_44 line 632
239. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_44_not_mem line 633
240. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_45 line 634
241. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_45_not_mem line 635
242. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_43 line 636
243. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_43_not_mem line 637
244. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_47 line 640
245. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_47_not_mem line 641
246. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_48 line 642
247. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_48_not_mem line 643
248. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_46 line 644
249. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_46_not_mem line 645
250. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_42 line 648
251. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_42_not_mem line 649
252. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_34 line 652
253. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_34_not_mem line 653
254. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_52 line 656
255. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_52_not_mem line 657
256. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_53 line 658
257. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_53_not_mem line 659
258. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_51 line 660
259. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_51_not_mem line 661
260. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_55 line 664
261. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_55_not_mem line 665
262. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_56 line 666
263. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_56_not_mem line 667
264. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_54 line 668
265. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_54_not_mem line 669
266. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_50 line 672
267. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_50_not_mem line 673
268. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_59 line 676
269. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_59_not_mem line 677
270. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_60 line 678
271. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_60_not_mem line 679
272. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_58 line 680
273. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_58_not_mem line 681
274. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_62 line 684
275. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_62_not_mem line 685
276. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_63 line 686
277. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_63_not_mem line 687
278. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_61 line 688
279. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_61_not_mem line 689
280. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_57 line 692
281. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_57_not_mem line 693
282. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_49 line 696
283. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_49_not_mem line 697
284. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_33 line 700
285. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_33_not_mem line 701
286. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_1 line 704
287. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_1_not_mem line 705
288. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_69 line 708
289. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_69_not_mem line 709
290. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_70 line 710
291. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_70_not_mem line 711
292. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_68 line 712
293. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_68_not_mem line 713
294. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_72 line 716
295. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_72_not_mem line 717
296. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_73 line 718
297. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_73_not_mem line 719
298. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_71 line 720
299. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_71_not_mem line 721
300. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_67 line 724
301. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_67_not_mem line 725
302. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_76 line 728
303. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_76_not_mem line 729
304. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_77 line 730
305. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_77_not_mem line 731
306. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_75 line 732
307. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_75_not_mem line 733
308. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_79 line 736
309. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_79_not_mem line 737
310. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_80 line 738
311. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_80_not_mem line 739
312. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_78 line 740
313. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_78_not_mem line 741
314. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_74 line 744
315. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_74_not_mem line 745
316. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_66 line 748
317. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_66_not_mem line 749
318. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_84 line 752
319. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_84_not_mem line 753
320. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_85 line 754
321. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_85_not_mem line 755
322. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_83 line 756
323. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_83_not_mem line 757
324. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_87 line 760
325. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_87_not_mem line 761
326. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_88 line 762
327. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_88_not_mem line 763
328. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_86 line 764
329. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_86_not_mem line 765
330. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_82 line 768
331. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_82_not_mem line 769
332. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_91 line 772
333. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_91_not_mem line 773
334. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_92 line 774
335. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_92_not_mem line 775
336. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_90 line 776
337. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_90_not_mem line 777
338. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_94 line 780
339. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_94_not_mem line 781
340. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_95 line 782
341. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_95_not_mem line 783
342. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_93 line 784
343. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_93_not_mem line 785
344. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_89 line 788
345. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_89_not_mem line 789
346. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_81 line 792
347. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_81_not_mem line 793
348. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_65 line 796
349. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_65_not_mem line 797
350. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_100 line 800
351. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_100_not_mem line 801
352. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_101 line 802
353. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_101_not_mem line 803
354. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_99 line 804
355. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_99_not_mem line 805
356. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_103 line 808
357. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_103_not_mem line 809
358. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_104 line 810
359. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_104_not_mem line 811
360. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_102 line 812
361. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_102_not_mem line 813
362. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_98 line 816
363. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_98_not_mem line 817
364. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_107 line 820
365. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_107_not_mem line 821
366. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_108 line 822
367. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_108_not_mem line 823
368. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_106 line 824
369. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_106_not_mem line 825
370. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_110 line 828
371. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_110_not_mem line 829
372. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_111 line 830
373. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_111_not_mem line 831
374. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_109 line 832
375. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_109_not_mem line 833
376. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_105 line 836
377. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_105_not_mem line 837
378. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_97 line 840
379. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_97_not_mem line 841
380. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_115 line 844
381. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_115_not_mem line 845
382. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_116 line 846
383. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_116_not_mem line 847
384. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_114 line 848
385. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_114_not_mem line 849
386. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_118 line 852
387. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_118_not_mem line 853
388. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_119 line 854
389. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_119_not_mem line 855
390. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_117 line 856
391. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_117_not_mem line 857
392. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_113 line 860
393. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_113_not_mem line 861
394. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_122 line 864
395. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_122_not_mem line 865
396. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_123 line 866
397. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_123_not_mem line 867
398. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_121 line 868
399. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_121_not_mem line 869
400. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_125 line 872
401. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_125_not_mem line 873
402. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_126 line 874
403. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_126_not_mem line 875
404. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_124 line 876
405. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_124_not_mem line 877
406. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_120 line 880
407. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_120_not_mem line 881
408. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_112 line 884
409. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_112_not_mem line 885
410. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_96 line 888
411. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_96_not_mem line 889
412. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_64 line 892
413. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_64_not_mem line 893
414. def OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_0 line 896
415. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_negative615_list_0_not_mem line 897
416. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_breaker_outside_615 line 900
417. theorem OAI.SnakyConditional.Internal.SnakyOpening.opening_breaker_disjoint_615 line 903
418. theorem OAI.SnakyConditional.row615_pair_after_breaker line 906
419. theorem OAI.SnakyConditional.near_local_left line 912
420. theorem OAI.SnakyConditional.near_local_right line 918
421. theorem OAI.SnakyConditional.near_works line 924
422. theorem OAI.SnakyConditional.all_first_replies line 951
423. theorem OAI.SnakyConditional.empty_board_wins line 962