OAI/GameTheory/SnakyTwentyOne/Cards/Height02Part02.lean

GitHub source file

324 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_96 line 9
  2. def OAI.SnakyPrototype.Certificate21.envelope_96 line 10
  3. def OAI.SnakyPrototype.Certificate21.childrenC_96 line 11
  4. def OAI.SnakyPrototype.Certificate21.childrenD_96 line 12
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_96 line 13
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_96 line 14
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_96 line 15
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_96 line 16
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_96 line 17
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_96 line 22
  11. def OAI.SnakyPrototype.Certificate21.required_102 line 27
  12. def OAI.SnakyPrototype.Certificate21.envelope_102 line 28
  13. def OAI.SnakyPrototype.Certificate21.childrenC_102 line 29
  14. def OAI.SnakyPrototype.Certificate21.childrenD_102 line 30
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_102 line 31
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_102 line 32
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_102 line 33
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_102 line 34
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_102 line 35
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_102 line 40
  21. def OAI.SnakyPrototype.Certificate21.required_121 line 45
  22. def OAI.SnakyPrototype.Certificate21.envelope_121 line 46
  23. def OAI.SnakyPrototype.Certificate21.childrenC_121 line 47
  24. def OAI.SnakyPrototype.Certificate21.childrenD_121 line 48
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_121 line 49
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_121 line 50
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_121 line 51
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_121 line 52
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_121 line 53
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_121 line 58
  31. def OAI.SnakyPrototype.Certificate21.required_123 line 63
  32. def OAI.SnakyPrototype.Certificate21.envelope_123 line 64
  33. def OAI.SnakyPrototype.Certificate21.childrenC_123 line 65
  34. def OAI.SnakyPrototype.Certificate21.childrenD_123 line 66
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_123 line 67
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_123 line 68
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_123 line 69
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_123 line 70
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_123 line 71
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_123 line 76
  41. def OAI.SnakyPrototype.Certificate21.required_129 line 81
  42. def OAI.SnakyPrototype.Certificate21.envelope_129 line 82
  43. def OAI.SnakyPrototype.Certificate21.childrenC_129 line 83
  44. def OAI.SnakyPrototype.Certificate21.childrenD_129 line 84
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_129 line 85
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_129 line 86
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_129 line 87
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_129 line 88
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_129 line 89
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_129 line 94
  51. def OAI.SnakyPrototype.Certificate21.required_138 line 99
  52. def OAI.SnakyPrototype.Certificate21.envelope_138 line 100
  53. def OAI.SnakyPrototype.Certificate21.childrenC_138 line 101
  54. def OAI.SnakyPrototype.Certificate21.childrenD_138 line 102
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_138 line 103
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_138 line 104
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_138 line 105
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_138 line 106
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_138 line 107
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_138 line 112
  61. def OAI.SnakyPrototype.Certificate21.required_146 line 117
  62. def OAI.SnakyPrototype.Certificate21.envelope_146 line 118
  63. def OAI.SnakyPrototype.Certificate21.childrenC_146 line 119
  64. def OAI.SnakyPrototype.Certificate21.childrenD_146 line 120
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_146 line 121
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_146 line 122
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_146 line 123
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_146 line 124
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_146 line 125
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_146 line 130
  71. def OAI.SnakyPrototype.Certificate21.required_153 line 135
  72. def OAI.SnakyPrototype.Certificate21.envelope_153 line 136
  73. def OAI.SnakyPrototype.Certificate21.childrenC_153 line 137
  74. def OAI.SnakyPrototype.Certificate21.childrenD_153 line 138
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_153 line 139
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_153 line 140
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_153 line 141
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_153 line 142
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_153 line 143
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_153 line 148
  81. def OAI.SnakyPrototype.Certificate21.required_154 line 153
  82. def OAI.SnakyPrototype.Certificate21.envelope_154 line 154
  83. def OAI.SnakyPrototype.Certificate21.childrenC_154 line 155
  84. def OAI.SnakyPrototype.Certificate21.childrenD_154 line 156
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_154 line 157
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_154 line 158
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_154 line 159
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_154 line 160
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_154 line 161
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_154 line 166
  91. def OAI.SnakyPrototype.Certificate21.required_156 line 171
  92. def OAI.SnakyPrototype.Certificate21.envelope_156 line 172
  93. def OAI.SnakyPrototype.Certificate21.childrenC_156 line 173
  94. def OAI.SnakyPrototype.Certificate21.childrenD_156 line 174
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_156 line 175
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_156 line 176
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_156 line 177
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_156 line 178
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_156 line 179
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_156 line 184
  101. def OAI.SnakyPrototype.Certificate21.required_169 line 189
  102. def OAI.SnakyPrototype.Certificate21.envelope_169 line 190
  103. def OAI.SnakyPrototype.Certificate21.childrenC_169 line 191
  104. def OAI.SnakyPrototype.Certificate21.childrenD_169 line 192
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_169 line 193
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_169 line 194
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_169 line 195
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_169 line 196
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_169 line 197
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_169 line 202
  111. def OAI.SnakyPrototype.Certificate21.required_170 line 207
  112. def OAI.SnakyPrototype.Certificate21.envelope_170 line 208
  113. def OAI.SnakyPrototype.Certificate21.childrenC_170 line 209
  114. def OAI.SnakyPrototype.Certificate21.childrenD_170 line 210
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_170 line 211
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_170 line 212
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_170 line 213
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_170 line 214
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_170 line 215
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_170 line 220
  121. def OAI.SnakyPrototype.Certificate21.required_200 line 225
  122. def OAI.SnakyPrototype.Certificate21.envelope_200 line 226
  123. def OAI.SnakyPrototype.Certificate21.childrenC_200 line 227
  124. def OAI.SnakyPrototype.Certificate21.childrenD_200 line 228
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_200 line 229
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_200 line 230
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_200 line 231
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_200 line 232
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_200 line 233
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_200 line 238
  131. def OAI.SnakyPrototype.Certificate21.required_210 line 243
  132. def OAI.SnakyPrototype.Certificate21.envelope_210 line 244
  133. def OAI.SnakyPrototype.Certificate21.childrenC_210 line 245
  134. def OAI.SnakyPrototype.Certificate21.childrenD_210 line 246
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_210 line 247
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_210 line 248
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_210 line 249
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_210 line 250
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_210 line 251
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_210 line 256
  141. def OAI.SnakyPrototype.Certificate21.required_220 line 261
  142. def OAI.SnakyPrototype.Certificate21.envelope_220 line 262
  143. def OAI.SnakyPrototype.Certificate21.childrenC_220 line 263
  144. def OAI.SnakyPrototype.Certificate21.childrenD_220 line 264
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_220 line 265
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_220 line 266
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_220 line 267
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_220 line 268
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_220 line 269
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_220 line 274
  151. def OAI.SnakyPrototype.Certificate21.required_224 line 279
  152. def OAI.SnakyPrototype.Certificate21.envelope_224 line 280
  153. def OAI.SnakyPrototype.Certificate21.childrenC_224 line 281
  154. def OAI.SnakyPrototype.Certificate21.childrenD_224 line 282
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_224 line 283
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_224 line 284
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_224 line 285
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_224 line 286
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_224 line 287
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_224 line 292
  161. def OAI.SnakyPrototype.Certificate21.required_244 line 297
  162. def OAI.SnakyPrototype.Certificate21.envelope_244 line 298
  163. def OAI.SnakyPrototype.Certificate21.childrenC_244 line 299
  164. def OAI.SnakyPrototype.Certificate21.childrenD_244 line 300
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_244 line 301
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_244 line 302
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_244 line 303
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_244 line 304
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_244 line 305
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_244 line 310
  171. def OAI.SnakyPrototype.Certificate21.required_281 line 315
  172. def OAI.SnakyPrototype.Certificate21.envelope_281 line 316
  173. def OAI.SnakyPrototype.Certificate21.childrenC_281 line 317
  174. def OAI.SnakyPrototype.Certificate21.childrenD_281 line 318
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_281 line 319
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_281 line 320
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_281 line 321
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_281 line 322
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_281 line 323
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_281 line 328
  181. def OAI.SnakyPrototype.Certificate21.height_96 line 333
  182. def OAI.SnakyPrototype.Certificate21.childrenH_96 line 334
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_96 line 335
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_96 line 336
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_96 line 338
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_96 line 342
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_96 line 344
  188. def OAI.SnakyPrototype.Certificate21.checked_96 line 348
  189. def OAI.SnakyPrototype.Certificate21.height_102 line 356
  190. def OAI.SnakyPrototype.Certificate21.childrenH_102 line 357
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_102 line 358
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_102 line 359
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_102 line 361
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_102 line 365
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_102 line 367
  196. def OAI.SnakyPrototype.Certificate21.checked_102 line 371
  197. def OAI.SnakyPrototype.Certificate21.height_121 line 379
  198. def OAI.SnakyPrototype.Certificate21.childrenH_121 line 380
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_121 line 381
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_121 line 382
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_121 line 384
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_121 line 388
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_121 line 390
  204. def OAI.SnakyPrototype.Certificate21.checked_121 line 394
  205. def OAI.SnakyPrototype.Certificate21.height_123 line 402
  206. def OAI.SnakyPrototype.Certificate21.childrenH_123 line 403
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_123 line 404
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_123 line 405
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_123 line 407
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_123 line 411
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_123 line 413
  212. def OAI.SnakyPrototype.Certificate21.checked_123 line 417
  213. def OAI.SnakyPrototype.Certificate21.height_129 line 425
  214. def OAI.SnakyPrototype.Certificate21.childrenH_129 line 426
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_129 line 427
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_129 line 428
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_129 line 430
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_129 line 434
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_129 line 436
  220. def OAI.SnakyPrototype.Certificate21.checked_129 line 440
  221. def OAI.SnakyPrototype.Certificate21.height_138 line 448
  222. def OAI.SnakyPrototype.Certificate21.childrenH_138 line 449
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_138 line 450
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_138 line 451
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_138 line 453
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_138 line 457
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_138 line 459
  228. def OAI.SnakyPrototype.Certificate21.checked_138 line 463
  229. def OAI.SnakyPrototype.Certificate21.height_146 line 471
  230. def OAI.SnakyPrototype.Certificate21.childrenH_146 line 472
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_146 line 473
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_146 line 474
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_146 line 476
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_146 line 480
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_146 line 482
  236. def OAI.SnakyPrototype.Certificate21.checked_146 line 486
  237. def OAI.SnakyPrototype.Certificate21.height_153 line 494
  238. def OAI.SnakyPrototype.Certificate21.childrenH_153 line 495
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_153 line 496
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_153 line 497
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_153 line 499
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_153 line 503
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_153 line 505
  244. def OAI.SnakyPrototype.Certificate21.checked_153 line 509
  245. def OAI.SnakyPrototype.Certificate21.height_154 line 517
  246. def OAI.SnakyPrototype.Certificate21.childrenH_154 line 518
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_154 line 519
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_154 line 520
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_154 line 522
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_154 line 526
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_154 line 528
  252. def OAI.SnakyPrototype.Certificate21.checked_154 line 532
  253. def OAI.SnakyPrototype.Certificate21.height_156 line 540
  254. def OAI.SnakyPrototype.Certificate21.childrenH_156 line 541
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_156 line 542
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_156 line 543
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_156 line 545
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_156 line 549
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_156 line 551
  260. def OAI.SnakyPrototype.Certificate21.checked_156 line 555
  261. def OAI.SnakyPrototype.Certificate21.height_169 line 563
  262. def OAI.SnakyPrototype.Certificate21.childrenH_169 line 564
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_169 line 565
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_169 line 566
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_169 line 568
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_169 line 572
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_169 line 574
  268. def OAI.SnakyPrototype.Certificate21.checked_169 line 578
  269. def OAI.SnakyPrototype.Certificate21.height_170 line 586
  270. def OAI.SnakyPrototype.Certificate21.childrenH_170 line 587
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_170 line 588
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_170 line 589
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_170 line 591
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_170 line 595
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_170 line 597
  276. def OAI.SnakyPrototype.Certificate21.checked_170 line 601
  277. def OAI.SnakyPrototype.Certificate21.height_200 line 609
  278. def OAI.SnakyPrototype.Certificate21.childrenH_200 line 610
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_200 line 611
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_200 line 612
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_200 line 614
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_200 line 618
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_200 line 620
  284. def OAI.SnakyPrototype.Certificate21.checked_200 line 624
  285. def OAI.SnakyPrototype.Certificate21.height_210 line 632
  286. def OAI.SnakyPrototype.Certificate21.childrenH_210 line 633
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_210 line 634
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_210 line 635
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_210 line 637
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_210 line 641
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_210 line 643
  292. def OAI.SnakyPrototype.Certificate21.checked_210 line 647
  293. def OAI.SnakyPrototype.Certificate21.height_220 line 655
  294. def OAI.SnakyPrototype.Certificate21.childrenH_220 line 656
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_220 line 657
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_220 line 658
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_220 line 660
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_220 line 664
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_220 line 666
  300. def OAI.SnakyPrototype.Certificate21.checked_220 line 670
  301. def OAI.SnakyPrototype.Certificate21.height_224 line 678
  302. def OAI.SnakyPrototype.Certificate21.childrenH_224 line 679
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_224 line 680
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_224 line 681
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_224 line 683
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_224 line 687
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_224 line 689
  308. def OAI.SnakyPrototype.Certificate21.checked_224 line 693
  309. def OAI.SnakyPrototype.Certificate21.height_244 line 701
  310. def OAI.SnakyPrototype.Certificate21.childrenH_244 line 702
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_244 line 703
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_244 line 704
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_244 line 706
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_244 line 710
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_244 line 712
  316. def OAI.SnakyPrototype.Certificate21.checked_244 line 716
  317. def OAI.SnakyPrototype.Certificate21.height_281 line 724
  318. def OAI.SnakyPrototype.Certificate21.childrenH_281 line 725
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_281 line 726
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_281 line 727
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_281 line 729
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_281 line 733
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_281 line 735
  324. def OAI.SnakyPrototype.Certificate21.checked_281 line 739