OAI/GameTheory/SnakyTwentyOne/Cards/Height08Part02.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_452_i0 line 23
  2. def OAI.SnakyPrototype.Certificate21.envelope_452_i0 line 24
  3. def OAI.SnakyPrototype.Certificate21.childrenC_452_i0 line 25
  4. def OAI.SnakyPrototype.Certificate21.childrenD_452_i0 line 26
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_452_i0 line 27
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_452_i0 line 28
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_452_i0 line 29
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_452_i0 line 30
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_452_i0 line 31
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_452_i0 line 36
  11. def OAI.SnakyPrototype.Certificate21.required_452 line 41
  12. def OAI.SnakyPrototype.Certificate21.envelope_452 line 42
  13. def OAI.SnakyPrototype.Certificate21.childrenC_452 line 43
  14. def OAI.SnakyPrototype.Certificate21.childrenD_452 line 44
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_452 line 45
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_452 line 46
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_452 line 47
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_452 line 48
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_452 line 49
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_452 line 55
  21. def OAI.SnakyPrototype.Certificate21.required_454 line 60
  22. def OAI.SnakyPrototype.Certificate21.envelope_454 line 61
  23. def OAI.SnakyPrototype.Certificate21.childrenC_454 line 62
  24. def OAI.SnakyPrototype.Certificate21.childrenD_454 line 63
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_454 line 64
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_454 line 65
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_454 line 66
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_454 line 67
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_454 line 68
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_454 line 73
  31. def OAI.SnakyPrototype.Certificate21.required_455 line 78
  32. def OAI.SnakyPrototype.Certificate21.envelope_455 line 79
  33. def OAI.SnakyPrototype.Certificate21.childrenC_455 line 80
  34. def OAI.SnakyPrototype.Certificate21.childrenD_455 line 81
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_455 line 82
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_455 line 83
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_455 line 84
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_455 line 85
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_455 line 86
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_455 line 93
  41. def OAI.SnakyPrototype.Certificate21.required_456 line 98
  42. def OAI.SnakyPrototype.Certificate21.envelope_456 line 99
  43. def OAI.SnakyPrototype.Certificate21.childrenC_456 line 100
  44. def OAI.SnakyPrototype.Certificate21.childrenD_456 line 101
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_456 line 102
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_456 line 103
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_456 line 104
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_456 line 105
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_456 line 106
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_456 line 111
  51. def OAI.SnakyPrototype.Certificate21.required_473 line 116
  52. def OAI.SnakyPrototype.Certificate21.envelope_473 line 117
  53. def OAI.SnakyPrototype.Certificate21.childrenC_473 line 118
  54. def OAI.SnakyPrototype.Certificate21.childrenD_473 line 119
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_473 line 120
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_473 line 121
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_473 line 122
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_473 line 123
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_473 line 124
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_473 line 129
  61. def OAI.SnakyPrototype.Certificate21.required_478 line 134
  62. def OAI.SnakyPrototype.Certificate21.envelope_478 line 135
  63. def OAI.SnakyPrototype.Certificate21.childrenC_478 line 136
  64. def OAI.SnakyPrototype.Certificate21.childrenD_478 line 137
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_478 line 138
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_478 line 139
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_478 line 140
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_478 line 141
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_478 line 142
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_478 line 147
  71. def OAI.SnakyPrototype.Certificate21.required_482 line 152
  72. def OAI.SnakyPrototype.Certificate21.envelope_482 line 153
  73. def OAI.SnakyPrototype.Certificate21.childrenC_482 line 154
  74. def OAI.SnakyPrototype.Certificate21.childrenD_482 line 155
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_482 line 156
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_482 line 157
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_482 line 158
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_482 line 159
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_482 line 160
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_482 line 167
  81. def OAI.SnakyPrototype.Certificate21.required_484_i1 line 172
  82. def OAI.SnakyPrototype.Certificate21.envelope_484_i1 line 173
  83. def OAI.SnakyPrototype.Certificate21.childrenC_484_i1 line 174
  84. def OAI.SnakyPrototype.Certificate21.childrenD_484_i1 line 175
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i1 line 176
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i1 line 177
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i1 line 178
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i1 line 179
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i1 line 180
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i1 line 185
  91. def OAI.SnakyPrototype.Certificate21.required_484_i2 line 190
  92. def OAI.SnakyPrototype.Certificate21.envelope_484_i2 line 191
  93. def OAI.SnakyPrototype.Certificate21.childrenC_484_i2 line 192
  94. def OAI.SnakyPrototype.Certificate21.childrenD_484_i2 line 193
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i2 line 194
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i2 line 195
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i2 line 196
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i2 line 197
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i2 line 198
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i2 line 204
  101. def OAI.SnakyPrototype.Certificate21.required_484_i4 line 209
  102. def OAI.SnakyPrototype.Certificate21.envelope_484_i4 line 210
  103. def OAI.SnakyPrototype.Certificate21.childrenC_484_i4 line 211
  104. def OAI.SnakyPrototype.Certificate21.childrenD_484_i4 line 212
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i4 line 213
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i4 line 214
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i4 line 215
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i4 line 216
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i4 line 217
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i4 line 222
  111. def OAI.SnakyPrototype.Certificate21.required_484_i3 line 227
  112. def OAI.SnakyPrototype.Certificate21.envelope_484_i3 line 228
  113. def OAI.SnakyPrototype.Certificate21.childrenC_484_i3 line 229
  114. def OAI.SnakyPrototype.Certificate21.childrenD_484_i3 line 230
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i3 line 231
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i3 line 232
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i3 line 233
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i3 line 234
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i3 line 235
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i3 line 241
  121. def OAI.SnakyPrototype.Certificate21.required_484_i0 line 246
  122. def OAI.SnakyPrototype.Certificate21.envelope_484_i0 line 247
  123. def OAI.SnakyPrototype.Certificate21.childrenC_484_i0 line 248
  124. def OAI.SnakyPrototype.Certificate21.childrenD_484_i0 line 249
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i0 line 250
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i0 line 251
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i0 line 252
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i0 line 253
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i0 line 254
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i0 line 260
  131. def OAI.SnakyPrototype.Certificate21.required_484_i6 line 265
  132. def OAI.SnakyPrototype.Certificate21.envelope_484_i6 line 266
  133. def OAI.SnakyPrototype.Certificate21.childrenC_484_i6 line 267
  134. def OAI.SnakyPrototype.Certificate21.childrenD_484_i6 line 268
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i6 line 269
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i6 line 270
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i6 line 271
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i6 line 272
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i6 line 273
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i6 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_484_i5 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_484_i5 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_484_i5 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_484_i5 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_484_i5 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484_i5 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484_i5 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484_i5 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_484_i5 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_484_i5 line 297
  151. def OAI.SnakyPrototype.Certificate21.required_484 line 302
  152. def OAI.SnakyPrototype.Certificate21.envelope_484 line 303
  153. def OAI.SnakyPrototype.Certificate21.childrenC_484 line 304
  154. def OAI.SnakyPrototype.Certificate21.childrenD_484 line 305
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_484 line 306
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_484 line 307
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_484 line 308
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_484 line 309
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_484 line 310
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_484 line 317
  161. def OAI.SnakyPrototype.Certificate21.required_494 line 322
  162. def OAI.SnakyPrototype.Certificate21.envelope_494 line 323
  163. def OAI.SnakyPrototype.Certificate21.childrenC_494 line 324
  164. def OAI.SnakyPrototype.Certificate21.childrenD_494 line 325
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_494 line 326
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_494 line 327
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_494 line 328
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_494 line 329
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_494 line 330
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_494 line 337
  171. def OAI.SnakyPrototype.Certificate21.required_510_i0 line 342
  172. def OAI.SnakyPrototype.Certificate21.envelope_510_i0 line 343
  173. def OAI.SnakyPrototype.Certificate21.childrenC_510_i0 line 344
  174. def OAI.SnakyPrototype.Certificate21.childrenD_510_i0 line 345
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_510_i0 line 346
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_510_i0 line 347
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_510_i0 line 348
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_510_i0 line 349
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_510_i0 line 350
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_510_i0 line 355
  181. def OAI.SnakyPrototype.Certificate21.required_510 line 360
  182. def OAI.SnakyPrototype.Certificate21.envelope_510 line 361
  183. def OAI.SnakyPrototype.Certificate21.childrenC_510 line 362
  184. def OAI.SnakyPrototype.Certificate21.childrenD_510 line 363
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_510 line 364
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_510 line 365
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_510 line 366
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_510 line 367
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_510 line 368
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_510 line 374
  191. def OAI.SnakyPrototype.Certificate21.required_513_i0 line 379
  192. def OAI.SnakyPrototype.Certificate21.envelope_513_i0 line 380
  193. def OAI.SnakyPrototype.Certificate21.childrenC_513_i0 line 381
  194. def OAI.SnakyPrototype.Certificate21.childrenD_513_i0 line 382
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_513_i0 line 383
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_513_i0 line 384
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_513_i0 line 385
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_513_i0 line 386
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_513_i0 line 387
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_513_i0 line 392
  201. def OAI.SnakyPrototype.Certificate21.required_513 line 397
  202. def OAI.SnakyPrototype.Certificate21.envelope_513 line 398
  203. def OAI.SnakyPrototype.Certificate21.childrenC_513 line 399
  204. def OAI.SnakyPrototype.Certificate21.childrenD_513 line 400
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_513 line 401
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_513 line 402
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_513 line 403
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_513 line 404
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_513 line 405
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_513 line 411
  211. def OAI.SnakyPrototype.Certificate21.height_452_i0 line 416
  212. def OAI.SnakyPrototype.Certificate21.childrenH_452_i0 line 417
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_452_i0 line 418
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_452_i0 line 419
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_452_i0 line 421
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_452_i0 line 425
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_452_i0 line 427
  218. def OAI.SnakyPrototype.Certificate21.checked_452_i0 line 431
  219. def OAI.SnakyPrototype.Certificate21.height_452 line 439
  220. def OAI.SnakyPrototype.Certificate21.childrenH_452 line 440
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_452 line 441
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_452 line 442
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_452 line 444
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_452 line 448
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_452 line 450
  226. def OAI.SnakyPrototype.Certificate21.checked_452 line 454
  227. def OAI.SnakyPrototype.Certificate21.height_454 line 462
  228. def OAI.SnakyPrototype.Certificate21.childrenH_454 line 463
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_454 line 464
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_454 line 465
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_454 line 467
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_454 line 471
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_454 line 473
  234. def OAI.SnakyPrototype.Certificate21.checked_454 line 477
  235. def OAI.SnakyPrototype.Certificate21.height_455 line 485
  236. def OAI.SnakyPrototype.Certificate21.childrenH_455 line 486
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_455 line 487
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_455 line 488
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_455 line 490
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_455 line 494
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_455 line 496
  242. def OAI.SnakyPrototype.Certificate21.checked_455 line 500
  243. def OAI.SnakyPrototype.Certificate21.height_456 line 508
  244. def OAI.SnakyPrototype.Certificate21.childrenH_456 line 509
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_456 line 510
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_456 line 511
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_456 line 513
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_456 line 517
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_456 line 519
  250. def OAI.SnakyPrototype.Certificate21.checked_456 line 523
  251. def OAI.SnakyPrototype.Certificate21.height_473 line 531
  252. def OAI.SnakyPrototype.Certificate21.childrenH_473 line 532
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_473 line 533
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_473 line 534
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_473 line 536
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_473 line 540
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_473 line 542
  258. def OAI.SnakyPrototype.Certificate21.checked_473 line 546
  259. def OAI.SnakyPrototype.Certificate21.height_478 line 554
  260. def OAI.SnakyPrototype.Certificate21.childrenH_478 line 555
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_478 line 556
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_478 line 557
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_478 line 559
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_478 line 563
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_478 line 565
  266. def OAI.SnakyPrototype.Certificate21.checked_478 line 569
  267. def OAI.SnakyPrototype.Certificate21.height_482 line 577
  268. def OAI.SnakyPrototype.Certificate21.childrenH_482 line 578
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_482 line 579
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_482 line 580
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_482 line 582
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_482 line 586
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_482 line 588
  274. def OAI.SnakyPrototype.Certificate21.checked_482 line 592
  275. def OAI.SnakyPrototype.Certificate21.height_484_i1 line 600
  276. def OAI.SnakyPrototype.Certificate21.childrenH_484_i1 line 601
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i1 line 602
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i1 line 603
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i1 line 605
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i1 line 609
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i1 line 611
  282. def OAI.SnakyPrototype.Certificate21.checked_484_i1 line 615
  283. def OAI.SnakyPrototype.Certificate21.height_484_i2 line 623
  284. def OAI.SnakyPrototype.Certificate21.childrenH_484_i2 line 624
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i2 line 625
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i2 line 626
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i2 line 628
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i2 line 632
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i2 line 634
  290. def OAI.SnakyPrototype.Certificate21.checked_484_i2 line 638
  291. def OAI.SnakyPrototype.Certificate21.height_484_i4 line 646
  292. def OAI.SnakyPrototype.Certificate21.childrenH_484_i4 line 647
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i4 line 648
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i4 line 649
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i4 line 651
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i4 line 655
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i4 line 657
  298. def OAI.SnakyPrototype.Certificate21.checked_484_i4 line 661
  299. def OAI.SnakyPrototype.Certificate21.height_484_i3 line 669
  300. def OAI.SnakyPrototype.Certificate21.childrenH_484_i3 line 670
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i3 line 671
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i3 line 672
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i3 line 674
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i3 line 678
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i3 line 680
  306. def OAI.SnakyPrototype.Certificate21.checked_484_i3 line 684
  307. def OAI.SnakyPrototype.Certificate21.height_484_i0 line 692
  308. def OAI.SnakyPrototype.Certificate21.childrenH_484_i0 line 693
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i0 line 694
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i0 line 695
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i0 line 697
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i0 line 701
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i0 line 703
  314. def OAI.SnakyPrototype.Certificate21.checked_484_i0 line 707
  315. def OAI.SnakyPrototype.Certificate21.height_484_i6 line 715
  316. def OAI.SnakyPrototype.Certificate21.childrenH_484_i6 line 716
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i6 line 717
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i6 line 718
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i6 line 720
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i6 line 724
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i6 line 726
  322. def OAI.SnakyPrototype.Certificate21.checked_484_i6 line 730
  323. def OAI.SnakyPrototype.Certificate21.height_484_i5 line 738
  324. def OAI.SnakyPrototype.Certificate21.childrenH_484_i5 line 739
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_484_i5 line 740
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_484_i5 line 741
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_484_i5 line 743
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484_i5 line 747
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484_i5 line 749
  330. def OAI.SnakyPrototype.Certificate21.checked_484_i5 line 753
  331. def OAI.SnakyPrototype.Certificate21.height_484 line 761
  332. def OAI.SnakyPrototype.Certificate21.childrenH_484 line 762
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_484 line 763
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_484 line 764
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_484 line 766
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_484 line 770
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_484 line 772
  338. def OAI.SnakyPrototype.Certificate21.checked_484 line 776
  339. def OAI.SnakyPrototype.Certificate21.height_494 line 784
  340. def OAI.SnakyPrototype.Certificate21.childrenH_494 line 785
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_494 line 786
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_494 line 787
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_494 line 789
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_494 line 793
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_494 line 795
  346. def OAI.SnakyPrototype.Certificate21.checked_494 line 799
  347. def OAI.SnakyPrototype.Certificate21.height_510_i0 line 807
  348. def OAI.SnakyPrototype.Certificate21.childrenH_510_i0 line 808
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_510_i0 line 809
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_510_i0 line 810
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_510_i0 line 812
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_510_i0 line 816
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_510_i0 line 818
  354. def OAI.SnakyPrototype.Certificate21.checked_510_i0 line 822
  355. def OAI.SnakyPrototype.Certificate21.height_510 line 830
  356. def OAI.SnakyPrototype.Certificate21.childrenH_510 line 831
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_510 line 832
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_510 line 833
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_510 line 835
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_510 line 839
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_510 line 841
  362. def OAI.SnakyPrototype.Certificate21.checked_510 line 845
  363. def OAI.SnakyPrototype.Certificate21.height_513_i0 line 853
  364. def OAI.SnakyPrototype.Certificate21.childrenH_513_i0 line 854
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_513_i0 line 855
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_513_i0 line 856
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_513_i0 line 858
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_513_i0 line 862
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_513_i0 line 864
  370. def OAI.SnakyPrototype.Certificate21.checked_513_i0 line 868
  371. def OAI.SnakyPrototype.Certificate21.height_513 line 876
  372. def OAI.SnakyPrototype.Certificate21.childrenH_513 line 877
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_513 line 878
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_513 line 879
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_513 line 881
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_513 line 885
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_513 line 887
  378. def OAI.SnakyPrototype.Certificate21.checked_513 line 891