OAI/GameTheory/SnakyConditional/Templates/Level34Part02.lean

GitHub source file

318 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_610 line 8
2. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_5 line 9
3. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_5_chain line 10
4. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_5_head line 11
5. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_5_last line 12
6. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_6 line 13
7. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_6_chain line 14
8. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_6_head line 15
9. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_6_last line 16
10. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_4 line 17
11. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_4_chain line 18
12. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_4_head line 21
13. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_4_last line 23
14. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_8 line 25
15. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_8_chain line 26
16. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_8_head line 27
17. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_8_last line 28
18. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_9 line 29
19. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_9_chain line 30
20. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_9_head line 31
21. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_9_last line 32
22. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_7 line 33
23. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_7_chain line 34
24. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_7_head line 37
25. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_7_last line 39
26. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_3 line 41
27. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_3_chain line 42
28. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_3_head line 45
29. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_3_last line 47
30. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_12 line 49
31. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_12_chain line 50
32. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_12_head line 51
33. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_12_last line 52
34. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_13 line 53
35. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_13_chain line 54
36. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_13_head line 55
37. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_13_last line 56
38. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_11 line 57
39. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_11_chain line 58
40. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_11_head line 61
41. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_11_last line 63
42. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_15 line 65
43. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_15_chain line 66
44. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_15_head line 67
45. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_15_last line 68
46. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_16 line 69
47. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_16_chain line 70
48. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_16_head line 71
49. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_16_last line 72
50. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_14 line 73
51. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_14_chain line 74
52. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_14_head line 77
53. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_14_last line 79
54. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_10 line 81
55. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_10_chain line 82
56. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_10_head line 85
57. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_10_last line 87
58. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_2 line 89
59. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_2_chain line 90
60. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_2_head line 93
61. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_2_last line 95
62. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_20 line 97
63. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_20_chain line 98
64. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_20_head line 99
65. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_20_last line 100
66. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_21 line 101
67. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_21_chain line 102
68. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_21_head line 103
69. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_21_last line 104
70. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_19 line 105
71. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_19_chain line 106
72. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_19_head line 109
73. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_19_last line 111
74. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_23 line 113
75. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_23_chain line 114
76. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_23_head line 115
77. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_23_last line 116
78. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_24 line 117
79. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_24_chain line 118
80. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_24_head line 119
81. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_24_last line 120
82. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_22 line 121
83. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_22_chain line 122
84. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_22_head line 125
85. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_22_last line 127
86. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_18 line 129
87. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_18_chain line 130
88. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_18_head line 133
89. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_18_last line 135
90. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_27 line 137
91. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_27_chain line 138
92. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_27_head line 139
93. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_27_last line 140
94. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_28 line 141
95. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_28_chain line 142
96. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_28_head line 143
97. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_28_last line 144
98. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_26 line 145
99. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_26_chain line 146
100. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_26_head line 149
101. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_26_last line 151
102. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_30 line 153
103. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_30_chain line 154
104. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_30_head line 155
105. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_30_last line 156
106. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_31 line 157
107. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_31_chain line 158
108. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_31_head line 159
109. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_31_last line 160
110. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_29 line 161
111. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_29_chain line 162
112. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_29_head line 165
113. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_29_last line 167
114. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_25 line 169
115. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_25_chain line 170
116. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_25_head line 173
117. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_25_last line 175
118. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_17 line 177
119. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_17_chain line 178
120. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_17_head line 181
121. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_17_last line 183
122. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_1 line 185
123. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_1_chain line 186
124. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_1_head line 189
125. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_1_last line 191
126. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_36 line 193
127. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_36_chain line 194
128. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_36_head line 195
129. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_36_last line 196
130. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_37 line 197
131. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_37_chain line 198
132. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_37_head line 199
133. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_37_last line 200
134. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_35 line 201
135. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_35_chain line 202
136. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_35_head line 205
137. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_35_last line 207
138. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_39 line 209
139. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_39_chain line 210
140. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_39_head line 211
141. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_39_last line 212
142. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_40 line 213
143. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_40_chain line 214
144. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_40_head line 215
145. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_40_last line 216
146. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_38 line 217
147. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_38_chain line 218
148. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_38_head line 221
149. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_38_last line 223
150. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_34 line 225
151. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_34_chain line 226
152. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_34_head line 229
153. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_34_last line 231
154. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_43 line 233
155. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_43_chain line 234
156. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_43_head line 235
157. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_43_last line 236
158. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_44 line 237
159. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_44_chain line 238
160. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_44_head line 239
161. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_44_last line 240
162. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_42 line 241
163. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_42_chain line 242
164. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_42_head line 245
165. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_42_last line 247
166. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_46 line 249
167. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_46_chain line 250
168. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_46_head line 251
169. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_46_last line 252
170. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_47 line 253
171. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_47_chain line 254
172. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_47_head line 255
173. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_47_last line 256
174. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_45 line 257
175. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_45_chain line 258
176. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_45_head line 261
177. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_45_last line 263
178. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_41 line 265
179. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_41_chain line 266
180. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_41_head line 269
181. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_41_last line 271
182. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_33 line 273
183. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_33_chain line 274
184. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_33_head line 277
185. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_33_last line 279
186. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_51 line 281
187. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_51_chain line 282
188. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_51_head line 283
189. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_51_last line 284
190. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_52 line 285
191. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_52_chain line 286
192. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_52_head line 287
193. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_52_last line 288
194. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_50 line 289
195. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_50_chain line 290
196. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_50_head line 293
197. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_50_last line 295
198. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_54 line 297
199. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_54_chain line 298
200. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_54_head line 299
201. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_54_last line 300
202. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_55 line 301
203. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_55_chain line 302
204. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_55_head line 303
205. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_55_last line 304
206. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_53 line 305
207. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_53_chain line 306
208. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_53_head line 309
209. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_53_last line 311
210. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_49 line 313
211. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_49_chain line 314
212. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_49_head line 317
213. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_49_last line 319
214. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_58 line 321
215. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_58_chain line 322
216. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_58_head line 323
217. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_58_last line 324
218. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_59 line 325
219. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_59_chain line 326
220. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_59_head line 327
221. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_59_last line 328
222. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_57 line 329
223. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_57_chain line 330
224. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_57_head line 333
225. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_57_last line 335
226. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_61 line 337
227. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_61_chain line 338
228. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_61_head line 339
229. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_61_last line 340
230. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_62 line 341
231. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_62_chain line 342
232. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_62_head line 343
233. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_62_last line 344
234. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_60 line 345
235. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_60_chain line 346
236. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_60_head line 349
237. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_60_last line 351
238. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_56 line 353
239. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_56_chain line 354
240. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_56_head line 357
241. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_56_last line 359
242. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_48 line 361
243. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_48_chain line 362
244. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_48_head line 365
245. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_48_last line 367
246. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_32 line 369
247. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_32_chain line 370
248. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_32_head line 373
249. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_32_last line 375
250. def OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_0 line 377
251. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_0_chain line 378
252. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_0_head line 381
253. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_0_last line 383
254. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_envelope_610_nodup line 385
255. def OAI.SnakyConditional.envelope_610 line 387
256. def OAI.SnakyConditional.childrenC_610 line 388
257. def OAI.SnakyConditional.childrenD_610 line 389
258. theorem OAI.SnakyConditional.common_sub_610 line 390
259. theorem OAI.SnakyConditional.child_required_sub_610 line 391
260. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_0_points_0 line 392
261. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_0_points_1 line 395
262. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_0 line 398
263. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_1_points_0 line 403
264. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_1_points_1 line 406
265. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_1 line 409
266. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_2_points_0 line 414
267. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_2 line 417
268. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_3_points_0 line 422
269. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_3_points_1 line 425
270. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_3_points_2 line 428
271. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_3_points_3 line 431
272. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_3_points_4 line 434
273. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_3 line 437
274. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_0 line 442
275. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_1 line 445
276. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_2 line 448
277. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_3 line 451
278. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_4 line 454
279. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_5 line 457
280. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4_points_6 line 460
281. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_4 line 463
282. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_5_points_0 line 468
283. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_5_points_1 line 471
284. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_5_points_2 line 474
285. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_5_points_3 line 477
286. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_5 line 480
287. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_6_points_0 line 485
288. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_6_points_1 line 488
289. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_6_points_2 line 491
290. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_6_points_3 line 494
291. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_6_points_4 line 497
292. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_6 line 500
293. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_0 line 505
294. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_1 line 508
295. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_2 line 511
296. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_3 line 514
297. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_4 line 517
298. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_5 line 520
299. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_6 line 523
300. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_7 line 526
301. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_8 line 529
302. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_9 line 532
303. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_10 line 535
304. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_11 line 538
305. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_12 line 541
306. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_13 line 544
307. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_14 line 547
308. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_15 line 550
309. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_16 line 553
310. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_17 line 556
311. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_18 line 559
312. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_19 line 562
313. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7_points_20 line 565
314. theorem OAI.SnakyConditional.Internal.SnakyRows012.containment_610_7 line 568
315. theorem OAI.SnakyConditional.child_envelope_sub_610 line 570
316. theorem OAI.SnakyConditional.pivot_mem_610 line 581
317. theorem OAI.SnakyConditional.children_work_610 line 582
318. theorem OAI.SnakyConditional.row_works_610 line 593