OAI/GameTheory/SnakyTwentyOne/Cards/Height17Part01.lean

GitHub source file

270 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_623_i0 line 36
  2. def OAI.SnakyPrototype.Certificate21.envelope_623_i0 line 37
  3. def OAI.SnakyPrototype.Certificate21.childrenC_623_i0 line 38
  4. def OAI.SnakyPrototype.Certificate21.childrenD_623_i0 line 39
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i0 line 40
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i0 line 41
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i0 line 42
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i0 line 43
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i0 line 44
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i0 line 51
  11. def OAI.SnakyPrototype.Certificate21.required_623_i1 line 56
  12. def OAI.SnakyPrototype.Certificate21.envelope_623_i1 line 57
  13. def OAI.SnakyPrototype.Certificate21.childrenC_623_i1 line 58
  14. def OAI.SnakyPrototype.Certificate21.childrenD_623_i1 line 59
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i1 line 60
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i1 line 61
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i1 line 62
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i1 line 63
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i1 line 64
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i1 line 72
  21. def OAI.SnakyPrototype.Certificate21.required_623_i4 line 77
  22. def OAI.SnakyPrototype.Certificate21.envelope_623_i4 line 78
  23. def OAI.SnakyPrototype.Certificate21.childrenC_623_i4 line 79
  24. def OAI.SnakyPrototype.Certificate21.childrenD_623_i4 line 80
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i4 line 81
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i4 line 82
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i4 line 83
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i4 line 84
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i4 line 85
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i4 line 90
  31. def OAI.SnakyPrototype.Certificate21.required_623_i3 line 95
  32. def OAI.SnakyPrototype.Certificate21.envelope_623_i3 line 96
  33. def OAI.SnakyPrototype.Certificate21.childrenC_623_i3 line 97
  34. def OAI.SnakyPrototype.Certificate21.childrenD_623_i3 line 98
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i3 line 99
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i3 line 100
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i3 line 101
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i3 line 102
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i3 line 103
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i3 line 111
  41. def OAI.SnakyPrototype.Certificate21.required_623_i5 line 116
  42. def OAI.SnakyPrototype.Certificate21.envelope_623_i5 line 117
  43. def OAI.SnakyPrototype.Certificate21.childrenC_623_i5 line 118
  44. def OAI.SnakyPrototype.Certificate21.childrenD_623_i5 line 119
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i5 line 120
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i5 line 121
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i5 line 122
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i5 line 123
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i5 line 124
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i5 line 130
  51. def OAI.SnakyPrototype.Certificate21.required_623_i2 line 135
  52. def OAI.SnakyPrototype.Certificate21.envelope_623_i2 line 136
  53. def OAI.SnakyPrototype.Certificate21.childrenC_623_i2 line 137
  54. def OAI.SnakyPrototype.Certificate21.childrenD_623_i2 line 138
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i2 line 139
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i2 line 140
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i2 line 141
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i2 line 142
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i2 line 143
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i2 line 153
  61. def OAI.SnakyPrototype.Certificate21.required_623_i7 line 158
  62. def OAI.SnakyPrototype.Certificate21.envelope_623_i7 line 159
  63. def OAI.SnakyPrototype.Certificate21.childrenC_623_i7 line 160
  64. def OAI.SnakyPrototype.Certificate21.childrenD_623_i7 line 161
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i7 line 162
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i7 line 163
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i7 line 164
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i7 line 165
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i7 line 166
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i7 line 172
  71. def OAI.SnakyPrototype.Certificate21.required_623_i6 line 177
  72. def OAI.SnakyPrototype.Certificate21.envelope_623_i6 line 178
  73. def OAI.SnakyPrototype.Certificate21.childrenC_623_i6 line 179
  74. def OAI.SnakyPrototype.Certificate21.childrenD_623_i6 line 180
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_623_i6 line 181
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623_i6 line 182
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623_i6 line 183
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623_i6 line 184
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_623_i6 line 185
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_623_i6 line 194
  81. def OAI.SnakyPrototype.Certificate21.required_623 line 199
  82. def OAI.SnakyPrototype.Certificate21.envelope_623 line 200
  83. def OAI.SnakyPrototype.Certificate21.childrenC_623 line 201
  84. def OAI.SnakyPrototype.Certificate21.childrenD_623 line 202
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_623 line 203
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_623 line 204
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_623 line 205
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_623 line 206
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_623 line 207
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_623 line 221
  91. def OAI.SnakyPrototype.Certificate21.required_630_i0 line 226
  92. def OAI.SnakyPrototype.Certificate21.envelope_630_i0 line 227
  93. def OAI.SnakyPrototype.Certificate21.childrenC_630_i0 line 228
  94. def OAI.SnakyPrototype.Certificate21.childrenD_630_i0 line 229
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_630_i0 line 230
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_630_i0 line 231
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_630_i0 line 232
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_630_i0 line 233
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_630_i0 line 234
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_630_i0 line 244
  101. def OAI.SnakyPrototype.Certificate21.required_630_i1 line 249
  102. def OAI.SnakyPrototype.Certificate21.envelope_630_i1 line 250
  103. def OAI.SnakyPrototype.Certificate21.childrenC_630_i1 line 251
  104. def OAI.SnakyPrototype.Certificate21.childrenD_630_i1 line 252
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_630_i1 line 253
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_630_i1 line 254
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_630_i1 line 255
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_630_i1 line 256
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_630_i1 line 257
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_630_i1 line 264
  111. def OAI.SnakyPrototype.Certificate21.required_630_i2 line 269
  112. def OAI.SnakyPrototype.Certificate21.envelope_630_i2 line 270
  113. def OAI.SnakyPrototype.Certificate21.childrenC_630_i2 line 271
  114. def OAI.SnakyPrototype.Certificate21.childrenD_630_i2 line 272
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_630_i2 line 273
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_630_i2 line 274
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_630_i2 line 275
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_630_i2 line 276
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_630_i2 line 277
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_630_i2 line 285
  121. def OAI.SnakyPrototype.Certificate21.required_630_i4 line 290
  122. def OAI.SnakyPrototype.Certificate21.envelope_630_i4 line 291
  123. def OAI.SnakyPrototype.Certificate21.childrenC_630_i4 line 292
  124. def OAI.SnakyPrototype.Certificate21.childrenD_630_i4 line 293
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_630_i4 line 294
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_630_i4 line 295
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_630_i4 line 296
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_630_i4 line 297
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_630_i4 line 298
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_630_i4 line 303
  131. def OAI.SnakyPrototype.Certificate21.required_630_i3 line 308
  132. def OAI.SnakyPrototype.Certificate21.envelope_630_i3 line 309
  133. def OAI.SnakyPrototype.Certificate21.childrenC_630_i3 line 310
  134. def OAI.SnakyPrototype.Certificate21.childrenD_630_i3 line 311
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_630_i3 line 312
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_630_i3 line 313
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_630_i3 line 314
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_630_i3 line 315
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_630_i3 line 316
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_630_i3 line 324
  141. def OAI.SnakyPrototype.Certificate21.required_630 line 329
  142. def OAI.SnakyPrototype.Certificate21.envelope_630 line 330
  143. def OAI.SnakyPrototype.Certificate21.childrenC_630 line 331
  144. def OAI.SnakyPrototype.Certificate21.childrenD_630 line 332
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_630 line 333
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_630 line 334
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_630 line 335
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_630 line 336
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_630 line 337
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_630 line 349
  151. def OAI.SnakyPrototype.Certificate21.height_623_i0 line 354
  152. def OAI.SnakyPrototype.Certificate21.childrenH_623_i0 line 355
  153. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i0 line 356
  154. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i0 line 357
  155. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i0 line 359
  156. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i0 line 363
  157. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i0 line 365
  158. def OAI.SnakyPrototype.Certificate21.checked_623_i0 line 369
  159. def OAI.SnakyPrototype.Certificate21.height_623_i1 line 377
  160. def OAI.SnakyPrototype.Certificate21.childrenH_623_i1 line 378
  161. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i1 line 379
  162. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i1 line 380
  163. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i1 line 382
  164. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i1 line 386
  165. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i1 line 388
  166. def OAI.SnakyPrototype.Certificate21.checked_623_i1 line 392
  167. def OAI.SnakyPrototype.Certificate21.height_623_i4 line 400
  168. def OAI.SnakyPrototype.Certificate21.childrenH_623_i4 line 401
  169. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i4 line 402
  170. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i4 line 403
  171. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i4 line 405
  172. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i4 line 409
  173. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i4 line 411
  174. def OAI.SnakyPrototype.Certificate21.checked_623_i4 line 415
  175. def OAI.SnakyPrototype.Certificate21.height_623_i3 line 423
  176. def OAI.SnakyPrototype.Certificate21.childrenH_623_i3 line 424
  177. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i3 line 425
  178. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i3 line 426
  179. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i3 line 428
  180. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i3 line 432
  181. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i3 line 434
  182. def OAI.SnakyPrototype.Certificate21.checked_623_i3 line 438
  183. def OAI.SnakyPrototype.Certificate21.height_623_i5 line 446
  184. def OAI.SnakyPrototype.Certificate21.childrenH_623_i5 line 447
  185. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i5 line 448
  186. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i5 line 449
  187. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i5 line 451
  188. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i5 line 455
  189. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i5 line 457
  190. def OAI.SnakyPrototype.Certificate21.checked_623_i5 line 461
  191. def OAI.SnakyPrototype.Certificate21.height_623_i2 line 469
  192. def OAI.SnakyPrototype.Certificate21.childrenH_623_i2 line 470
  193. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i2 line 471
  194. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i2 line 472
  195. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i2 line 474
  196. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i2 line 478
  197. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i2 line 480
  198. def OAI.SnakyPrototype.Certificate21.checked_623_i2 line 484
  199. def OAI.SnakyPrototype.Certificate21.height_623_i7 line 492
  200. def OAI.SnakyPrototype.Certificate21.childrenH_623_i7 line 493
  201. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i7 line 494
  202. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i7 line 495
  203. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i7 line 497
  204. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i7 line 501
  205. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i7 line 503
  206. def OAI.SnakyPrototype.Certificate21.checked_623_i7 line 507
  207. def OAI.SnakyPrototype.Certificate21.height_623_i6 line 515
  208. def OAI.SnakyPrototype.Certificate21.childrenH_623_i6 line 516
  209. theorem OAI.SnakyPrototype.Certificate21.height_exact_623_i6 line 517
  210. theorem OAI.SnakyPrototype.Certificate21.required_origin_623_i6 line 518
  211. theorem OAI.SnakyPrototype.Certificate21.required_exact_623_i6 line 520
  212. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623_i6 line 524
  213. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623_i6 line 526
  214. def OAI.SnakyPrototype.Certificate21.checked_623_i6 line 530
  215. def OAI.SnakyPrototype.Certificate21.height_623 line 538
  216. def OAI.SnakyPrototype.Certificate21.childrenH_623 line 539
  217. theorem OAI.SnakyPrototype.Certificate21.height_exact_623 line 540
  218. theorem OAI.SnakyPrototype.Certificate21.required_origin_623 line 541
  219. theorem OAI.SnakyPrototype.Certificate21.required_exact_623 line 543
  220. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_623 line 547
  221. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_623 line 549
  222. def OAI.SnakyPrototype.Certificate21.checked_623 line 553
  223. def OAI.SnakyPrototype.Certificate21.height_630_i0 line 561
  224. def OAI.SnakyPrototype.Certificate21.childrenH_630_i0 line 562
  225. theorem OAI.SnakyPrototype.Certificate21.height_exact_630_i0 line 563
  226. theorem OAI.SnakyPrototype.Certificate21.required_origin_630_i0 line 564
  227. theorem OAI.SnakyPrototype.Certificate21.required_exact_630_i0 line 566
  228. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_630_i0 line 570
  229. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_630_i0 line 572
  230. def OAI.SnakyPrototype.Certificate21.checked_630_i0 line 576
  231. def OAI.SnakyPrototype.Certificate21.height_630_i1 line 584
  232. def OAI.SnakyPrototype.Certificate21.childrenH_630_i1 line 585
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_630_i1 line 586
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_630_i1 line 587
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_630_i1 line 589
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_630_i1 line 593
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_630_i1 line 595
  238. def OAI.SnakyPrototype.Certificate21.checked_630_i1 line 599
  239. def OAI.SnakyPrototype.Certificate21.height_630_i2 line 607
  240. def OAI.SnakyPrototype.Certificate21.childrenH_630_i2 line 608
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_630_i2 line 609
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_630_i2 line 610
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_630_i2 line 612
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_630_i2 line 616
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_630_i2 line 618
  246. def OAI.SnakyPrototype.Certificate21.checked_630_i2 line 622
  247. def OAI.SnakyPrototype.Certificate21.height_630_i4 line 630
  248. def OAI.SnakyPrototype.Certificate21.childrenH_630_i4 line 631
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_630_i4 line 632
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_630_i4 line 633
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_630_i4 line 635
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_630_i4 line 639
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_630_i4 line 641
  254. def OAI.SnakyPrototype.Certificate21.checked_630_i4 line 645
  255. def OAI.SnakyPrototype.Certificate21.height_630_i3 line 653
  256. def OAI.SnakyPrototype.Certificate21.childrenH_630_i3 line 654
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_630_i3 line 655
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_630_i3 line 656
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_630_i3 line 658
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_630_i3 line 662
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_630_i3 line 664
  262. def OAI.SnakyPrototype.Certificate21.checked_630_i3 line 668
  263. def OAI.SnakyPrototype.Certificate21.height_630 line 676
  264. def OAI.SnakyPrototype.Certificate21.childrenH_630 line 677
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_630 line 678
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_630 line 679
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_630 line 681
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_630 line 685
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_630 line 687
  270. def OAI.SnakyPrototype.Certificate21.checked_630 line 691