OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part03.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_591_i0 line 38
  2. def OAI.SnakyPrototype.Certificate21.envelope_591_i0 line 39
  3. def OAI.SnakyPrototype.Certificate21.childrenC_591_i0 line 40
  4. def OAI.SnakyPrototype.Certificate21.childrenD_591_i0 line 41
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_591_i0 line 42
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591_i0 line 43
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591_i0 line 44
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591_i0 line 45
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_591_i0 line 46
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_591_i0 line 51
  11. def OAI.SnakyPrototype.Certificate21.required_591_i1 line 56
  12. def OAI.SnakyPrototype.Certificate21.envelope_591_i1 line 57
  13. def OAI.SnakyPrototype.Certificate21.childrenC_591_i1 line 58
  14. def OAI.SnakyPrototype.Certificate21.childrenD_591_i1 line 59
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_591_i1 line 60
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591_i1 line 61
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591_i1 line 62
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591_i1 line 63
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_591_i1 line 64
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_591_i1 line 72
  21. def OAI.SnakyPrototype.Certificate21.required_591_i4 line 77
  22. def OAI.SnakyPrototype.Certificate21.envelope_591_i4 line 78
  23. def OAI.SnakyPrototype.Certificate21.childrenC_591_i4 line 79
  24. def OAI.SnakyPrototype.Certificate21.childrenD_591_i4 line 80
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_591_i4 line 81
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591_i4 line 82
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591_i4 line 83
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591_i4 line 84
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_591_i4 line 85
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_591_i4 line 90
  31. def OAI.SnakyPrototype.Certificate21.required_591_i3 line 95
  32. def OAI.SnakyPrototype.Certificate21.envelope_591_i3 line 96
  33. def OAI.SnakyPrototype.Certificate21.childrenC_591_i3 line 97
  34. def OAI.SnakyPrototype.Certificate21.childrenD_591_i3 line 98
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_591_i3 line 99
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591_i3 line 100
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591_i3 line 101
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591_i3 line 102
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_591_i3 line 103
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_591_i3 line 109
  41. def OAI.SnakyPrototype.Certificate21.required_591_i5 line 114
  42. def OAI.SnakyPrototype.Certificate21.envelope_591_i5 line 115
  43. def OAI.SnakyPrototype.Certificate21.childrenC_591_i5 line 116
  44. def OAI.SnakyPrototype.Certificate21.childrenD_591_i5 line 117
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_591_i5 line 118
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591_i5 line 119
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591_i5 line 120
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591_i5 line 121
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_591_i5 line 122
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_591_i5 line 128
  51. def OAI.SnakyPrototype.Certificate21.required_591_i2 line 133
  52. def OAI.SnakyPrototype.Certificate21.envelope_591_i2 line 134
  53. def OAI.SnakyPrototype.Certificate21.childrenC_591_i2 line 135
  54. def OAI.SnakyPrototype.Certificate21.childrenD_591_i2 line 136
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_591_i2 line 137
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591_i2 line 138
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591_i2 line 139
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591_i2 line 140
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_591_i2 line 141
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_591_i2 line 149
  61. def OAI.SnakyPrototype.Certificate21.required_591 line 154
  62. def OAI.SnakyPrototype.Certificate21.envelope_591 line 155
  63. def OAI.SnakyPrototype.Certificate21.childrenC_591 line 156
  64. def OAI.SnakyPrototype.Certificate21.childrenD_591 line 157
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_591 line 158
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_591 line 159
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_591 line 160
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_591 line 161
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_591 line 162
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_591 line 170
  71. def OAI.SnakyPrototype.Certificate21.required_597_i0 line 175
  72. def OAI.SnakyPrototype.Certificate21.envelope_597_i0 line 176
  73. def OAI.SnakyPrototype.Certificate21.childrenC_597_i0 line 177
  74. def OAI.SnakyPrototype.Certificate21.childrenD_597_i0 line 178
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i0 line 179
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i0 line 180
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i0 line 181
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i0 line 182
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i0 line 183
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i0 line 189
  81. def OAI.SnakyPrototype.Certificate21.required_597_i3 line 194
  82. def OAI.SnakyPrototype.Certificate21.envelope_597_i3 line 195
  83. def OAI.SnakyPrototype.Certificate21.childrenC_597_i3 line 196
  84. def OAI.SnakyPrototype.Certificate21.childrenD_597_i3 line 197
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i3 line 198
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i3 line 199
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i3 line 200
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i3 line 201
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i3 line 202
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i3 line 207
  91. def OAI.SnakyPrototype.Certificate21.required_597_i2 line 212
  92. def OAI.SnakyPrototype.Certificate21.envelope_597_i2 line 213
  93. def OAI.SnakyPrototype.Certificate21.childrenC_597_i2 line 214
  94. def OAI.SnakyPrototype.Certificate21.childrenD_597_i2 line 215
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i2 line 216
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i2 line 217
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i2 line 218
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i2 line 219
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i2 line 220
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i2 line 225
  101. def OAI.SnakyPrototype.Certificate21.required_597_i6 line 230
  102. def OAI.SnakyPrototype.Certificate21.envelope_597_i6 line 231
  103. def OAI.SnakyPrototype.Certificate21.childrenC_597_i6 line 232
  104. def OAI.SnakyPrototype.Certificate21.childrenD_597_i6 line 233
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i6 line 234
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i6 line 235
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i6 line 236
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i6 line 237
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i6 line 238
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i6 line 243
  111. def OAI.SnakyPrototype.Certificate21.required_597_i5 line 248
  112. def OAI.SnakyPrototype.Certificate21.envelope_597_i5 line 249
  113. def OAI.SnakyPrototype.Certificate21.childrenC_597_i5 line 250
  114. def OAI.SnakyPrototype.Certificate21.childrenD_597_i5 line 251
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i5 line 252
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i5 line 253
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i5 line 254
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i5 line 255
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i5 line 256
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i5 line 261
  121. def OAI.SnakyPrototype.Certificate21.required_597_i4 line 266
  122. def OAI.SnakyPrototype.Certificate21.envelope_597_i4 line 267
  123. def OAI.SnakyPrototype.Certificate21.childrenC_597_i4 line 268
  124. def OAI.SnakyPrototype.Certificate21.childrenD_597_i4 line 269
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i4 line 270
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i4 line 271
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i4 line 272
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i4 line 273
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i4 line 274
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i4 line 279
  131. def OAI.SnakyPrototype.Certificate21.required_597_i1 line 284
  132. def OAI.SnakyPrototype.Certificate21.envelope_597_i1 line 285
  133. def OAI.SnakyPrototype.Certificate21.childrenC_597_i1 line 286
  134. def OAI.SnakyPrototype.Certificate21.childrenD_597_i1 line 287
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_597_i1 line 288
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597_i1 line 289
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597_i1 line 290
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597_i1 line 291
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_597_i1 line 292
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_597_i1 line 298
  141. def OAI.SnakyPrototype.Certificate21.required_597 line 303
  142. def OAI.SnakyPrototype.Certificate21.envelope_597 line 304
  143. def OAI.SnakyPrototype.Certificate21.childrenC_597 line 305
  144. def OAI.SnakyPrototype.Certificate21.childrenD_597 line 306
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_597 line 307
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_597 line 308
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_597 line 309
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_597 line 310
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_597 line 311
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_597 line 319
  151. def OAI.SnakyPrototype.Certificate21.required_603_i0 line 324
  152. def OAI.SnakyPrototype.Certificate21.envelope_603_i0 line 325
  153. def OAI.SnakyPrototype.Certificate21.childrenC_603_i0 line 326
  154. def OAI.SnakyPrototype.Certificate21.childrenD_603_i0 line 327
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_603_i0 line 328
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_603_i0 line 329
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_603_i0 line 330
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_603_i0 line 331
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_603_i0 line 332
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_603_i0 line 339
  161. def OAI.SnakyPrototype.Certificate21.required_603 line 344
  162. def OAI.SnakyPrototype.Certificate21.envelope_603 line 345
  163. def OAI.SnakyPrototype.Certificate21.childrenC_603 line 346
  164. def OAI.SnakyPrototype.Certificate21.childrenD_603 line 347
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_603 line 348
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_603 line 349
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_603 line 350
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_603 line 351
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_603 line 352
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_603 line 362
  171. def OAI.SnakyPrototype.Certificate21.required_634 line 367
  172. def OAI.SnakyPrototype.Certificate21.envelope_634 line 368
  173. def OAI.SnakyPrototype.Certificate21.childrenC_634 line 369
  174. def OAI.SnakyPrototype.Certificate21.childrenD_634 line 370
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_634 line 371
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_634 line 372
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_634 line 373
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_634 line 374
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_634 line 375
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_634 line 383
  181. def OAI.SnakyPrototype.Certificate21.required_642 line 388
  182. def OAI.SnakyPrototype.Certificate21.envelope_642 line 389
  183. def OAI.SnakyPrototype.Certificate21.childrenC_642 line 390
  184. def OAI.SnakyPrototype.Certificate21.childrenD_642 line 391
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_642 line 392
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_642 line 393
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_642 line 394
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_642 line 395
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_642 line 396
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_642 line 406
  191. def OAI.SnakyPrototype.Certificate21.required_643 line 411
  192. def OAI.SnakyPrototype.Certificate21.envelope_643 line 412
  193. def OAI.SnakyPrototype.Certificate21.childrenC_643 line 413
  194. def OAI.SnakyPrototype.Certificate21.childrenD_643 line 414
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_643 line 415
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_643 line 416
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_643 line 417
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_643 line 418
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_643 line 419
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_643 line 429
  201. def OAI.SnakyPrototype.Certificate21.required_647_i1 line 434
  202. def OAI.SnakyPrototype.Certificate21.envelope_647_i1 line 435
  203. def OAI.SnakyPrototype.Certificate21.childrenC_647_i1 line 436
  204. def OAI.SnakyPrototype.Certificate21.childrenD_647_i1 line 437
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_647_i1 line 438
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_647_i1 line 439
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_647_i1 line 440
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_647_i1 line 441
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_647_i1 line 442
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_647_i1 line 448
  211. def OAI.SnakyPrototype.Certificate21.required_647_i0 line 453
  212. def OAI.SnakyPrototype.Certificate21.envelope_647_i0 line 454
  213. def OAI.SnakyPrototype.Certificate21.childrenC_647_i0 line 455
  214. def OAI.SnakyPrototype.Certificate21.childrenD_647_i0 line 456
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_647_i0 line 457
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_647_i0 line 458
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_647_i0 line 459
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_647_i0 line 460
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_647_i0 line 461
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_647_i0 line 468
  221. def OAI.SnakyPrototype.Certificate21.required_647 line 473
  222. def OAI.SnakyPrototype.Certificate21.envelope_647 line 474
  223. def OAI.SnakyPrototype.Certificate21.childrenC_647 line 475
  224. def OAI.SnakyPrototype.Certificate21.childrenD_647 line 476
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_647 line 477
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_647 line 478
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_647 line 479
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_647 line 480
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_647 line 481
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_647 line 493
  231. def OAI.SnakyPrototype.Certificate21.height_591_i0 line 498
  232. def OAI.SnakyPrototype.Certificate21.childrenH_591_i0 line 499
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_591_i0 line 500
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_591_i0 line 501
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_591_i0 line 503
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591_i0 line 507
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591_i0 line 509
  238. def OAI.SnakyPrototype.Certificate21.checked_591_i0 line 513
  239. def OAI.SnakyPrototype.Certificate21.height_591_i1 line 521
  240. def OAI.SnakyPrototype.Certificate21.childrenH_591_i1 line 522
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_591_i1 line 523
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_591_i1 line 524
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_591_i1 line 526
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591_i1 line 530
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591_i1 line 532
  246. def OAI.SnakyPrototype.Certificate21.checked_591_i1 line 536
  247. def OAI.SnakyPrototype.Certificate21.height_591_i4 line 544
  248. def OAI.SnakyPrototype.Certificate21.childrenH_591_i4 line 545
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_591_i4 line 546
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_591_i4 line 547
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_591_i4 line 549
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591_i4 line 553
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591_i4 line 555
  254. def OAI.SnakyPrototype.Certificate21.checked_591_i4 line 559
  255. def OAI.SnakyPrototype.Certificate21.height_591_i3 line 567
  256. def OAI.SnakyPrototype.Certificate21.childrenH_591_i3 line 568
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_591_i3 line 569
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_591_i3 line 570
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_591_i3 line 572
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591_i3 line 576
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591_i3 line 578
  262. def OAI.SnakyPrototype.Certificate21.checked_591_i3 line 582
  263. def OAI.SnakyPrototype.Certificate21.height_591_i5 line 590
  264. def OAI.SnakyPrototype.Certificate21.childrenH_591_i5 line 591
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_591_i5 line 592
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_591_i5 line 593
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_591_i5 line 595
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591_i5 line 599
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591_i5 line 601
  270. def OAI.SnakyPrototype.Certificate21.checked_591_i5 line 605
  271. def OAI.SnakyPrototype.Certificate21.height_591_i2 line 613
  272. def OAI.SnakyPrototype.Certificate21.childrenH_591_i2 line 614
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_591_i2 line 615
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_591_i2 line 616
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_591_i2 line 618
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591_i2 line 622
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591_i2 line 624
  278. def OAI.SnakyPrototype.Certificate21.checked_591_i2 line 628
  279. def OAI.SnakyPrototype.Certificate21.height_591 line 636
  280. def OAI.SnakyPrototype.Certificate21.childrenH_591 line 637
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_591 line 638
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_591 line 639
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_591 line 641
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_591 line 645
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_591 line 647
  286. def OAI.SnakyPrototype.Certificate21.checked_591 line 651
  287. def OAI.SnakyPrototype.Certificate21.height_597_i0 line 659
  288. def OAI.SnakyPrototype.Certificate21.childrenH_597_i0 line 660
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i0 line 661
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i0 line 662
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i0 line 664
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i0 line 668
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i0 line 670
  294. def OAI.SnakyPrototype.Certificate21.checked_597_i0 line 674
  295. def OAI.SnakyPrototype.Certificate21.height_597_i3 line 682
  296. def OAI.SnakyPrototype.Certificate21.childrenH_597_i3 line 683
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i3 line 684
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i3 line 685
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i3 line 687
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i3 line 691
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i3 line 693
  302. def OAI.SnakyPrototype.Certificate21.checked_597_i3 line 697
  303. def OAI.SnakyPrototype.Certificate21.height_597_i2 line 705
  304. def OAI.SnakyPrototype.Certificate21.childrenH_597_i2 line 706
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i2 line 707
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i2 line 708
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i2 line 710
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i2 line 714
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i2 line 716
  310. def OAI.SnakyPrototype.Certificate21.checked_597_i2 line 720
  311. def OAI.SnakyPrototype.Certificate21.height_597_i6 line 728
  312. def OAI.SnakyPrototype.Certificate21.childrenH_597_i6 line 729
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i6 line 730
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i6 line 731
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i6 line 733
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i6 line 737
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i6 line 739
  318. def OAI.SnakyPrototype.Certificate21.checked_597_i6 line 743
  319. def OAI.SnakyPrototype.Certificate21.height_597_i5 line 751
  320. def OAI.SnakyPrototype.Certificate21.childrenH_597_i5 line 752
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i5 line 753
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i5 line 754
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i5 line 756
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i5 line 760
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i5 line 762
  326. def OAI.SnakyPrototype.Certificate21.checked_597_i5 line 766
  327. def OAI.SnakyPrototype.Certificate21.height_597_i4 line 774
  328. def OAI.SnakyPrototype.Certificate21.childrenH_597_i4 line 775
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i4 line 776
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i4 line 777
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i4 line 779
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i4 line 783
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i4 line 785
  334. def OAI.SnakyPrototype.Certificate21.checked_597_i4 line 789
  335. def OAI.SnakyPrototype.Certificate21.height_597_i1 line 797
  336. def OAI.SnakyPrototype.Certificate21.childrenH_597_i1 line 798
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_597_i1 line 799
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_597_i1 line 800
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_597_i1 line 802
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597_i1 line 806
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597_i1 line 808
  342. def OAI.SnakyPrototype.Certificate21.checked_597_i1 line 812
  343. def OAI.SnakyPrototype.Certificate21.height_597 line 820
  344. def OAI.SnakyPrototype.Certificate21.childrenH_597 line 821
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_597 line 822
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_597 line 823
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_597 line 825
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_597 line 829
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_597 line 831
  350. def OAI.SnakyPrototype.Certificate21.checked_597 line 835
  351. def OAI.SnakyPrototype.Certificate21.height_603_i0 line 843
  352. def OAI.SnakyPrototype.Certificate21.childrenH_603_i0 line 844
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_603_i0 line 845
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_603_i0 line 846
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_603_i0 line 848
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_603_i0 line 852
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_603_i0 line 854
  358. def OAI.SnakyPrototype.Certificate21.checked_603_i0 line 858
  359. def OAI.SnakyPrototype.Certificate21.height_603 line 866
  360. def OAI.SnakyPrototype.Certificate21.childrenH_603 line 867
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_603 line 868
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_603 line 869
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_603 line 871
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_603 line 875
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_603 line 877
  366. def OAI.SnakyPrototype.Certificate21.checked_603 line 881
  367. def OAI.SnakyPrototype.Certificate21.height_634 line 889
  368. def OAI.SnakyPrototype.Certificate21.childrenH_634 line 890
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_634 line 891
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_634 line 892
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_634 line 894
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_634 line 898
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_634 line 900
  374. def OAI.SnakyPrototype.Certificate21.checked_634 line 904
  375. def OAI.SnakyPrototype.Certificate21.height_642 line 912
  376. def OAI.SnakyPrototype.Certificate21.childrenH_642 line 913
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_642 line 914
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_642 line 915
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_642 line 917
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_642 line 921
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_642 line 923
  382. def OAI.SnakyPrototype.Certificate21.checked_642 line 927
  383. def OAI.SnakyPrototype.Certificate21.height_643 line 935
  384. def OAI.SnakyPrototype.Certificate21.childrenH_643 line 936
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_643 line 937
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_643 line 938
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_643 line 940
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_643 line 944
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_643 line 946
  390. def OAI.SnakyPrototype.Certificate21.checked_643 line 950
  391. def OAI.SnakyPrototype.Certificate21.height_647_i1 line 958
  392. def OAI.SnakyPrototype.Certificate21.childrenH_647_i1 line 959
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_647_i1 line 960
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_647_i1 line 961
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_647_i1 line 963
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_647_i1 line 967
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_647_i1 line 969
  398. def OAI.SnakyPrototype.Certificate21.checked_647_i1 line 973
  399. def OAI.SnakyPrototype.Certificate21.height_647_i0 line 981
  400. def OAI.SnakyPrototype.Certificate21.childrenH_647_i0 line 982
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_647_i0 line 983
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_647_i0 line 984
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_647_i0 line 986
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_647_i0 line 990
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_647_i0 line 992
  406. def OAI.SnakyPrototype.Certificate21.checked_647_i0 line 996
  407. def OAI.SnakyPrototype.Certificate21.height_647 line 1004
  408. def OAI.SnakyPrototype.Certificate21.childrenH_647 line 1005
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_647 line 1006
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_647 line 1007
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_647 line 1009
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_647 line 1013
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_647 line 1015
  414. def OAI.SnakyPrototype.Certificate21.checked_647 line 1019