OAI/GameTheory/SnakyTwentyOne/Cards/Height05Part03.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_272 line 16
  2. def OAI.SnakyPrototype.Certificate21.envelope_272 line 17
  3. def OAI.SnakyPrototype.Certificate21.childrenC_272 line 18
  4. def OAI.SnakyPrototype.Certificate21.childrenD_272 line 19
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_272 line 20
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_272 line 21
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_272 line 22
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_272 line 23
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_272 line 24
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_272 line 29
  11. def OAI.SnakyPrototype.Certificate21.required_273 line 34
  12. def OAI.SnakyPrototype.Certificate21.envelope_273 line 35
  13. def OAI.SnakyPrototype.Certificate21.childrenC_273 line 36
  14. def OAI.SnakyPrototype.Certificate21.childrenD_273 line 37
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_273 line 38
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_273 line 39
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_273 line 40
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_273 line 41
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_273 line 42
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_273 line 47
  21. def OAI.SnakyPrototype.Certificate21.required_274 line 52
  22. def OAI.SnakyPrototype.Certificate21.envelope_274 line 53
  23. def OAI.SnakyPrototype.Certificate21.childrenC_274 line 54
  24. def OAI.SnakyPrototype.Certificate21.childrenD_274 line 55
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_274 line 56
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_274 line 57
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_274 line 58
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_274 line 59
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_274 line 60
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_274 line 66
  31. def OAI.SnakyPrototype.Certificate21.required_278 line 71
  32. def OAI.SnakyPrototype.Certificate21.envelope_278 line 72
  33. def OAI.SnakyPrototype.Certificate21.childrenC_278 line 73
  34. def OAI.SnakyPrototype.Certificate21.childrenD_278 line 74
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_278 line 75
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_278 line 76
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_278 line 77
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_278 line 78
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_278 line 79
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_278 line 84
  41. def OAI.SnakyPrototype.Certificate21.required_279 line 89
  42. def OAI.SnakyPrototype.Certificate21.envelope_279 line 90
  43. def OAI.SnakyPrototype.Certificate21.childrenC_279 line 91
  44. def OAI.SnakyPrototype.Certificate21.childrenD_279 line 92
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_279 line 93
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_279 line 94
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_279 line 95
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_279 line 96
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_279 line 97
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_279 line 102
  51. def OAI.SnakyPrototype.Certificate21.required_282 line 107
  52. def OAI.SnakyPrototype.Certificate21.envelope_282 line 108
  53. def OAI.SnakyPrototype.Certificate21.childrenC_282 line 109
  54. def OAI.SnakyPrototype.Certificate21.childrenD_282 line 110
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_282 line 111
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_282 line 112
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_282 line 113
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_282 line 114
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_282 line 115
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_282 line 121
  61. def OAI.SnakyPrototype.Certificate21.required_293 line 126
  62. def OAI.SnakyPrototype.Certificate21.envelope_293 line 127
  63. def OAI.SnakyPrototype.Certificate21.childrenC_293 line 128
  64. def OAI.SnakyPrototype.Certificate21.childrenD_293 line 129
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_293 line 130
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_293 line 131
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_293 line 132
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_293 line 133
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_293 line 134
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_293 line 139
  71. def OAI.SnakyPrototype.Certificate21.required_294 line 144
  72. def OAI.SnakyPrototype.Certificate21.envelope_294 line 145
  73. def OAI.SnakyPrototype.Certificate21.childrenC_294 line 146
  74. def OAI.SnakyPrototype.Certificate21.childrenD_294 line 147
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_294 line 148
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_294 line 149
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_294 line 150
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_294 line 151
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_294 line 152
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_294 line 158
  81. def OAI.SnakyPrototype.Certificate21.required_296 line 163
  82. def OAI.SnakyPrototype.Certificate21.envelope_296 line 164
  83. def OAI.SnakyPrototype.Certificate21.childrenC_296 line 165
  84. def OAI.SnakyPrototype.Certificate21.childrenD_296 line 166
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_296 line 167
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_296 line 168
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_296 line 169
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_296 line 170
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_296 line 171
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_296 line 176
  91. def OAI.SnakyPrototype.Certificate21.required_299 line 181
  92. def OAI.SnakyPrototype.Certificate21.envelope_299 line 182
  93. def OAI.SnakyPrototype.Certificate21.childrenC_299 line 183
  94. def OAI.SnakyPrototype.Certificate21.childrenD_299 line 184
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_299 line 185
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_299 line 186
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_299 line 187
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_299 line 188
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_299 line 189
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_299 line 195
  101. def OAI.SnakyPrototype.Certificate21.required_301 line 200
  102. def OAI.SnakyPrototype.Certificate21.envelope_301 line 201
  103. def OAI.SnakyPrototype.Certificate21.childrenC_301 line 202
  104. def OAI.SnakyPrototype.Certificate21.childrenD_301 line 203
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_301 line 204
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_301 line 205
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_301 line 206
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_301 line 207
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_301 line 208
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_301 line 213
  111. def OAI.SnakyPrototype.Certificate21.required_306 line 218
  112. def OAI.SnakyPrototype.Certificate21.envelope_306 line 219
  113. def OAI.SnakyPrototype.Certificate21.childrenC_306 line 220
  114. def OAI.SnakyPrototype.Certificate21.childrenD_306 line 221
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_306 line 222
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_306 line 223
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_306 line 224
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_306 line 225
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_306 line 226
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_306 line 231
  121. def OAI.SnakyPrototype.Certificate21.required_308 line 236
  122. def OAI.SnakyPrototype.Certificate21.envelope_308 line 237
  123. def OAI.SnakyPrototype.Certificate21.childrenC_308 line 238
  124. def OAI.SnakyPrototype.Certificate21.childrenD_308 line 239
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_308 line 240
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_308 line 241
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_308 line 242
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_308 line 243
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_308 line 244
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_308 line 251
  131. def OAI.SnakyPrototype.Certificate21.required_312 line 256
  132. def OAI.SnakyPrototype.Certificate21.envelope_312 line 257
  133. def OAI.SnakyPrototype.Certificate21.childrenC_312 line 258
  134. def OAI.SnakyPrototype.Certificate21.childrenD_312 line 259
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_312 line 260
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_312 line 261
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_312 line 262
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_312 line 263
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_312 line 264
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_312 line 269
  141. def OAI.SnakyPrototype.Certificate21.required_314_i0 line 274
  142. def OAI.SnakyPrototype.Certificate21.envelope_314_i0 line 275
  143. def OAI.SnakyPrototype.Certificate21.childrenC_314_i0 line 276
  144. def OAI.SnakyPrototype.Certificate21.childrenD_314_i0 line 277
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_314_i0 line 278
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_314_i0 line 279
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_314_i0 line 280
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_314_i0 line 281
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_314_i0 line 282
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_314_i0 line 287
  151. def OAI.SnakyPrototype.Certificate21.required_314 line 292
  152. def OAI.SnakyPrototype.Certificate21.envelope_314 line 293
  153. def OAI.SnakyPrototype.Certificate21.childrenC_314 line 294
  154. def OAI.SnakyPrototype.Certificate21.childrenD_314 line 295
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_314 line 296
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_314 line 297
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_314 line 298
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_314 line 299
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_314 line 300
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_314 line 307
  161. def OAI.SnakyPrototype.Certificate21.required_335 line 312
  162. def OAI.SnakyPrototype.Certificate21.envelope_335 line 313
  163. def OAI.SnakyPrototype.Certificate21.childrenC_335 line 314
  164. def OAI.SnakyPrototype.Certificate21.childrenD_335 line 315
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_335 line 316
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_335 line 317
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_335 line 318
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_335 line 319
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_335 line 320
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_335 line 325
  171. def OAI.SnakyPrototype.Certificate21.required_342_i0 line 330
  172. def OAI.SnakyPrototype.Certificate21.envelope_342_i0 line 331
  173. def OAI.SnakyPrototype.Certificate21.childrenC_342_i0 line 332
  174. def OAI.SnakyPrototype.Certificate21.childrenD_342_i0 line 333
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_342_i0 line 334
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_342_i0 line 335
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_342_i0 line 336
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_342_i0 line 337
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_342_i0 line 338
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_342_i0 line 343
  181. def OAI.SnakyPrototype.Certificate21.required_342 line 348
  182. def OAI.SnakyPrototype.Certificate21.envelope_342 line 349
  183. def OAI.SnakyPrototype.Certificate21.childrenC_342 line 350
  184. def OAI.SnakyPrototype.Certificate21.childrenD_342 line 351
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_342 line 352
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_342 line 353
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_342 line 354
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_342 line 355
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_342 line 356
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_342 line 361
  191. def OAI.SnakyPrototype.Certificate21.required_347_i1 line 366
  192. def OAI.SnakyPrototype.Certificate21.envelope_347_i1 line 367
  193. def OAI.SnakyPrototype.Certificate21.childrenC_347_i1 line 368
  194. def OAI.SnakyPrototype.Certificate21.childrenD_347_i1 line 369
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_347_i1 line 370
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_347_i1 line 371
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_347_i1 line 372
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_347_i1 line 373
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_347_i1 line 374
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_347_i1 line 379
  201. def OAI.SnakyPrototype.Certificate21.required_347_i0 line 384
  202. def OAI.SnakyPrototype.Certificate21.envelope_347_i0 line 385
  203. def OAI.SnakyPrototype.Certificate21.childrenC_347_i0 line 386
  204. def OAI.SnakyPrototype.Certificate21.childrenD_347_i0 line 387
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_347_i0 line 388
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_347_i0 line 389
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_347_i0 line 390
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_347_i0 line 391
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_347_i0 line 392
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_347_i0 line 397
  211. def OAI.SnakyPrototype.Certificate21.required_347 line 402
  212. def OAI.SnakyPrototype.Certificate21.envelope_347 line 403
  213. def OAI.SnakyPrototype.Certificate21.childrenC_347 line 404
  214. def OAI.SnakyPrototype.Certificate21.childrenD_347 line 405
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_347 line 406
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_347 line 407
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_347 line 408
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_347 line 409
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_347 line 410
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_347 line 416
  221. def OAI.SnakyPrototype.Certificate21.required_352 line 421
  222. def OAI.SnakyPrototype.Certificate21.envelope_352 line 422
  223. def OAI.SnakyPrototype.Certificate21.childrenC_352 line 423
  224. def OAI.SnakyPrototype.Certificate21.childrenD_352 line 424
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_352 line 425
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_352 line 426
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_352 line 427
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_352 line 428
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_352 line 429
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_352 line 434
  231. def OAI.SnakyPrototype.Certificate21.required_355 line 439
  232. def OAI.SnakyPrototype.Certificate21.envelope_355 line 440
  233. def OAI.SnakyPrototype.Certificate21.childrenC_355 line 441
  234. def OAI.SnakyPrototype.Certificate21.childrenD_355 line 442
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_355 line 443
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_355 line 444
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_355 line 445
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_355 line 446
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_355 line 447
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_355 line 452
  241. def OAI.SnakyPrototype.Certificate21.height_272 line 457
  242. def OAI.SnakyPrototype.Certificate21.childrenH_272 line 458
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_272 line 459
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_272 line 460
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_272 line 462
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_272 line 466
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_272 line 468
  248. def OAI.SnakyPrototype.Certificate21.checked_272 line 472
  249. def OAI.SnakyPrototype.Certificate21.height_273 line 480
  250. def OAI.SnakyPrototype.Certificate21.childrenH_273 line 481
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_273 line 482
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_273 line 483
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_273 line 485
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_273 line 489
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_273 line 491
  256. def OAI.SnakyPrototype.Certificate21.checked_273 line 495
  257. def OAI.SnakyPrototype.Certificate21.height_274 line 503
  258. def OAI.SnakyPrototype.Certificate21.childrenH_274 line 504
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_274 line 505
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_274 line 506
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_274 line 508
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_274 line 512
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_274 line 514
  264. def OAI.SnakyPrototype.Certificate21.checked_274 line 518
  265. def OAI.SnakyPrototype.Certificate21.height_278 line 526
  266. def OAI.SnakyPrototype.Certificate21.childrenH_278 line 527
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_278 line 528
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_278 line 529
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_278 line 531
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_278 line 535
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_278 line 537
  272. def OAI.SnakyPrototype.Certificate21.checked_278 line 541
  273. def OAI.SnakyPrototype.Certificate21.height_279 line 549
  274. def OAI.SnakyPrototype.Certificate21.childrenH_279 line 550
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_279 line 551
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_279 line 552
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_279 line 554
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_279 line 558
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_279 line 560
  280. def OAI.SnakyPrototype.Certificate21.checked_279 line 564
  281. def OAI.SnakyPrototype.Certificate21.height_282 line 572
  282. def OAI.SnakyPrototype.Certificate21.childrenH_282 line 573
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_282 line 574
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_282 line 575
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_282 line 577
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_282 line 581
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_282 line 583
  288. def OAI.SnakyPrototype.Certificate21.checked_282 line 587
  289. def OAI.SnakyPrototype.Certificate21.height_293 line 595
  290. def OAI.SnakyPrototype.Certificate21.childrenH_293 line 596
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_293 line 597
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_293 line 598
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_293 line 600
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_293 line 604
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_293 line 606
  296. def OAI.SnakyPrototype.Certificate21.checked_293 line 610
  297. def OAI.SnakyPrototype.Certificate21.height_294 line 618
  298. def OAI.SnakyPrototype.Certificate21.childrenH_294 line 619
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_294 line 620
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_294 line 621
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_294 line 623
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_294 line 627
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_294 line 629
  304. def OAI.SnakyPrototype.Certificate21.checked_294 line 633
  305. def OAI.SnakyPrototype.Certificate21.height_296 line 641
  306. def OAI.SnakyPrototype.Certificate21.childrenH_296 line 642
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_296 line 643
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_296 line 644
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_296 line 646
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_296 line 650
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_296 line 652
  312. def OAI.SnakyPrototype.Certificate21.checked_296 line 656
  313. def OAI.SnakyPrototype.Certificate21.height_299 line 664
  314. def OAI.SnakyPrototype.Certificate21.childrenH_299 line 665
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_299 line 666
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_299 line 667
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_299 line 669
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_299 line 673
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_299 line 675
  320. def OAI.SnakyPrototype.Certificate21.checked_299 line 679
  321. def OAI.SnakyPrototype.Certificate21.height_301 line 687
  322. def OAI.SnakyPrototype.Certificate21.childrenH_301 line 688
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_301 line 689
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_301 line 690
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_301 line 692
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_301 line 696
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_301 line 698
  328. def OAI.SnakyPrototype.Certificate21.checked_301 line 702
  329. def OAI.SnakyPrototype.Certificate21.height_306 line 710
  330. def OAI.SnakyPrototype.Certificate21.childrenH_306 line 711
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_306 line 712
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_306 line 713
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_306 line 715
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_306 line 719
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_306 line 721
  336. def OAI.SnakyPrototype.Certificate21.checked_306 line 725
  337. def OAI.SnakyPrototype.Certificate21.height_308 line 733
  338. def OAI.SnakyPrototype.Certificate21.childrenH_308 line 734
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_308 line 735
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_308 line 736
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_308 line 738
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_308 line 742
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_308 line 744
  344. def OAI.SnakyPrototype.Certificate21.checked_308 line 748
  345. def OAI.SnakyPrototype.Certificate21.height_312 line 756
  346. def OAI.SnakyPrototype.Certificate21.childrenH_312 line 757
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_312 line 758
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_312 line 759
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_312 line 761
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_312 line 765
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_312 line 767
  352. def OAI.SnakyPrototype.Certificate21.checked_312 line 771
  353. def OAI.SnakyPrototype.Certificate21.height_314_i0 line 779
  354. def OAI.SnakyPrototype.Certificate21.childrenH_314_i0 line 780
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_314_i0 line 781
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_314_i0 line 782
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_314_i0 line 784
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_314_i0 line 788
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_314_i0 line 790
  360. def OAI.SnakyPrototype.Certificate21.checked_314_i0 line 794
  361. def OAI.SnakyPrototype.Certificate21.height_314 line 802
  362. def OAI.SnakyPrototype.Certificate21.childrenH_314 line 803
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_314 line 804
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_314 line 805
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_314 line 807
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_314 line 811
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_314 line 813
  368. def OAI.SnakyPrototype.Certificate21.checked_314 line 817
  369. def OAI.SnakyPrototype.Certificate21.height_335 line 825
  370. def OAI.SnakyPrototype.Certificate21.childrenH_335 line 826
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_335 line 827
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_335 line 828
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_335 line 830
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_335 line 834
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_335 line 836
  376. def OAI.SnakyPrototype.Certificate21.checked_335 line 840
  377. def OAI.SnakyPrototype.Certificate21.height_342_i0 line 848
  378. def OAI.SnakyPrototype.Certificate21.childrenH_342_i0 line 849
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_342_i0 line 850
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_342_i0 line 851
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_342_i0 line 853
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_342_i0 line 857
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_342_i0 line 859
  384. def OAI.SnakyPrototype.Certificate21.checked_342_i0 line 863
  385. def OAI.SnakyPrototype.Certificate21.height_342 line 871
  386. def OAI.SnakyPrototype.Certificate21.childrenH_342 line 872
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_342 line 873
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_342 line 874
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_342 line 876
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_342 line 880
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_342 line 882
  392. def OAI.SnakyPrototype.Certificate21.checked_342 line 886
  393. def OAI.SnakyPrototype.Certificate21.height_347_i1 line 894
  394. def OAI.SnakyPrototype.Certificate21.childrenH_347_i1 line 895
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_347_i1 line 896
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_347_i1 line 897
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_347_i1 line 899
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_347_i1 line 903
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_347_i1 line 905
  400. def OAI.SnakyPrototype.Certificate21.checked_347_i1 line 909
  401. def OAI.SnakyPrototype.Certificate21.height_347_i0 line 917
  402. def OAI.SnakyPrototype.Certificate21.childrenH_347_i0 line 918
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_347_i0 line 919
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_347_i0 line 920
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_347_i0 line 922
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_347_i0 line 926
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_347_i0 line 928
  408. def OAI.SnakyPrototype.Certificate21.checked_347_i0 line 932
  409. def OAI.SnakyPrototype.Certificate21.height_347 line 940
  410. def OAI.SnakyPrototype.Certificate21.childrenH_347 line 941
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_347 line 942
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_347 line 943
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_347 line 945
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_347 line 949
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_347 line 951
  416. def OAI.SnakyPrototype.Certificate21.checked_347 line 955
  417. def OAI.SnakyPrototype.Certificate21.height_352 line 963
  418. def OAI.SnakyPrototype.Certificate21.childrenH_352 line 964
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_352 line 965
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_352 line 966
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_352 line 968
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_352 line 972
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_352 line 974
  424. def OAI.SnakyPrototype.Certificate21.checked_352 line 978
  425. def OAI.SnakyPrototype.Certificate21.height_355 line 986
  426. def OAI.SnakyPrototype.Certificate21.childrenH_355 line 987
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_355 line 988
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_355 line 989
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_355 line 991
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_355 line 995
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_355 line 997
  432. def OAI.SnakyPrototype.Certificate21.checked_355 line 1001