OAI/GameTheory/SnakyConditional/Templates/Level33Part01.lean

GitHub source file

267 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_606 line 6
2. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_5 line 7
3. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_5_chain line 8
4. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_5_head line 9
5. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_5_last line 10
6. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_6 line 11
7. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_6_chain line 12
8. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_6_head line 13
9. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_6_last line 14
10. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_4 line 15
11. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_4_chain line 16
12. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_4_head line 19
13. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_4_last line 21
14. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_8 line 23
15. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_8_chain line 24
16. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_8_head line 25
17. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_8_last line 26
18. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_9 line 27
19. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_9_chain line 28
20. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_9_head line 29
21. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_9_last line 30
22. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_7 line 31
23. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_7_chain line 32
24. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_7_head line 35
25. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_7_last line 37
26. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_3 line 39
27. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_3_chain line 40
28. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_3_head line 43
29. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_3_last line 45
30. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_12 line 47
31. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_12_chain line 48
32. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_12_head line 49
33. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_12_last line 50
34. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_13 line 51
35. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_13_chain line 52
36. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_13_head line 53
37. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_13_last line 54
38. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_11 line 55
39. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_11_chain line 56
40. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_11_head line 59
41. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_11_last line 61
42. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_15 line 63
43. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_15_chain line 64
44. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_15_head line 65
45. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_15_last line 66
46. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_16 line 67
47. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_16_chain line 68
48. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_16_head line 69
49. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_16_last line 70
50. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_14 line 71
51. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_14_chain line 72
52. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_14_head line 75
53. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_14_last line 77
54. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_10 line 79
55. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_10_chain line 80
56. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_10_head line 83
57. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_10_last line 85
58. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_2 line 87
59. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_2_chain line 88
60. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_2_head line 91
61. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_2_last line 93
62. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_20 line 95
63. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_20_chain line 96
64. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_20_head line 97
65. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_20_last line 98
66. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_21 line 99
67. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_21_chain line 100
68. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_21_head line 101
69. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_21_last line 102
70. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_19 line 103
71. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_19_chain line 104
72. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_19_head line 107
73. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_19_last line 109
74. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_23 line 111
75. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_23_chain line 112
76. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_23_head line 113
77. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_23_last line 114
78. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_24 line 115
79. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_24_chain line 116
80. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_24_head line 117
81. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_24_last line 118
82. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_22 line 119
83. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_22_chain line 120
84. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_22_head line 123
85. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_22_last line 125
86. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_18 line 127
87. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_18_chain line 128
88. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_18_head line 131
89. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_18_last line 133
90. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_27 line 135
91. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_27_chain line 136
92. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_27_head line 137
93. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_27_last line 138
94. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_28 line 139
95. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_28_chain line 140
96. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_28_head line 141
97. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_28_last line 142
98. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_26 line 143
99. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_26_chain line 144
100. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_26_head line 147
101. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_26_last line 149
102. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_30 line 151
103. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_30_chain line 152
104. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_30_head line 153
105. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_30_last line 154
106. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_31 line 155
107. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_31_chain line 156
108. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_31_head line 157
109. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_31_last line 158
110. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_29 line 159
111. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_29_chain line 160
112. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_29_head line 163
113. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_29_last line 165
114. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_25 line 167
115. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_25_chain line 168
116. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_25_head line 171
117. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_25_last line 173
118. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_17 line 175
119. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_17_chain line 176
120. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_17_head line 179
121. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_17_last line 181
122. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_1 line 183
123. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_1_chain line 184
124. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_1_head line 187
125. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_1_last line 189
126. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_36 line 191
127. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_36_chain line 192
128. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_36_head line 193
129. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_36_last line 194
130. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_37 line 195
131. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_37_chain line 196
132. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_37_head line 197
133. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_37_last line 198
134. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_35 line 199
135. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_35_chain line 200
136. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_35_head line 203
137. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_35_last line 205
138. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_39 line 207
139. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_39_chain line 208
140. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_39_head line 209
141. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_39_last line 210
142. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_40 line 211
143. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_40_chain line 212
144. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_40_head line 213
145. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_40_last line 214
146. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_38 line 215
147. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_38_chain line 216
148. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_38_head line 219
149. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_38_last line 221
150. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_34 line 223
151. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_34_chain line 224
152. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_34_head line 227
153. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_34_last line 229
154. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_43 line 231
155. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_43_chain line 232
156. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_43_head line 233
157. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_43_last line 234
158. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_44 line 235
159. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_44_chain line 236
160. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_44_head line 237
161. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_44_last line 238
162. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_42 line 239
163. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_42_chain line 240
164. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_42_head line 243
165. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_42_last line 245
166. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_46 line 247
167. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_46_chain line 248
168. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_46_head line 249
169. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_46_last line 250
170. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_47 line 251
171. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_47_chain line 252
172. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_47_head line 253
173. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_47_last line 254
174. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_45 line 255
175. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_45_chain line 256
176. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_45_head line 259
177. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_45_last line 261
178. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_41 line 263
179. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_41_chain line 264
180. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_41_head line 267
181. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_41_last line 269
182. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_33 line 271
183. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_33_chain line 272
184. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_33_head line 275
185. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_33_last line 277
186. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_51 line 279
187. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_51_chain line 280
188. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_51_head line 281
189. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_51_last line 282
190. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_52 line 283
191. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_52_chain line 284
192. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_52_head line 285
193. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_52_last line 286
194. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_50 line 287
195. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_50_chain line 288
196. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_50_head line 291
197. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_50_last line 293
198. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_54 line 295
199. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_54_chain line 296
200. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_54_head line 297
201. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_54_last line 298
202. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_55 line 299
203. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_55_chain line 300
204. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_55_head line 301
205. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_55_last line 302
206. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_53 line 303
207. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_53_chain line 304
208. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_53_head line 307
209. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_53_last line 309
210. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_49 line 311
211. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_49_chain line 312
212. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_49_head line 315
213. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_49_last line 317
214. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_58 line 319
215. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_58_chain line 320
216. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_58_head line 321
217. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_58_last line 322
218. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_59 line 323
219. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_59_chain line 324
220. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_59_head line 325
221. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_59_last line 326
222. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_57 line 327
223. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_57_chain line 328
224. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_57_head line 331
225. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_57_last line 333
226. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_61 line 335
227. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_61_chain line 336
228. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_61_head line 337
229. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_61_last line 338
230. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_62 line 339
231. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_62_chain line 340
232. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_62_head line 341
233. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_62_last line 342
234. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_60 line 343
235. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_60_chain line 344
236. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_60_head line 347
237. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_60_last line 349
238. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_56 line 351
239. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_56_chain line 352
240. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_56_head line 355
241. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_56_last line 357
242. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_48 line 359
243. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_48_chain line 360
244. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_48_head line 363
245. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_48_last line 365
246. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_32 line 367
247. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_32_chain line 368
248. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_32_head line 371
249. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_32_last line 373
250. def OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_0 line 375
251. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_0_chain line 376
252. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_0_head line 379
253. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_0_last line 381
254. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_envelope_606_nodup line 383
255. def OAI.SnakyConditional.envelope_606 line 385
256. def OAI.SnakyConditional.childrenC_606 line 386
257. def OAI.SnakyConditional.childrenD_606 line 387
258. theorem OAI.SnakyConditional.common_sub_606 line 388
259. theorem OAI.SnakyConditional.child_required_sub_606 line 389
260. theorem OAI.SnakyConditional.Internal.SnakyRows012A.containment_606_0 line 390
261. theorem OAI.SnakyConditional.Internal.SnakyRows012A.containment_606_1 line 392
262. theorem OAI.SnakyConditional.Internal.SnakyRows012A.containment_606_2 line 394
263. theorem OAI.SnakyConditional.Internal.SnakyRows012A.containment_606_3 line 396
264. theorem OAI.SnakyConditional.child_envelope_sub_606 line 398
265. theorem OAI.SnakyConditional.pivot_mem_606 line 405
266. theorem OAI.SnakyConditional.children_work_606 line 406
267. theorem OAI.SnakyConditional.row_works_606 line 413