OAI/GameTheory/SnakyConditional/Regions/Region603.lean

GitHub source file

249 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.Internal.SnakyRows011H.namedCellKey line 6
2. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_nodup_of_chain line 7
3. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_chain_append line 10
4. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_head_append line 24
5. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_last_append line 29
6. theorem OAI.SnakyConditional.Internal.SnakyRows011H.required_603_nodup line 34
7. def OAI.SnakyConditional.required_603 line 36
8. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_5 line 38
9. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_5_chain line 39
10. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_5_last line 40
11. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_6 line 41
12. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_6_chain line 42
13. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_6_head line 43
14. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_6_last line 44
15. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_4 line 45
16. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_4_chain line 46
17. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_4_last line 49
18. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_8 line 51
19. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_8_chain line 52
20. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_8_head line 53
21. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_8_last line 54
22. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_9 line 55
23. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_9_chain line 56
24. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_9_head line 57
25. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_9_last line 58
26. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_7 line 59
27. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_7_chain line 60
28. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_7_head line 63
29. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_7_last line 65
30. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_3 line 67
31. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_3_chain line 68
32. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_3_last line 71
33. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_12 line 73
34. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_12_chain line 74
35. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_12_head line 75
36. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_12_last line 76
37. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_13 line 77
38. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_13_chain line 78
39. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_13_head line 79
40. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_13_last line 80
41. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_11 line 81
42. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_11_chain line 82
43. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_11_head line 85
44. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_11_last line 87
45. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_15 line 89
46. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_15_chain line 90
47. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_15_head line 91
48. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_15_last line 92
49. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_16 line 93
50. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_16_chain line 94
51. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_16_head line 95
52. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_16_last line 96
53. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_14 line 97
54. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_14_chain line 98
55. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_14_head line 101
56. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_14_last line 103
57. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_10 line 105
58. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_10_chain line 106
59. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_10_head line 109
60. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_10_last line 111
61. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_2 line 113
62. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_2_chain line 114
63. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_2_last line 117
64. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_20 line 119
65. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_20_chain line 120
66. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_20_head line 121
67. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_20_last line 122
68. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_21 line 123
69. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_21_chain line 124
70. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_21_head line 125
71. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_21_last line 126
72. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_19 line 127
73. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_19_chain line 128
74. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_19_head line 131
75. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_19_last line 133
76. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_23 line 135
77. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_23_chain line 136
78. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_23_head line 137
79. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_23_last line 138
80. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_24 line 139
81. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_24_chain line 140
82. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_24_head line 141
83. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_24_last line 142
84. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_22 line 143
85. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_22_chain line 144
86. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_22_head line 147
87. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_22_last line 149
88. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_18 line 151
89. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_18_chain line 152
90. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_18_head line 155
91. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_18_last line 157
92. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_27 line 159
93. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_27_chain line 160
94. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_27_head line 161
95. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_27_last line 162
96. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_28 line 163
97. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_28_chain line 164
98. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_28_head line 165
99. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_28_last line 166
100. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_26 line 167
101. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_26_chain line 168
102. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_26_head line 171
103. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_26_last line 173
104. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_30 line 175
105. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_30_chain line 176
106. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_30_head line 177
107. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_30_last line 178
108. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_31 line 179
109. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_31_chain line 180
110. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_31_head line 181
111. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_31_last line 182
112. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_29 line 183
113. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_29_chain line 184
114. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_29_head line 187
115. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_29_last line 189
116. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_25 line 191
117. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_25_chain line 192
118. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_25_head line 195
119. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_25_last line 197
120. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_17 line 199
121. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_17_chain line 200
122. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_17_head line 203
123. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_17_last line 205
124. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_1 line 207
125. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_1_chain line 208
126. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_1_last line 211
127. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_36 line 213
128. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_36_chain line 214
129. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_36_head line 215
130. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_36_last line 216
131. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_37 line 217
132. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_37_chain line 218
133. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_37_head line 219
134. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_37_last line 220
135. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_35 line 221
136. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_35_chain line 222
137. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_35_head line 225
138. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_35_last line 227
139. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_39 line 229
140. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_39_chain line 230
141. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_39_head line 231
142. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_39_last line 232
143. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_40 line 233
144. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_40_chain line 234
145. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_40_head line 235
146. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_40_last line 236
147. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_38 line 237
148. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_38_chain line 238
149. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_38_head line 241
150. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_38_last line 243
151. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_34 line 245
152. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_34_chain line 246
153. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_34_head line 249
154. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_34_last line 251
155. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_43 line 253
156. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_43_chain line 254
157. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_43_head line 255
158. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_43_last line 256
159. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_44 line 257
160. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_44_chain line 258
161. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_44_head line 259
162. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_44_last line 260
163. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_42 line 261
164. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_42_chain line 262
165. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_42_head line 265
166. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_42_last line 267
167. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_46 line 269
168. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_46_chain line 270
169. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_46_head line 271
170. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_46_last line 272
171. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_47 line 273
172. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_47_chain line 274
173. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_47_head line 275
174. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_47_last line 276
175. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_45 line 277
176. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_45_chain line 278
177. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_45_head line 281
178. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_45_last line 283
179. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_41 line 285
180. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_41_chain line 286
181. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_41_head line 289
182. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_41_last line 291
183. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_33 line 293
184. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_33_chain line 294
185. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_33_head line 297
186. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_33_last line 299
187. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_51 line 301
188. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_51_chain line 302
189. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_51_head line 303
190. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_51_last line 304
191. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_52 line 305
192. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_52_chain line 306
193. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_52_head line 307
194. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_52_last line 308
195. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_50 line 309
196. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_50_chain line 310
197. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_50_head line 313
198. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_50_last line 315
199. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_54 line 317
200. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_54_chain line 318
201. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_54_head line 319
202. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_54_last line 320
203. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_55 line 321
204. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_55_chain line 322
205. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_55_head line 323
206. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_55_last line 324
207. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_53 line 325
208. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_53_chain line 326
209. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_53_head line 329
210. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_53_last line 331
211. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_49 line 333
212. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_49_chain line 334
213. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_49_head line 337
214. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_49_last line 339
215. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_58 line 341
216. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_58_chain line 342
217. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_58_head line 343
218. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_58_last line 344
219. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_59 line 345
220. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_59_chain line 346
221. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_59_head line 347
222. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_59_last line 348
223. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_57 line 349
224. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_57_chain line 350
225. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_57_head line 353
226. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_57_last line 355
227. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_61 line 357
228. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_61_chain line 358
229. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_61_head line 359
230. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_61_last line 360
231. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_62 line 361
232. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_62_chain line 362
233. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_62_head line 363
234. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_60 line 364
235. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_60_chain line 365
236. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_60_head line 368
237. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_56 line 370
238. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_56_chain line 371
239. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_56_head line 374
240. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_48 line 376
241. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_48_chain line 377
242. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_48_head line 380
243. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_32 line 382
244. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_32_chain line 383
245. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_32_head line 386
246. def OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_0 line 388
247. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_0_chain line 389
248. theorem OAI.SnakyConditional.Internal.SnakyRows011H.named_envelope_603_nodup line 392
249. def OAI.SnakyConditional.envelope_603 line 394