OAI/GameTheory/SnakyConditional/Templates/Level31Part01.lean

GitHub source file

280 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_596 line 7
2. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_4 line 8
3. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_4_chain line 9
4. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_4_head line 10
5. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_4_last line 11
6. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_5 line 12
7. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_5_chain line 13
8. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_5_head line 14
9. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_5_last line 15
10. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_3 line 16
11. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_3_chain line 17
12. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_3_head line 20
13. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_3_last line 22
14. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_7 line 24
15. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_7_chain line 25
16. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_7_head line 26
17. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_7_last line 27
18. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_8 line 28
19. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_8_chain line 29
20. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_8_head line 30
21. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_8_last line 31
22. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_6 line 32
23. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_6_chain line 33
24. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_6_head line 36
25. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_6_last line 38
26. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_2 line 40
27. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_2_chain line 41
28. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_2_head line 44
29. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_2_last line 46
30. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_11 line 48
31. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_11_chain line 49
32. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_11_head line 50
33. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_11_last line 51
34. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_12 line 52
35. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_12_chain line 53
36. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_12_head line 54
37. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_12_last line 55
38. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_10 line 56
39. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_10_chain line 57
40. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_10_head line 60
41. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_10_last line 62
42. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_14 line 64
43. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_14_chain line 65
44. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_14_head line 66
45. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_14_last line 67
46. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_15 line 68
47. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_15_chain line 69
48. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_15_head line 70
49. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_15_last line 71
50. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_13 line 72
51. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_13_chain line 73
52. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_13_head line 76
53. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_13_last line 78
54. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_9 line 80
55. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_9_chain line 81
56. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_9_head line 84
57. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_9_last line 86
58. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_1 line 88
59. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_1_chain line 89
60. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_1_head line 92
61. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_1_last line 94
62. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_19 line 96
63. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_19_chain line 97
64. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_19_head line 98
65. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_19_last line 99
66. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_20 line 100
67. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_20_chain line 101
68. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_20_head line 102
69. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_20_last line 103
70. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_18 line 104
71. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_18_chain line 105
72. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_18_head line 108
73. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_18_last line 110
74. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_22 line 112
75. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_22_chain line 113
76. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_22_head line 114
77. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_22_last line 115
78. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_23 line 116
79. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_23_chain line 117
80. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_23_head line 118
81. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_23_last line 119
82. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_21 line 120
83. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_21_chain line 121
84. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_21_head line 124
85. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_21_last line 126
86. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_17 line 128
87. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_17_chain line 129
88. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_17_head line 132
89. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_17_last line 134
90. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_26 line 136
91. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_26_chain line 137
92. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_26_head line 138
93. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_26_last line 139
94. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_27 line 140
95. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_27_chain line 141
96. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_27_head line 142
97. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_27_last line 143
98. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_25 line 144
99. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_25_chain line 145
100. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_25_head line 148
101. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_25_last line 150
102. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_29 line 152
103. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_29_chain line 153
104. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_29_head line 154
105. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_29_last line 155
106. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_30 line 156
107. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_30_chain line 157
108. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_30_head line 158
109. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_30_last line 159
110. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_28 line 160
111. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_28_chain line 161
112. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_28_head line 164
113. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_28_last line 166
114. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_24 line 168
115. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_24_chain line 169
116. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_24_head line 172
117. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_24_last line 174
118. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_16 line 176
119. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_16_chain line 177
120. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_16_head line 180
121. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_16_last line 182
122. def OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_0 line 184
123. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_0_chain line 185
124. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_0_head line 188
125. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_0_last line 190
126. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_envelope_596_nodup line 192
127. def OAI.SnakyConditional.envelope_596 line 194
128. def OAI.SnakyConditional.childrenC_596 line 195
129. def OAI.SnakyConditional.childrenD_596 line 196
130. theorem OAI.SnakyConditional.common_sub_596 line 197
131. theorem OAI.SnakyConditional.child_required_sub_596 line 198
132. theorem OAI.SnakyConditional.Internal.SnakyRows011A.containment_596_0 line 199
133. theorem OAI.SnakyConditional.Internal.SnakyRows011A.containment_596_1 line 201
134. theorem OAI.SnakyConditional.Internal.SnakyRows011A.containment_596_2 line 203
135. theorem OAI.SnakyConditional.Internal.SnakyRows011A.containment_596_3 line 205
136. theorem OAI.SnakyConditional.Internal.SnakyRows011A.containment_596_4 line 207
137. theorem OAI.SnakyConditional.Internal.SnakyRows011A.containment_596_5 line 209
138. theorem OAI.SnakyConditional.child_envelope_sub_596 line 211
139. theorem OAI.SnakyConditional.pivot_mem_596 line 220
140. theorem OAI.SnakyConditional.children_work_596 line 221
141. theorem OAI.SnakyConditional.row_works_596 line 230
142. def OAI.SnakyConditional.required_597 line 234
143. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_4 line 235
144. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_4_chain line 236
145. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_4_head line 237
146. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_4_last line 238
147. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_5 line 239
148. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_5_chain line 240
149. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_5_head line 241
150. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_5_last line 242
151. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_3 line 243
152. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_3_chain line 244
153. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_3_head line 247
154. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_3_last line 249
155. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_7 line 251
156. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_7_chain line 252
157. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_7_head line 253
158. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_7_last line 254
159. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_8 line 255
160. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_8_chain line 256
161. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_8_head line 257
162. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_8_last line 258
163. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_6 line 259
164. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_6_chain line 260
165. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_6_head line 263
166. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_6_last line 265
167. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_2 line 267
168. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_2_chain line 268
169. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_2_head line 271
170. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_2_last line 273
171. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_11 line 275
172. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_11_chain line 276
173. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_11_head line 277
174. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_11_last line 278
175. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_12 line 279
176. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_12_chain line 280
177. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_12_head line 281
178. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_12_last line 282
179. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_10 line 283
180. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_10_chain line 284
181. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_10_head line 287
182. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_10_last line 289
183. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_14 line 291
184. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_14_chain line 292
185. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_14_head line 293
186. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_14_last line 294
187. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_15 line 295
188. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_15_chain line 296
189. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_15_head line 297
190. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_15_last line 298
191. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_13 line 299
192. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_13_chain line 300
193. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_13_head line 303
194. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_13_last line 305
195. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_9 line 307
196. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_9_chain line 308
197. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_9_head line 311
198. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_9_last line 313
199. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_1 line 315
200. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_1_chain line 316
201. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_1_head line 319
202. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_1_last line 321
203. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_19 line 323
204. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_19_chain line 324
205. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_19_head line 325
206. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_19_last line 326
207. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_20 line 327
208. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_20_chain line 328
209. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_20_head line 329
210. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_20_last line 330
211. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_18 line 331
212. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_18_chain line 332
213. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_18_head line 335
214. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_18_last line 337
215. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_22 line 339
216. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_22_chain line 340
217. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_22_head line 341
218. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_22_last line 342
219. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_23 line 343
220. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_23_chain line 344
221. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_23_head line 345
222. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_23_last line 346
223. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_21 line 347
224. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_21_chain line 348
225. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_21_head line 351
226. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_21_last line 353
227. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_17 line 355
228. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_17_chain line 356
229. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_17_head line 359
230. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_17_last line 361
231. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_26 line 363
232. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_26_chain line 364
233. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_26_head line 365
234. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_26_last line 366
235. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_27 line 367
236. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_27_chain line 368
237. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_27_head line 369
238. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_27_last line 370
239. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_25 line 371
240. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_25_chain line 372
241. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_25_head line 375
242. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_25_last line 377
243. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_29 line 379
244. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_29_chain line 380
245. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_29_head line 381
246. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_29_last line 382
247. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_30 line 383
248. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_30_chain line 384
249. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_30_head line 385
250. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_30_last line 386
251. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_28 line 387
252. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_28_chain line 388
253. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_28_head line 391
254. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_28_last line 393
255. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_24 line 395
256. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_24_chain line 396
257. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_24_head line 399
258. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_24_last line 401
259. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_16 line 403
260. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_16_chain line 404
261. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_16_head line 407
262. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_16_last line 409
263. def OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_0 line 411
264. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_0_chain line 412
265. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_0_head line 415
266. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_0_last line 417
267. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_envelope_597_nodup line 419
268. def OAI.SnakyConditional.envelope_597 line 421
269. def OAI.SnakyConditional.childrenC_597 line 422
270. def OAI.SnakyConditional.childrenD_597 line 423
271. theorem OAI.SnakyConditional.common_sub_597 line 424
272. theorem OAI.SnakyConditional.child_required_sub_597 line 425
273. theorem OAI.SnakyConditional.Internal.SnakyRows011B.containment_597_0 line 426
274. theorem OAI.SnakyConditional.Internal.SnakyRows011B.containment_597_1 line 428
275. theorem OAI.SnakyConditional.Internal.SnakyRows011B.containment_597_2 line 430
276. theorem OAI.SnakyConditional.Internal.SnakyRows011B.containment_597_3 line 432
277. theorem OAI.SnakyConditional.child_envelope_sub_597 line 434
278. theorem OAI.SnakyConditional.pivot_mem_597 line 441
279. theorem OAI.SnakyConditional.children_work_597 line 442
280. theorem OAI.SnakyConditional.row_works_597 line 449