OAI/GameTheory/SnakyConditional/Templates/Level34Part01.lean

GitHub source file

349 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_608 line 10
2. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_5 line 11
3. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_5_chain line 12
4. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_5_head line 13
5. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_5_last line 14
6. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_6 line 15
7. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_6_chain line 16
8. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_6_head line 17
9. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_6_last line 18
10. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_4 line 19
11. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_4_chain line 20
12. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_4_head line 23
13. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_4_last line 25
14. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_8 line 27
15. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_8_chain line 28
16. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_8_head line 29
17. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_8_last line 30
18. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_9 line 31
19. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_9_chain line 32
20. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_9_head line 33
21. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_9_last line 34
22. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_7 line 35
23. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_7_chain line 36
24. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_7_head line 39
25. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_7_last line 41
26. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_3 line 43
27. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_3_chain line 44
28. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_3_head line 47
29. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_3_last line 49
30. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_12 line 51
31. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_12_chain line 52
32. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_12_head line 53
33. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_12_last line 54
34. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_13 line 55
35. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_13_chain line 56
36. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_13_head line 57
37. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_13_last line 58
38. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_11 line 59
39. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_11_chain line 60
40. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_11_head line 63
41. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_11_last line 65
42. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_15 line 67
43. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_15_chain line 68
44. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_15_head line 69
45. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_15_last line 70
46. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_16 line 71
47. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_16_chain line 72
48. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_16_head line 73
49. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_16_last line 74
50. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_14 line 75
51. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_14_chain line 76
52. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_14_head line 79
53. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_14_last line 81
54. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_10 line 83
55. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_10_chain line 84
56. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_10_head line 87
57. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_10_last line 89
58. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_2 line 91
59. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_2_chain line 92
60. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_2_head line 95
61. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_2_last line 97
62. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_20 line 99
63. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_20_chain line 100
64. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_20_head line 101
65. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_20_last line 102
66. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_21 line 103
67. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_21_chain line 104
68. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_21_head line 105
69. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_21_last line 106
70. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_19 line 107
71. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_19_chain line 108
72. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_19_head line 111
73. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_19_last line 113
74. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_23 line 115
75. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_23_chain line 116
76. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_23_head line 117
77. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_23_last line 118
78. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_24 line 119
79. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_24_chain line 120
80. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_24_head line 121
81. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_24_last line 122
82. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_22 line 123
83. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_22_chain line 124
84. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_22_head line 127
85. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_22_last line 129
86. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_18 line 131
87. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_18_chain line 132
88. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_18_head line 135
89. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_18_last line 137
90. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_27 line 139
91. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_27_chain line 140
92. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_27_head line 141
93. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_27_last line 142
94. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_28 line 143
95. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_28_chain line 144
96. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_28_head line 145
97. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_28_last line 146
98. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_26 line 147
99. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_26_chain line 148
100. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_26_head line 151
101. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_26_last line 153
102. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_30 line 155
103. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_30_chain line 156
104. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_30_head line 157
105. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_30_last line 158
106. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_31 line 159
107. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_31_chain line 160
108. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_31_head line 161
109. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_31_last line 162
110. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_29 line 163
111. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_29_chain line 164
112. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_29_head line 167
113. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_29_last line 169
114. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_25 line 171
115. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_25_chain line 172
116. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_25_head line 175
117. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_25_last line 177
118. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_17 line 179
119. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_17_chain line 180
120. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_17_head line 183
121. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_17_last line 185
122. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_1 line 187
123. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_1_chain line 188
124. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_1_head line 191
125. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_1_last line 193
126. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_36 line 195
127. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_36_chain line 196
128. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_36_head line 197
129. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_36_last line 198
130. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_37 line 199
131. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_37_chain line 200
132. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_37_head line 201
133. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_37_last line 202
134. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_35 line 203
135. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_35_chain line 204
136. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_35_head line 207
137. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_35_last line 209
138. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_39 line 211
139. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_39_chain line 212
140. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_39_head line 213
141. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_39_last line 214
142. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_40 line 215
143. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_40_chain line 216
144. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_40_head line 217
145. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_40_last line 218
146. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_38 line 219
147. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_38_chain line 220
148. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_38_head line 223
149. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_38_last line 225
150. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_34 line 227
151. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_34_chain line 228
152. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_34_head line 231
153. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_34_last line 233
154. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_43 line 235
155. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_43_chain line 236
156. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_43_head line 237
157. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_43_last line 238
158. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_44 line 239
159. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_44_chain line 240
160. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_44_head line 241
161. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_44_last line 242
162. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_42 line 243
163. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_42_chain line 244
164. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_42_head line 247
165. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_42_last line 249
166. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_46 line 251
167. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_46_chain line 252
168. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_46_head line 253
169. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_46_last line 254
170. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_47 line 255
171. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_47_chain line 256
172. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_47_head line 257
173. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_47_last line 258
174. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_45 line 259
175. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_45_chain line 260
176. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_45_head line 263
177. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_45_last line 265
178. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_41 line 267
179. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_41_chain line 268
180. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_41_head line 271
181. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_41_last line 273
182. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_33 line 275
183. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_33_chain line 276
184. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_33_head line 279
185. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_33_last line 281
186. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_51 line 283
187. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_51_chain line 284
188. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_51_head line 285
189. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_51_last line 286
190. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_52 line 287
191. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_52_chain line 288
192. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_52_head line 289
193. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_52_last line 290
194. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_50 line 291
195. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_50_chain line 292
196. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_50_head line 295
197. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_50_last line 297
198. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_54 line 299
199. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_54_chain line 300
200. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_54_head line 301
201. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_54_last line 302
202. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_55 line 303
203. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_55_chain line 304
204. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_55_head line 305
205. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_55_last line 306
206. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_53 line 307
207. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_53_chain line 308
208. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_53_head line 311
209. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_53_last line 313
210. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_49 line 315
211. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_49_chain line 316
212. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_49_head line 319
213. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_49_last line 321
214. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_58 line 323
215. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_58_chain line 324
216. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_58_head line 325
217. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_58_last line 326
218. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_59 line 327
219. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_59_chain line 328
220. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_59_head line 329
221. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_59_last line 330
222. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_57 line 331
223. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_57_chain line 332
224. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_57_head line 335
225. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_57_last line 337
226. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_61 line 339
227. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_61_chain line 340
228. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_61_head line 341
229. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_61_last line 342
230. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_62 line 343
231. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_62_chain line 344
232. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_62_head line 345
233. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_62_last line 346
234. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_60 line 347
235. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_60_chain line 348
236. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_60_head line 351
237. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_60_last line 353
238. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_56 line 355
239. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_56_chain line 356
240. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_56_head line 359
241. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_56_last line 361
242. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_48 line 363
243. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_48_chain line 364
244. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_48_head line 367
245. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_48_last line 369
246. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_32 line 371
247. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_32_chain line 372
248. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_32_head line 375
249. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_32_last line 377
250. def OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_0 line 379
251. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_0_chain line 380
252. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_0_head line 383
253. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_0_last line 385
254. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_envelope_608_nodup line 387
255. def OAI.SnakyConditional.envelope_608 line 389
256. def OAI.SnakyConditional.childrenC_608 line 390
257. def OAI.SnakyConditional.childrenD_608 line 391
258. theorem OAI.SnakyConditional.common_sub_608 line 392
259. theorem OAI.SnakyConditional.child_required_sub_608 line 393
260. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_0_points_0 line 394
261. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_0_points_1 line 397
262. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_0_points_2 line 400
263. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_0 line 403
264. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_1_points_0 line 408
265. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_1_points_1 line 411
266. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_1_points_2 line 414
267. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_1_points_3 line 417
268. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_1 line 420
269. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_0 line 425
270. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_1 line 428
271. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_2 line 431
272. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_3 line 434
273. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_4 line 437
274. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_5 line 440
275. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_6 line 443
276. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_7 line 446
277. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_8 line 449
278. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2_points_9 line 452
279. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_2 line 455
280. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_3_points_0 line 460
281. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_3_points_1 line 463
282. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_3_points_2 line 466
283. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_3_points_3 line 469
284. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_3 line 472
285. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_0 line 477
286. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_1 line 480
287. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_2 line 483
288. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_3 line 486
289. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_4 line 489
290. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_5 line 492
291. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_6 line 495
292. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_7 line 498
293. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_8 line 501
294. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4_points_9 line 504
295. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_4 line 507
296. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_0 line 512
297. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_1 line 515
298. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_2 line 518
299. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_3 line 521
300. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_4 line 524
301. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_5 line 527
302. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_6 line 530
303. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_7 line 533
304. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_8 line 536
305. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_9 line 539
306. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_10 line 542
307. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_11 line 545
308. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5_points_12 line 548
309. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_5 line 551
310. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_0 line 556
311. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_1 line 559
312. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_2 line 562
313. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_3 line 565
314. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_4 line 568
315. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_5 line 571
316. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_6 line 574
317. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_7 line 577
318. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_8 line 580
319. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_9 line 583
320. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_10 line 586
321. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_11 line 589
322. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_12 line 592
323. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_13 line 595
324. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6_points_14 line 598
325. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_6 line 601
326. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_0 line 603
327. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_1 line 606
328. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_2 line 609
329. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_3 line 612
330. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_4 line 615
331. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_5 line 618
332. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_6 line 621
333. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_7 line 624
334. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_8 line 627
335. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_9 line 630
336. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_10 line 633
337. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_11 line 636
338. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_12 line 639
339. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_13 line 642
340. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_14 line 645
341. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_15 line 648
342. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_16 line 651
343. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_17 line 654
344. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7_points_18 line 657
345. theorem OAI.SnakyConditional.Internal.SnakyRows012C.containment_608_7 line 660
346. theorem OAI.SnakyConditional.child_envelope_sub_608 line 662
347. theorem OAI.SnakyConditional.pivot_mem_608 line 673
348. theorem OAI.SnakyConditional.children_work_608 line 674
349. theorem OAI.SnakyConditional.row_works_608 line 685