OAI/GameTheory/SnakyTwentyOne/Cards/Height14Part02.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_598_i2 line 37
  2. def OAI.SnakyPrototype.Certificate21.envelope_598_i2 line 38
  3. def OAI.SnakyPrototype.Certificate21.childrenC_598_i2 line 39
  4. def OAI.SnakyPrototype.Certificate21.childrenD_598_i2 line 40
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i2 line 41
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i2 line 42
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i2 line 43
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i2 line 44
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i2 line 45
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i2 line 50
  11. def OAI.SnakyPrototype.Certificate21.required_598_i1 line 55
  12. def OAI.SnakyPrototype.Certificate21.envelope_598_i1 line 56
  13. def OAI.SnakyPrototype.Certificate21.childrenC_598_i1 line 57
  14. def OAI.SnakyPrototype.Certificate21.childrenD_598_i1 line 58
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i1 line 59
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i1 line 60
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i1 line 61
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i1 line 62
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i1 line 63
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i1 line 68
  21. def OAI.SnakyPrototype.Certificate21.required_598_i0 line 73
  22. def OAI.SnakyPrototype.Certificate21.envelope_598_i0 line 74
  23. def OAI.SnakyPrototype.Certificate21.childrenC_598_i0 line 75
  24. def OAI.SnakyPrototype.Certificate21.childrenD_598_i0 line 76
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i0 line 77
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i0 line 78
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i0 line 79
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i0 line 80
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i0 line 81
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i0 line 86
  31. def OAI.SnakyPrototype.Certificate21.required_598_i5 line 91
  32. def OAI.SnakyPrototype.Certificate21.envelope_598_i5 line 92
  33. def OAI.SnakyPrototype.Certificate21.childrenC_598_i5 line 93
  34. def OAI.SnakyPrototype.Certificate21.childrenD_598_i5 line 94
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i5 line 95
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i5 line 96
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i5 line 97
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i5 line 98
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i5 line 99
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i5 line 104
  41. def OAI.SnakyPrototype.Certificate21.required_598_i4 line 109
  42. def OAI.SnakyPrototype.Certificate21.envelope_598_i4 line 110
  43. def OAI.SnakyPrototype.Certificate21.childrenC_598_i4 line 111
  44. def OAI.SnakyPrototype.Certificate21.childrenD_598_i4 line 112
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i4 line 113
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i4 line 114
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i4 line 115
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i4 line 116
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i4 line 117
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i4 line 122
  51. def OAI.SnakyPrototype.Certificate21.required_598_i3 line 127
  52. def OAI.SnakyPrototype.Certificate21.envelope_598_i3 line 128
  53. def OAI.SnakyPrototype.Certificate21.childrenC_598_i3 line 129
  54. def OAI.SnakyPrototype.Certificate21.childrenD_598_i3 line 130
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i3 line 131
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i3 line 132
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i3 line 133
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i3 line 134
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i3 line 135
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i3 line 140
  61. def OAI.SnakyPrototype.Certificate21.required_598_i8 line 145
  62. def OAI.SnakyPrototype.Certificate21.envelope_598_i8 line 146
  63. def OAI.SnakyPrototype.Certificate21.childrenC_598_i8 line 147
  64. def OAI.SnakyPrototype.Certificate21.childrenD_598_i8 line 148
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i8 line 149
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i8 line 150
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i8 line 151
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i8 line 152
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i8 line 153
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i8 line 158
  71. def OAI.SnakyPrototype.Certificate21.required_598_i7 line 163
  72. def OAI.SnakyPrototype.Certificate21.envelope_598_i7 line 164
  73. def OAI.SnakyPrototype.Certificate21.childrenC_598_i7 line 165
  74. def OAI.SnakyPrototype.Certificate21.childrenD_598_i7 line 166
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i7 line 167
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i7 line 168
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i7 line 169
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i7 line 170
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i7 line 171
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i7 line 176
  81. def OAI.SnakyPrototype.Certificate21.required_598_i6 line 181
  82. def OAI.SnakyPrototype.Certificate21.envelope_598_i6 line 182
  83. def OAI.SnakyPrototype.Certificate21.childrenC_598_i6 line 183
  84. def OAI.SnakyPrototype.Certificate21.childrenD_598_i6 line 184
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_598_i6 line 185
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598_i6 line 186
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598_i6 line 187
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598_i6 line 188
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_598_i6 line 189
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_598_i6 line 194
  91. def OAI.SnakyPrototype.Certificate21.required_598 line 199
  92. def OAI.SnakyPrototype.Certificate21.envelope_598 line 200
  93. def OAI.SnakyPrototype.Certificate21.childrenC_598 line 201
  94. def OAI.SnakyPrototype.Certificate21.childrenD_598 line 202
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_598 line 203
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_598 line 204
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_598 line 205
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_598 line 206
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_598 line 207
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_598 line 217
  101. def OAI.SnakyPrototype.Certificate21.required_636_i1 line 222
  102. def OAI.SnakyPrototype.Certificate21.envelope_636_i1 line 223
  103. def OAI.SnakyPrototype.Certificate21.childrenC_636_i1 line 224
  104. def OAI.SnakyPrototype.Certificate21.childrenD_636_i1 line 225
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i1 line 226
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i1 line 227
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i1 line 228
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i1 line 229
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i1 line 230
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i1 line 236
  111. def OAI.SnakyPrototype.Certificate21.required_636_i2 line 241
  112. def OAI.SnakyPrototype.Certificate21.envelope_636_i2 line 242
  113. def OAI.SnakyPrototype.Certificate21.childrenC_636_i2 line 243
  114. def OAI.SnakyPrototype.Certificate21.childrenD_636_i2 line 244
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i2 line 245
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i2 line 246
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i2 line 247
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i2 line 248
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i2 line 249
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i2 line 256
  121. def OAI.SnakyPrototype.Certificate21.required_636_i5 line 261
  122. def OAI.SnakyPrototype.Certificate21.envelope_636_i5 line 262
  123. def OAI.SnakyPrototype.Certificate21.childrenC_636_i5 line 263
  124. def OAI.SnakyPrototype.Certificate21.childrenD_636_i5 line 264
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i5 line 265
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i5 line 266
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i5 line 267
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i5 line 268
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i5 line 269
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i5 line 275
  131. def OAI.SnakyPrototype.Certificate21.required_636_i4 line 280
  132. def OAI.SnakyPrototype.Certificate21.envelope_636_i4 line 281
  133. def OAI.SnakyPrototype.Certificate21.childrenC_636_i4 line 282
  134. def OAI.SnakyPrototype.Certificate21.childrenD_636_i4 line 283
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i4 line 284
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i4 line 285
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i4 line 286
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i4 line 287
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i4 line 288
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i4 line 293
  141. def OAI.SnakyPrototype.Certificate21.required_636_i6 line 298
  142. def OAI.SnakyPrototype.Certificate21.envelope_636_i6 line 299
  143. def OAI.SnakyPrototype.Certificate21.childrenC_636_i6 line 300
  144. def OAI.SnakyPrototype.Certificate21.childrenD_636_i6 line 301
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i6 line 302
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i6 line 303
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i6 line 304
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i6 line 305
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i6 line 306
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i6 line 312
  151. def OAI.SnakyPrototype.Certificate21.required_636_i3 line 317
  152. def OAI.SnakyPrototype.Certificate21.envelope_636_i3 line 318
  153. def OAI.SnakyPrototype.Certificate21.childrenC_636_i3 line 319
  154. def OAI.SnakyPrototype.Certificate21.childrenD_636_i3 line 320
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i3 line 321
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i3 line 322
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i3 line 323
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i3 line 324
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i3 line 325
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i3 line 333
  161. def OAI.SnakyPrototype.Certificate21.required_636_i0 line 338
  162. def OAI.SnakyPrototype.Certificate21.envelope_636_i0 line 339
  163. def OAI.SnakyPrototype.Certificate21.childrenC_636_i0 line 340
  164. def OAI.SnakyPrototype.Certificate21.childrenD_636_i0 line 341
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i0 line 342
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i0 line 343
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i0 line 344
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i0 line 345
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i0 line 346
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i0 line 358
  171. def OAI.SnakyPrototype.Certificate21.required_636_i7 line 363
  172. def OAI.SnakyPrototype.Certificate21.envelope_636_i7 line 364
  173. def OAI.SnakyPrototype.Certificate21.childrenC_636_i7 line 365
  174. def OAI.SnakyPrototype.Certificate21.childrenD_636_i7 line 366
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_636_i7 line 367
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636_i7 line 368
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636_i7 line 369
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636_i7 line 370
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_636_i7 line 371
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_636_i7 line 380
  181. def OAI.SnakyPrototype.Certificate21.required_636 line 385
  182. def OAI.SnakyPrototype.Certificate21.envelope_636 line 386
  183. def OAI.SnakyPrototype.Certificate21.childrenC_636 line 387
  184. def OAI.SnakyPrototype.Certificate21.childrenD_636 line 388
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_636 line 389
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_636 line 390
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_636 line 391
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_636 line 392
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_636 line 393
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_636 line 400
  191. def OAI.SnakyPrototype.Certificate21.required_644_i1 line 405
  192. def OAI.SnakyPrototype.Certificate21.envelope_644_i1 line 406
  193. def OAI.SnakyPrototype.Certificate21.childrenC_644_i1 line 407
  194. def OAI.SnakyPrototype.Certificate21.childrenD_644_i1 line 408
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_644_i1 line 409
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_644_i1 line 410
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_644_i1 line 411
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_644_i1 line 412
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_644_i1 line 413
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_644_i1 line 419
  201. def OAI.SnakyPrototype.Certificate21.required_644_i0 line 424
  202. def OAI.SnakyPrototype.Certificate21.envelope_644_i0 line 425
  203. def OAI.SnakyPrototype.Certificate21.childrenC_644_i0 line 426
  204. def OAI.SnakyPrototype.Certificate21.childrenD_644_i0 line 427
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_644_i0 line 428
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_644_i0 line 429
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_644_i0 line 430
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_644_i0 line 431
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_644_i0 line 432
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_644_i0 line 441
  211. def OAI.SnakyPrototype.Certificate21.required_644 line 446
  212. def OAI.SnakyPrototype.Certificate21.envelope_644 line 447
  213. def OAI.SnakyPrototype.Certificate21.childrenC_644 line 448
  214. def OAI.SnakyPrototype.Certificate21.childrenD_644 line 449
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_644 line 450
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_644 line 451
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_644 line 452
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_644 line 453
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_644 line 454
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_644 line 466
  221. def OAI.SnakyPrototype.Certificate21.height_598_i2 line 471
  222. def OAI.SnakyPrototype.Certificate21.childrenH_598_i2 line 472
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i2 line 473
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i2 line 474
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i2 line 476
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i2 line 480
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i2 line 482
  228. def OAI.SnakyPrototype.Certificate21.checked_598_i2 line 486
  229. def OAI.SnakyPrototype.Certificate21.height_598_i1 line 494
  230. def OAI.SnakyPrototype.Certificate21.childrenH_598_i1 line 495
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i1 line 496
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i1 line 497
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i1 line 499
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i1 line 503
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i1 line 505
  236. def OAI.SnakyPrototype.Certificate21.checked_598_i1 line 509
  237. def OAI.SnakyPrototype.Certificate21.height_598_i0 line 517
  238. def OAI.SnakyPrototype.Certificate21.childrenH_598_i0 line 518
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i0 line 519
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i0 line 520
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i0 line 522
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i0 line 526
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i0 line 528
  244. def OAI.SnakyPrototype.Certificate21.checked_598_i0 line 532
  245. def OAI.SnakyPrototype.Certificate21.height_598_i5 line 540
  246. def OAI.SnakyPrototype.Certificate21.childrenH_598_i5 line 541
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i5 line 542
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i5 line 543
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i5 line 545
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i5 line 549
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i5 line 551
  252. def OAI.SnakyPrototype.Certificate21.checked_598_i5 line 555
  253. def OAI.SnakyPrototype.Certificate21.height_598_i4 line 563
  254. def OAI.SnakyPrototype.Certificate21.childrenH_598_i4 line 564
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i4 line 565
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i4 line 566
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i4 line 568
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i4 line 572
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i4 line 574
  260. def OAI.SnakyPrototype.Certificate21.checked_598_i4 line 578
  261. def OAI.SnakyPrototype.Certificate21.height_598_i3 line 586
  262. def OAI.SnakyPrototype.Certificate21.childrenH_598_i3 line 587
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i3 line 588
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i3 line 589
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i3 line 591
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i3 line 595
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i3 line 597
  268. def OAI.SnakyPrototype.Certificate21.checked_598_i3 line 601
  269. def OAI.SnakyPrototype.Certificate21.height_598_i8 line 609
  270. def OAI.SnakyPrototype.Certificate21.childrenH_598_i8 line 610
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i8 line 611
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i8 line 612
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i8 line 614
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i8 line 618
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i8 line 620
  276. def OAI.SnakyPrototype.Certificate21.checked_598_i8 line 624
  277. def OAI.SnakyPrototype.Certificate21.height_598_i7 line 632
  278. def OAI.SnakyPrototype.Certificate21.childrenH_598_i7 line 633
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i7 line 634
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i7 line 635
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i7 line 637
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i7 line 641
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i7 line 643
  284. def OAI.SnakyPrototype.Certificate21.checked_598_i7 line 647
  285. def OAI.SnakyPrototype.Certificate21.height_598_i6 line 655
  286. def OAI.SnakyPrototype.Certificate21.childrenH_598_i6 line 656
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_598_i6 line 657
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_598_i6 line 658
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_598_i6 line 660
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598_i6 line 664
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598_i6 line 666
  292. def OAI.SnakyPrototype.Certificate21.checked_598_i6 line 670
  293. def OAI.SnakyPrototype.Certificate21.height_598 line 678
  294. def OAI.SnakyPrototype.Certificate21.childrenH_598 line 679
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_598 line 680
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_598 line 681
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_598 line 683
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_598 line 687
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_598 line 689
  300. def OAI.SnakyPrototype.Certificate21.checked_598 line 693
  301. def OAI.SnakyPrototype.Certificate21.height_636_i1 line 701
  302. def OAI.SnakyPrototype.Certificate21.childrenH_636_i1 line 702
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i1 line 703
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i1 line 704
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i1 line 706
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i1 line 710
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i1 line 712
  308. def OAI.SnakyPrototype.Certificate21.checked_636_i1 line 716
  309. def OAI.SnakyPrototype.Certificate21.height_636_i2 line 724
  310. def OAI.SnakyPrototype.Certificate21.childrenH_636_i2 line 725
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i2 line 726
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i2 line 727
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i2 line 729
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i2 line 733
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i2 line 735
  316. def OAI.SnakyPrototype.Certificate21.checked_636_i2 line 739
  317. def OAI.SnakyPrototype.Certificate21.height_636_i5 line 747
  318. def OAI.SnakyPrototype.Certificate21.childrenH_636_i5 line 748
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i5 line 749
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i5 line 750
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i5 line 752
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i5 line 756
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i5 line 758
  324. def OAI.SnakyPrototype.Certificate21.checked_636_i5 line 762
  325. def OAI.SnakyPrototype.Certificate21.height_636_i4 line 770
  326. def OAI.SnakyPrototype.Certificate21.childrenH_636_i4 line 771
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i4 line 772
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i4 line 773
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i4 line 775
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i4 line 779
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i4 line 781
  332. def OAI.SnakyPrototype.Certificate21.checked_636_i4 line 785
  333. def OAI.SnakyPrototype.Certificate21.height_636_i6 line 793
  334. def OAI.SnakyPrototype.Certificate21.childrenH_636_i6 line 794
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i6 line 795
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i6 line 796
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i6 line 798
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i6 line 802
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i6 line 804
  340. def OAI.SnakyPrototype.Certificate21.checked_636_i6 line 808
  341. def OAI.SnakyPrototype.Certificate21.height_636_i3 line 816
  342. def OAI.SnakyPrototype.Certificate21.childrenH_636_i3 line 817
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i3 line 818
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i3 line 819
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i3 line 821
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i3 line 825
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i3 line 827
  348. def OAI.SnakyPrototype.Certificate21.checked_636_i3 line 831
  349. def OAI.SnakyPrototype.Certificate21.height_636_i0 line 839
  350. def OAI.SnakyPrototype.Certificate21.childrenH_636_i0 line 840
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i0 line 841
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i0 line 842
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i0 line 844
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i0 line 848
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i0 line 850
  356. def OAI.SnakyPrototype.Certificate21.checked_636_i0 line 854
  357. def OAI.SnakyPrototype.Certificate21.height_636_i7 line 862
  358. def OAI.SnakyPrototype.Certificate21.childrenH_636_i7 line 863
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_636_i7 line 864
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_636_i7 line 865
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_636_i7 line 867
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636_i7 line 871
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636_i7 line 873
  364. def OAI.SnakyPrototype.Certificate21.checked_636_i7 line 877
  365. def OAI.SnakyPrototype.Certificate21.height_636 line 885
  366. def OAI.SnakyPrototype.Certificate21.childrenH_636 line 886
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_636 line 887
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_636 line 888
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_636 line 890
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_636 line 894
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_636 line 896
  372. def OAI.SnakyPrototype.Certificate21.checked_636 line 900
  373. def OAI.SnakyPrototype.Certificate21.height_644_i1 line 908
  374. def OAI.SnakyPrototype.Certificate21.childrenH_644_i1 line 909
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_644_i1 line 910
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_644_i1 line 911
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_644_i1 line 913
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_644_i1 line 917
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_644_i1 line 919
  380. def OAI.SnakyPrototype.Certificate21.checked_644_i1 line 923
  381. def OAI.SnakyPrototype.Certificate21.height_644_i0 line 931
  382. def OAI.SnakyPrototype.Certificate21.childrenH_644_i0 line 932
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_644_i0 line 933
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_644_i0 line 934
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_644_i0 line 936
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_644_i0 line 940
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_644_i0 line 942
  388. def OAI.SnakyPrototype.Certificate21.checked_644_i0 line 946
  389. def OAI.SnakyPrototype.Certificate21.height_644 line 954
  390. def OAI.SnakyPrototype.Certificate21.childrenH_644 line 955
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_644 line 956
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_644 line 957
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_644 line 959
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_644 line 963
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_644 line 965
  396. def OAI.SnakyPrototype.Certificate21.checked_644 line 969