OAI/GameTheory/SnakyTwentyOne/Cards/Height09Part03.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_512_i0 line 23
  2. def OAI.SnakyPrototype.Certificate21.envelope_512_i0 line 24
  3. def OAI.SnakyPrototype.Certificate21.childrenC_512_i0 line 25
  4. def OAI.SnakyPrototype.Certificate21.childrenD_512_i0 line 26
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_512_i0 line 27
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_512_i0 line 28
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_512_i0 line 29
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_512_i0 line 30
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_512_i0 line 31
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_512_i0 line 36
  11. def OAI.SnakyPrototype.Certificate21.required_512_i3 line 41
  12. def OAI.SnakyPrototype.Certificate21.envelope_512_i3 line 42
  13. def OAI.SnakyPrototype.Certificate21.childrenC_512_i3 line 43
  14. def OAI.SnakyPrototype.Certificate21.childrenD_512_i3 line 44
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_512_i3 line 45
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_512_i3 line 46
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_512_i3 line 47
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_512_i3 line 48
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_512_i3 line 49
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_512_i3 line 54
  21. def OAI.SnakyPrototype.Certificate21.required_512_i4 line 59
  22. def OAI.SnakyPrototype.Certificate21.envelope_512_i4 line 60
  23. def OAI.SnakyPrototype.Certificate21.childrenC_512_i4 line 61
  24. def OAI.SnakyPrototype.Certificate21.childrenD_512_i4 line 62
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_512_i4 line 63
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_512_i4 line 64
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_512_i4 line 65
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_512_i4 line 66
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_512_i4 line 67
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_512_i4 line 72
  31. def OAI.SnakyPrototype.Certificate21.required_512_i2 line 77
  32. def OAI.SnakyPrototype.Certificate21.envelope_512_i2 line 78
  33. def OAI.SnakyPrototype.Certificate21.childrenC_512_i2 line 79
  34. def OAI.SnakyPrototype.Certificate21.childrenD_512_i2 line 80
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_512_i2 line 81
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_512_i2 line 82
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_512_i2 line 83
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_512_i2 line 84
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_512_i2 line 85
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_512_i2 line 90
  41. def OAI.SnakyPrototype.Certificate21.required_512_i1 line 95
  42. def OAI.SnakyPrototype.Certificate21.envelope_512_i1 line 96
  43. def OAI.SnakyPrototype.Certificate21.childrenC_512_i1 line 97
  44. def OAI.SnakyPrototype.Certificate21.childrenD_512_i1 line 98
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_512_i1 line 99
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_512_i1 line 100
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_512_i1 line 101
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_512_i1 line 102
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_512_i1 line 103
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_512_i1 line 110
  51. def OAI.SnakyPrototype.Certificate21.required_512 line 115
  52. def OAI.SnakyPrototype.Certificate21.envelope_512 line 116
  53. def OAI.SnakyPrototype.Certificate21.childrenC_512 line 117
  54. def OAI.SnakyPrototype.Certificate21.childrenD_512 line 118
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_512 line 119
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_512 line 120
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_512 line 121
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_512 line 122
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_512 line 123
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_512 line 130
  61. def OAI.SnakyPrototype.Certificate21.required_514 line 135
  62. def OAI.SnakyPrototype.Certificate21.envelope_514 line 136
  63. def OAI.SnakyPrototype.Certificate21.childrenC_514 line 137
  64. def OAI.SnakyPrototype.Certificate21.childrenD_514 line 138
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_514 line 139
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_514 line 140
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_514 line 141
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_514 line 142
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_514 line 143
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_514 line 149
  71. def OAI.SnakyPrototype.Certificate21.required_519 line 154
  72. def OAI.SnakyPrototype.Certificate21.envelope_519 line 155
  73. def OAI.SnakyPrototype.Certificate21.childrenC_519 line 156
  74. def OAI.SnakyPrototype.Certificate21.childrenD_519 line 157
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_519 line 158
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_519 line 159
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_519 line 160
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_519 line 161
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_519 line 162
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_519 line 169
  81. def OAI.SnakyPrototype.Certificate21.required_528_i0 line 174
  82. def OAI.SnakyPrototype.Certificate21.envelope_528_i0 line 175
  83. def OAI.SnakyPrototype.Certificate21.childrenC_528_i0 line 176
  84. def OAI.SnakyPrototype.Certificate21.childrenD_528_i0 line 177
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_528_i0 line 178
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_528_i0 line 179
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_528_i0 line 180
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_528_i0 line 181
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_528_i0 line 182
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_528_i0 line 187
  91. def OAI.SnakyPrototype.Certificate21.required_528_i1 line 192
  92. def OAI.SnakyPrototype.Certificate21.envelope_528_i1 line 193
  93. def OAI.SnakyPrototype.Certificate21.childrenC_528_i1 line 194
  94. def OAI.SnakyPrototype.Certificate21.childrenD_528_i1 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_528_i1 line 196
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_528_i1 line 197
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_528_i1 line 198
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_528_i1 line 199
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_528_i1 line 200
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_528_i1 line 205
  101. def OAI.SnakyPrototype.Certificate21.required_528 line 210
  102. def OAI.SnakyPrototype.Certificate21.envelope_528 line 211
  103. def OAI.SnakyPrototype.Certificate21.childrenC_528 line 212
  104. def OAI.SnakyPrototype.Certificate21.childrenD_528 line 213
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_528 line 214
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_528 line 215
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_528 line 216
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_528 line 217
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_528 line 218
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_528 line 224
  111. def OAI.SnakyPrototype.Certificate21.required_531 line 229
  112. def OAI.SnakyPrototype.Certificate21.envelope_531 line 230
  113. def OAI.SnakyPrototype.Certificate21.childrenC_531 line 231
  114. def OAI.SnakyPrototype.Certificate21.childrenD_531 line 232
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_531 line 233
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_531 line 234
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_531 line 235
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_531 line 236
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_531 line 237
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_531 line 242
  121. def OAI.SnakyPrototype.Certificate21.required_536 line 247
  122. def OAI.SnakyPrototype.Certificate21.envelope_536 line 248
  123. def OAI.SnakyPrototype.Certificate21.childrenC_536 line 249
  124. def OAI.SnakyPrototype.Certificate21.childrenD_536 line 250
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_536 line 251
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_536 line 252
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_536 line 253
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_536 line 254
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_536 line 255
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_536 line 262
  131. def OAI.SnakyPrototype.Certificate21.required_537_i0 line 267
  132. def OAI.SnakyPrototype.Certificate21.envelope_537_i0 line 268
  133. def OAI.SnakyPrototype.Certificate21.childrenC_537_i0 line 269
  134. def OAI.SnakyPrototype.Certificate21.childrenD_537_i0 line 270
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i0 line 271
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i0 line 272
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i0 line 273
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i0 line 274
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i0 line 275
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i0 line 280
  141. def OAI.SnakyPrototype.Certificate21.required_537_i2 line 285
  142. def OAI.SnakyPrototype.Certificate21.envelope_537_i2 line 286
  143. def OAI.SnakyPrototype.Certificate21.childrenC_537_i2 line 287
  144. def OAI.SnakyPrototype.Certificate21.childrenD_537_i2 line 288
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i2 line 289
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i2 line 290
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i2 line 291
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i2 line 292
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i2 line 293
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i2 line 298
  151. def OAI.SnakyPrototype.Certificate21.required_537_i6 line 303
  152. def OAI.SnakyPrototype.Certificate21.envelope_537_i6 line 304
  153. def OAI.SnakyPrototype.Certificate21.childrenC_537_i6 line 305
  154. def OAI.SnakyPrototype.Certificate21.childrenD_537_i6 line 306
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i6 line 307
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i6 line 308
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i6 line 309
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i6 line 310
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i6 line 311
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i6 line 316
  161. def OAI.SnakyPrototype.Certificate21.required_537_i5 line 321
  162. def OAI.SnakyPrototype.Certificate21.envelope_537_i5 line 322
  163. def OAI.SnakyPrototype.Certificate21.childrenC_537_i5 line 323
  164. def OAI.SnakyPrototype.Certificate21.childrenD_537_i5 line 324
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i5 line 325
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i5 line 326
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i5 line 327
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i5 line 328
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i5 line 329
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i5 line 334
  171. def OAI.SnakyPrototype.Certificate21.required_537_i4 line 339
  172. def OAI.SnakyPrototype.Certificate21.envelope_537_i4 line 340
  173. def OAI.SnakyPrototype.Certificate21.childrenC_537_i4 line 341
  174. def OAI.SnakyPrototype.Certificate21.childrenD_537_i4 line 342
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i4 line 343
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i4 line 344
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i4 line 345
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i4 line 346
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i4 line 347
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i4 line 353
  181. def OAI.SnakyPrototype.Certificate21.required_537_i3 line 358
  182. def OAI.SnakyPrototype.Certificate21.envelope_537_i3 line 359
  183. def OAI.SnakyPrototype.Certificate21.childrenC_537_i3 line 360
  184. def OAI.SnakyPrototype.Certificate21.childrenD_537_i3 line 361
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i3 line 362
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i3 line 363
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i3 line 364
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i3 line 365
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i3 line 366
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i3 line 372
  191. def OAI.SnakyPrototype.Certificate21.required_537_i1 line 377
  192. def OAI.SnakyPrototype.Certificate21.envelope_537_i1 line 378
  193. def OAI.SnakyPrototype.Certificate21.childrenC_537_i1 line 379
  194. def OAI.SnakyPrototype.Certificate21.childrenD_537_i1 line 380
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_537_i1 line 381
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537_i1 line 382
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537_i1 line 383
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537_i1 line 384
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_537_i1 line 385
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_537_i1 line 392
  201. def OAI.SnakyPrototype.Certificate21.required_537 line 397
  202. def OAI.SnakyPrototype.Certificate21.envelope_537 line 398
  203. def OAI.SnakyPrototype.Certificate21.childrenC_537 line 399
  204. def OAI.SnakyPrototype.Certificate21.childrenD_537 line 400
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_537 line 401
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_537 line 402
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_537 line 403
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_537 line 404
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_537 line 405
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_537 line 412
  211. def OAI.SnakyPrototype.Certificate21.height_512_i0 line 417
  212. def OAI.SnakyPrototype.Certificate21.childrenH_512_i0 line 418
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_512_i0 line 419
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_512_i0 line 420
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_512_i0 line 422
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_512_i0 line 426
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_512_i0 line 428
  218. def OAI.SnakyPrototype.Certificate21.checked_512_i0 line 432
  219. def OAI.SnakyPrototype.Certificate21.height_512_i3 line 440
  220. def OAI.SnakyPrototype.Certificate21.childrenH_512_i3 line 441
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_512_i3 line 442
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_512_i3 line 443
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_512_i3 line 445
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_512_i3 line 449
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_512_i3 line 451
  226. def OAI.SnakyPrototype.Certificate21.checked_512_i3 line 455
  227. def OAI.SnakyPrototype.Certificate21.height_512_i4 line 463
  228. def OAI.SnakyPrototype.Certificate21.childrenH_512_i4 line 464
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_512_i4 line 465
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_512_i4 line 466
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_512_i4 line 468
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_512_i4 line 472
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_512_i4 line 474
  234. def OAI.SnakyPrototype.Certificate21.checked_512_i4 line 478
  235. def OAI.SnakyPrototype.Certificate21.height_512_i2 line 486
  236. def OAI.SnakyPrototype.Certificate21.childrenH_512_i2 line 487
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_512_i2 line 488
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_512_i2 line 489
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_512_i2 line 491
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_512_i2 line 495
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_512_i2 line 497
  242. def OAI.SnakyPrototype.Certificate21.checked_512_i2 line 501
  243. def OAI.SnakyPrototype.Certificate21.height_512_i1 line 509
  244. def OAI.SnakyPrototype.Certificate21.childrenH_512_i1 line 510
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_512_i1 line 511
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_512_i1 line 512
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_512_i1 line 514
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_512_i1 line 518
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_512_i1 line 520
  250. def OAI.SnakyPrototype.Certificate21.checked_512_i1 line 524
  251. def OAI.SnakyPrototype.Certificate21.height_512 line 532
  252. def OAI.SnakyPrototype.Certificate21.childrenH_512 line 533
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_512 line 534
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_512 line 535
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_512 line 537
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_512 line 541
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_512 line 543
  258. def OAI.SnakyPrototype.Certificate21.checked_512 line 547
  259. def OAI.SnakyPrototype.Certificate21.height_514 line 555
  260. def OAI.SnakyPrototype.Certificate21.childrenH_514 line 556
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_514 line 557
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_514 line 558
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_514 line 560
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_514 line 564
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_514 line 566
  266. def OAI.SnakyPrototype.Certificate21.checked_514 line 570
  267. def OAI.SnakyPrototype.Certificate21.height_519 line 578
  268. def OAI.SnakyPrototype.Certificate21.childrenH_519 line 579
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_519 line 580
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_519 line 581
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_519 line 583
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_519 line 587
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_519 line 589
  274. def OAI.SnakyPrototype.Certificate21.checked_519 line 593
  275. def OAI.SnakyPrototype.Certificate21.height_528_i0 line 601
  276. def OAI.SnakyPrototype.Certificate21.childrenH_528_i0 line 602
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_528_i0 line 603
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_528_i0 line 604
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_528_i0 line 606
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_528_i0 line 610
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_528_i0 line 612
  282. def OAI.SnakyPrototype.Certificate21.checked_528_i0 line 616
  283. def OAI.SnakyPrototype.Certificate21.height_528_i1 line 624
  284. def OAI.SnakyPrototype.Certificate21.childrenH_528_i1 line 625
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_528_i1 line 626
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_528_i1 line 627
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_528_i1 line 629
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_528_i1 line 633
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_528_i1 line 635
  290. def OAI.SnakyPrototype.Certificate21.checked_528_i1 line 639
  291. def OAI.SnakyPrototype.Certificate21.height_528 line 647
  292. def OAI.SnakyPrototype.Certificate21.childrenH_528 line 648
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_528 line 649
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_528 line 650
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_528 line 652
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_528 line 656
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_528 line 658
  298. def OAI.SnakyPrototype.Certificate21.checked_528 line 662
  299. def OAI.SnakyPrototype.Certificate21.height_531 line 670
  300. def OAI.SnakyPrototype.Certificate21.childrenH_531 line 671
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_531 line 672
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_531 line 673
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_531 line 675
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_531 line 679
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_531 line 681
  306. def OAI.SnakyPrototype.Certificate21.checked_531 line 685
  307. def OAI.SnakyPrototype.Certificate21.height_536 line 693
  308. def OAI.SnakyPrototype.Certificate21.childrenH_536 line 694
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_536 line 695
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_536 line 696
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_536 line 698
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_536 line 702
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_536 line 704
  314. def OAI.SnakyPrototype.Certificate21.checked_536 line 708
  315. def OAI.SnakyPrototype.Certificate21.height_537_i0 line 716
  316. def OAI.SnakyPrototype.Certificate21.childrenH_537_i0 line 717
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i0 line 718
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i0 line 719
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i0 line 721
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i0 line 725
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i0 line 727
  322. def OAI.SnakyPrototype.Certificate21.checked_537_i0 line 731
  323. def OAI.SnakyPrototype.Certificate21.height_537_i2 line 739
  324. def OAI.SnakyPrototype.Certificate21.childrenH_537_i2 line 740
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i2 line 741
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i2 line 742
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i2 line 744
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i2 line 748
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i2 line 750
  330. def OAI.SnakyPrototype.Certificate21.checked_537_i2 line 754
  331. def OAI.SnakyPrototype.Certificate21.height_537_i6 line 762
  332. def OAI.SnakyPrototype.Certificate21.childrenH_537_i6 line 763
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i6 line 764
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i6 line 765
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i6 line 767
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i6 line 771
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i6 line 773
  338. def OAI.SnakyPrototype.Certificate21.checked_537_i6 line 777
  339. def OAI.SnakyPrototype.Certificate21.height_537_i5 line 785
  340. def OAI.SnakyPrototype.Certificate21.childrenH_537_i5 line 786
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i5 line 787
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i5 line 788
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i5 line 790
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i5 line 794
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i5 line 796
  346. def OAI.SnakyPrototype.Certificate21.checked_537_i5 line 800
  347. def OAI.SnakyPrototype.Certificate21.height_537_i4 line 808
  348. def OAI.SnakyPrototype.Certificate21.childrenH_537_i4 line 809
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i4 line 810
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i4 line 811
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i4 line 813
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i4 line 817
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i4 line 819
  354. def OAI.SnakyPrototype.Certificate21.checked_537_i4 line 823
  355. def OAI.SnakyPrototype.Certificate21.height_537_i3 line 831
  356. def OAI.SnakyPrototype.Certificate21.childrenH_537_i3 line 832
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i3 line 833
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i3 line 834
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i3 line 836
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i3 line 840
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i3 line 842
  362. def OAI.SnakyPrototype.Certificate21.checked_537_i3 line 846
  363. def OAI.SnakyPrototype.Certificate21.height_537_i1 line 854
  364. def OAI.SnakyPrototype.Certificate21.childrenH_537_i1 line 855
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_537_i1 line 856
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_537_i1 line 857
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_537_i1 line 859
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537_i1 line 863
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537_i1 line 865
  370. def OAI.SnakyPrototype.Certificate21.checked_537_i1 line 869
  371. def OAI.SnakyPrototype.Certificate21.height_537 line 877
  372. def OAI.SnakyPrototype.Certificate21.childrenH_537 line 878
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_537 line 879
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_537 line 880
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_537 line 882
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_537 line 886
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_537 line 888
  378. def OAI.SnakyPrototype.Certificate21.checked_537 line 892