OAI/GameTheory/SnakyTwentyOne/Cards/Height07Part03.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_447_i0 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_447_i0 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_447_i0 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_447_i0 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_447_i0 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_447_i0 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_447_i0 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_447_i0 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_447_i0 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_447_i0 line 33
  11. def OAI.SnakyPrototype.Certificate21.required_447 line 38
  12. def OAI.SnakyPrototype.Certificate21.envelope_447 line 39
  13. def OAI.SnakyPrototype.Certificate21.childrenC_447 line 40
  14. def OAI.SnakyPrototype.Certificate21.childrenD_447 line 41
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_447 line 42
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_447 line 43
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_447 line 44
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_447 line 45
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_447 line 46
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_447 line 51
  21. def OAI.SnakyPrototype.Certificate21.required_453_i1 line 56
  22. def OAI.SnakyPrototype.Certificate21.envelope_453_i1 line 57
  23. def OAI.SnakyPrototype.Certificate21.childrenC_453_i1 line 58
  24. def OAI.SnakyPrototype.Certificate21.childrenD_453_i1 line 59
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_453_i1 line 60
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_453_i1 line 61
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_453_i1 line 62
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_453_i1 line 63
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_453_i1 line 64
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_453_i1 line 70
  31. def OAI.SnakyPrototype.Certificate21.required_453_i0 line 75
  32. def OAI.SnakyPrototype.Certificate21.envelope_453_i0 line 76
  33. def OAI.SnakyPrototype.Certificate21.childrenC_453_i0 line 77
  34. def OAI.SnakyPrototype.Certificate21.childrenD_453_i0 line 78
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_453_i0 line 79
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_453_i0 line 80
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_453_i0 line 81
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_453_i0 line 82
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_453_i0 line 83
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_453_i0 line 88
  41. def OAI.SnakyPrototype.Certificate21.required_453 line 93
  42. def OAI.SnakyPrototype.Certificate21.envelope_453 line 94
  43. def OAI.SnakyPrototype.Certificate21.childrenC_453 line 95
  44. def OAI.SnakyPrototype.Certificate21.childrenD_453 line 96
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_453 line 97
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_453 line 98
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_453 line 99
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_453 line 100
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_453 line 101
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_453 line 106
  51. def OAI.SnakyPrototype.Certificate21.required_466 line 111
  52. def OAI.SnakyPrototype.Certificate21.envelope_466 line 112
  53. def OAI.SnakyPrototype.Certificate21.childrenC_466 line 113
  54. def OAI.SnakyPrototype.Certificate21.childrenD_466 line 114
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_466 line 115
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_466 line 116
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_466 line 117
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_466 line 118
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_466 line 119
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_466 line 126
  61. def OAI.SnakyPrototype.Certificate21.required_469_i0 line 131
  62. def OAI.SnakyPrototype.Certificate21.envelope_469_i0 line 132
  63. def OAI.SnakyPrototype.Certificate21.childrenC_469_i0 line 133
  64. def OAI.SnakyPrototype.Certificate21.childrenD_469_i0 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_469_i0 line 135
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_469_i0 line 136
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_469_i0 line 137
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_469_i0 line 138
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_469_i0 line 139
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_469_i0 line 144
  71. def OAI.SnakyPrototype.Certificate21.required_469 line 149
  72. def OAI.SnakyPrototype.Certificate21.envelope_469 line 150
  73. def OAI.SnakyPrototype.Certificate21.childrenC_469 line 151
  74. def OAI.SnakyPrototype.Certificate21.childrenD_469 line 152
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_469 line 153
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_469 line 154
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_469 line 155
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_469 line 156
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_469 line 157
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_469 line 162
  81. def OAI.SnakyPrototype.Certificate21.required_472 line 167
  82. def OAI.SnakyPrototype.Certificate21.envelope_472 line 168
  83. def OAI.SnakyPrototype.Certificate21.childrenC_472 line 169
  84. def OAI.SnakyPrototype.Certificate21.childrenD_472 line 170
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_472 line 171
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_472 line 172
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_472 line 173
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_472 line 174
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_472 line 175
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_472 line 180
  91. def OAI.SnakyPrototype.Certificate21.required_487 line 185
  92. def OAI.SnakyPrototype.Certificate21.envelope_487 line 186
  93. def OAI.SnakyPrototype.Certificate21.childrenC_487 line 187
  94. def OAI.SnakyPrototype.Certificate21.childrenD_487 line 188
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_487 line 189
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_487 line 190
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_487 line 191
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_487 line 192
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_487 line 193
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_487 line 198
  101. def OAI.SnakyPrototype.Certificate21.required_488_i1 line 203
  102. def OAI.SnakyPrototype.Certificate21.envelope_488_i1 line 204
  103. def OAI.SnakyPrototype.Certificate21.childrenC_488_i1 line 205
  104. def OAI.SnakyPrototype.Certificate21.childrenD_488_i1 line 206
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_488_i1 line 207
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_488_i1 line 208
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_488_i1 line 209
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_488_i1 line 210
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_488_i1 line 211
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_488_i1 line 216
  111. def OAI.SnakyPrototype.Certificate21.required_488_i0 line 221
  112. def OAI.SnakyPrototype.Certificate21.envelope_488_i0 line 222
  113. def OAI.SnakyPrototype.Certificate21.childrenC_488_i0 line 223
  114. def OAI.SnakyPrototype.Certificate21.childrenD_488_i0 line 224
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_488_i0 line 225
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_488_i0 line 226
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_488_i0 line 227
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_488_i0 line 228
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_488_i0 line 229
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_488_i0 line 234
  121. def OAI.SnakyPrototype.Certificate21.required_488_i2 line 239
  122. def OAI.SnakyPrototype.Certificate21.envelope_488_i2 line 240
  123. def OAI.SnakyPrototype.Certificate21.childrenC_488_i2 line 241
  124. def OAI.SnakyPrototype.Certificate21.childrenD_488_i2 line 242
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_488_i2 line 243
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_488_i2 line 244
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_488_i2 line 245
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_488_i2 line 246
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_488_i2 line 247
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_488_i2 line 253
  131. def OAI.SnakyPrototype.Certificate21.required_488 line 258
  132. def OAI.SnakyPrototype.Certificate21.envelope_488 line 259
  133. def OAI.SnakyPrototype.Certificate21.childrenC_488 line 260
  134. def OAI.SnakyPrototype.Certificate21.childrenD_488 line 261
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_488 line 262
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_488 line 263
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_488 line 264
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_488 line 265
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_488 line 266
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_488 line 272
  141. def OAI.SnakyPrototype.Certificate21.required_499_i0 line 277
  142. def OAI.SnakyPrototype.Certificate21.envelope_499_i0 line 278
  143. def OAI.SnakyPrototype.Certificate21.childrenC_499_i0 line 279
  144. def OAI.SnakyPrototype.Certificate21.childrenD_499_i0 line 280
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_499_i0 line 281
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_499_i0 line 282
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_499_i0 line 283
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_499_i0 line 284
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_499_i0 line 285
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_499_i0 line 290
  151. def OAI.SnakyPrototype.Certificate21.required_499_i1 line 295
  152. def OAI.SnakyPrototype.Certificate21.envelope_499_i1 line 296
  153. def OAI.SnakyPrototype.Certificate21.childrenC_499_i1 line 297
  154. def OAI.SnakyPrototype.Certificate21.childrenD_499_i1 line 298
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_499_i1 line 299
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_499_i1 line 300
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_499_i1 line 301
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_499_i1 line 302
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_499_i1 line 303
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_499_i1 line 308
  161. def OAI.SnakyPrototype.Certificate21.required_499 line 313
  162. def OAI.SnakyPrototype.Certificate21.envelope_499 line 314
  163. def OAI.SnakyPrototype.Certificate21.childrenC_499 line 315
  164. def OAI.SnakyPrototype.Certificate21.childrenD_499 line 316
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_499 line 317
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_499 line 318
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_499 line 319
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_499 line 320
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_499 line 321
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_499 line 327
  171. def OAI.SnakyPrototype.Certificate21.required_504_i1 line 332
  172. def OAI.SnakyPrototype.Certificate21.envelope_504_i1 line 333
  173. def OAI.SnakyPrototype.Certificate21.childrenC_504_i1 line 334
  174. def OAI.SnakyPrototype.Certificate21.childrenD_504_i1 line 335
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_504_i1 line 336
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_504_i1 line 337
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_504_i1 line 338
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_504_i1 line 339
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_504_i1 line 340
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_504_i1 line 345
  181. def OAI.SnakyPrototype.Certificate21.required_504_i0 line 350
  182. def OAI.SnakyPrototype.Certificate21.envelope_504_i0 line 351
  183. def OAI.SnakyPrototype.Certificate21.childrenC_504_i0 line 352
  184. def OAI.SnakyPrototype.Certificate21.childrenD_504_i0 line 353
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_504_i0 line 354
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_504_i0 line 355
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_504_i0 line 356
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_504_i0 line 357
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_504_i0 line 358
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_504_i0 line 364
  191. def OAI.SnakyPrototype.Certificate21.required_504 line 369
  192. def OAI.SnakyPrototype.Certificate21.envelope_504 line 370
  193. def OAI.SnakyPrototype.Certificate21.childrenC_504 line 371
  194. def OAI.SnakyPrototype.Certificate21.childrenD_504 line 372
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_504 line 373
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_504 line 374
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_504 line 375
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_504 line 376
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_504 line 377
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_504 line 382
  201. def OAI.SnakyPrototype.Certificate21.required_507_i0 line 387
  202. def OAI.SnakyPrototype.Certificate21.envelope_507_i0 line 388
  203. def OAI.SnakyPrototype.Certificate21.childrenC_507_i0 line 389
  204. def OAI.SnakyPrototype.Certificate21.childrenD_507_i0 line 390
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_507_i0 line 391
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_507_i0 line 392
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_507_i0 line 393
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_507_i0 line 394
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_507_i0 line 395
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_507_i0 line 401
  211. def OAI.SnakyPrototype.Certificate21.required_507 line 406
  212. def OAI.SnakyPrototype.Certificate21.envelope_507 line 407
  213. def OAI.SnakyPrototype.Certificate21.childrenC_507 line 408
  214. def OAI.SnakyPrototype.Certificate21.childrenD_507 line 409
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_507 line 410
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_507 line 411
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_507 line 412
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_507 line 413
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_507 line 414
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_507 line 421
  221. def OAI.SnakyPrototype.Certificate21.height_447_i0 line 426
  222. def OAI.SnakyPrototype.Certificate21.childrenH_447_i0 line 427
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_447_i0 line 428
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_447_i0 line 429
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_447_i0 line 431
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_447_i0 line 435
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_447_i0 line 437
  228. def OAI.SnakyPrototype.Certificate21.checked_447_i0 line 441
  229. def OAI.SnakyPrototype.Certificate21.height_447 line 449
  230. def OAI.SnakyPrototype.Certificate21.childrenH_447 line 450
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_447 line 451
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_447 line 452
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_447 line 454
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_447 line 458
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_447 line 460
  236. def OAI.SnakyPrototype.Certificate21.checked_447 line 464
  237. def OAI.SnakyPrototype.Certificate21.height_453_i1 line 472
  238. def OAI.SnakyPrototype.Certificate21.childrenH_453_i1 line 473
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_453_i1 line 474
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_453_i1 line 475
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_453_i1 line 477
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_453_i1 line 481
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_453_i1 line 483
  244. def OAI.SnakyPrototype.Certificate21.checked_453_i1 line 487
  245. def OAI.SnakyPrototype.Certificate21.height_453_i0 line 495
  246. def OAI.SnakyPrototype.Certificate21.childrenH_453_i0 line 496
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_453_i0 line 497
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_453_i0 line 498
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_453_i0 line 500
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_453_i0 line 504
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_453_i0 line 506
  252. def OAI.SnakyPrototype.Certificate21.checked_453_i0 line 510
  253. def OAI.SnakyPrototype.Certificate21.height_453 line 518
  254. def OAI.SnakyPrototype.Certificate21.childrenH_453 line 519
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_453 line 520
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_453 line 521
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_453 line 523
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_453 line 527
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_453 line 529
  260. def OAI.SnakyPrototype.Certificate21.checked_453 line 533
  261. def OAI.SnakyPrototype.Certificate21.height_466 line 541
  262. def OAI.SnakyPrototype.Certificate21.childrenH_466 line 542
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_466 line 543
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_466 line 544
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_466 line 546
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_466 line 550
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_466 line 552
  268. def OAI.SnakyPrototype.Certificate21.checked_466 line 556
  269. def OAI.SnakyPrototype.Certificate21.height_469_i0 line 564
  270. def OAI.SnakyPrototype.Certificate21.childrenH_469_i0 line 565
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_469_i0 line 566
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_469_i0 line 567
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_469_i0 line 569
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_469_i0 line 573
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_469_i0 line 575
  276. def OAI.SnakyPrototype.Certificate21.checked_469_i0 line 579
  277. def OAI.SnakyPrototype.Certificate21.height_469 line 587
  278. def OAI.SnakyPrototype.Certificate21.childrenH_469 line 588
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_469 line 589
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_469 line 590
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_469 line 592
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_469 line 596
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_469 line 598
  284. def OAI.SnakyPrototype.Certificate21.checked_469 line 602
  285. def OAI.SnakyPrototype.Certificate21.height_472 line 610
  286. def OAI.SnakyPrototype.Certificate21.childrenH_472 line 611
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_472 line 612
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_472 line 613
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_472 line 615
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_472 line 619
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_472 line 621
  292. def OAI.SnakyPrototype.Certificate21.checked_472 line 625
  293. def OAI.SnakyPrototype.Certificate21.height_487 line 633
  294. def OAI.SnakyPrototype.Certificate21.childrenH_487 line 634
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_487 line 635
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_487 line 636
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_487 line 638
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_487 line 642
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_487 line 644
  300. def OAI.SnakyPrototype.Certificate21.checked_487 line 648
  301. def OAI.SnakyPrototype.Certificate21.height_488_i1 line 656
  302. def OAI.SnakyPrototype.Certificate21.childrenH_488_i1 line 657
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_488_i1 line 658
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_488_i1 line 659
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_488_i1 line 661
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_488_i1 line 665
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_488_i1 line 667
  308. def OAI.SnakyPrototype.Certificate21.checked_488_i1 line 671
  309. def OAI.SnakyPrototype.Certificate21.height_488_i0 line 679
  310. def OAI.SnakyPrototype.Certificate21.childrenH_488_i0 line 680
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_488_i0 line 681
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_488_i0 line 682
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_488_i0 line 684
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_488_i0 line 688
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_488_i0 line 690
  316. def OAI.SnakyPrototype.Certificate21.checked_488_i0 line 694
  317. def OAI.SnakyPrototype.Certificate21.height_488_i2 line 702
  318. def OAI.SnakyPrototype.Certificate21.childrenH_488_i2 line 703
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_488_i2 line 704
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_488_i2 line 705
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_488_i2 line 707
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_488_i2 line 711
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_488_i2 line 713
  324. def OAI.SnakyPrototype.Certificate21.checked_488_i2 line 717
  325. def OAI.SnakyPrototype.Certificate21.height_488 line 725
  326. def OAI.SnakyPrototype.Certificate21.childrenH_488 line 726
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_488 line 727
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_488 line 728
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_488 line 730
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_488 line 734
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_488 line 736
  332. def OAI.SnakyPrototype.Certificate21.checked_488 line 740
  333. def OAI.SnakyPrototype.Certificate21.height_499_i0 line 748
  334. def OAI.SnakyPrototype.Certificate21.childrenH_499_i0 line 749
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_499_i0 line 750
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_499_i0 line 751
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_499_i0 line 753
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_499_i0 line 757
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_499_i0 line 759
  340. def OAI.SnakyPrototype.Certificate21.checked_499_i0 line 763
  341. def OAI.SnakyPrototype.Certificate21.height_499_i1 line 771
  342. def OAI.SnakyPrototype.Certificate21.childrenH_499_i1 line 772
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_499_i1 line 773
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_499_i1 line 774
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_499_i1 line 776
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_499_i1 line 780
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_499_i1 line 782
  348. def OAI.SnakyPrototype.Certificate21.checked_499_i1 line 786
  349. def OAI.SnakyPrototype.Certificate21.height_499 line 794
  350. def OAI.SnakyPrototype.Certificate21.childrenH_499 line 795
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_499 line 796
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_499 line 797
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_499 line 799
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_499 line 803
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_499 line 805
  356. def OAI.SnakyPrototype.Certificate21.checked_499 line 809
  357. def OAI.SnakyPrototype.Certificate21.height_504_i1 line 817
  358. def OAI.SnakyPrototype.Certificate21.childrenH_504_i1 line 818
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_504_i1 line 819
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_504_i1 line 820
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_504_i1 line 822
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_504_i1 line 826
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_504_i1 line 828
  364. def OAI.SnakyPrototype.Certificate21.checked_504_i1 line 832
  365. def OAI.SnakyPrototype.Certificate21.height_504_i0 line 840
  366. def OAI.SnakyPrototype.Certificate21.childrenH_504_i0 line 841
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_504_i0 line 842
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_504_i0 line 843
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_504_i0 line 845
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_504_i0 line 849
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_504_i0 line 851
  372. def OAI.SnakyPrototype.Certificate21.checked_504_i0 line 855
  373. def OAI.SnakyPrototype.Certificate21.height_504 line 863
  374. def OAI.SnakyPrototype.Certificate21.childrenH_504 line 864
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_504 line 865
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_504 line 866
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_504 line 868
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_504 line 872
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_504 line 874
  380. def OAI.SnakyPrototype.Certificate21.checked_504 line 878
  381. def OAI.SnakyPrototype.Certificate21.height_507_i0 line 886
  382. def OAI.SnakyPrototype.Certificate21.childrenH_507_i0 line 887
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_507_i0 line 888
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_507_i0 line 889
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_507_i0 line 891
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_507_i0 line 895
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_507_i0 line 897
  388. def OAI.SnakyPrototype.Certificate21.checked_507_i0 line 901
  389. def OAI.SnakyPrototype.Certificate21.height_507 line 909
  390. def OAI.SnakyPrototype.Certificate21.childrenH_507 line 910
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_507 line 911
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_507 line 912
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_507 line 914
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_507 line 918
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_507 line 920
  396. def OAI.SnakyPrototype.Certificate21.checked_507 line 924