OAI/GameTheory/SnakyTwentyOne/Cards/Height15Part02.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_670_i0 line 45
  2. def OAI.SnakyPrototype.Certificate21.envelope_670_i0 line 46
  3. def OAI.SnakyPrototype.Certificate21.childrenC_670_i0 line 47
  4. def OAI.SnakyPrototype.Certificate21.childrenD_670_i0 line 48
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i0 line 49
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i0 line 50
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i0 line 51
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i0 line 52
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i0 line 53
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i0 line 59
  11. def OAI.SnakyPrototype.Certificate21.required_670_i1 line 64
  12. def OAI.SnakyPrototype.Certificate21.envelope_670_i1 line 65
  13. def OAI.SnakyPrototype.Certificate21.childrenC_670_i1 line 66
  14. def OAI.SnakyPrototype.Certificate21.childrenD_670_i1 line 67
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i1 line 68
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i1 line 69
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i1 line 70
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i1 line 71
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i1 line 72
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i1 line 78
  21. def OAI.SnakyPrototype.Certificate21.required_670_i3 line 83
  22. def OAI.SnakyPrototype.Certificate21.envelope_670_i3 line 84
  23. def OAI.SnakyPrototype.Certificate21.childrenC_670_i3 line 85
  24. def OAI.SnakyPrototype.Certificate21.childrenD_670_i3 line 86
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i3 line 87
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i3 line 88
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i3 line 89
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i3 line 90
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i3 line 91
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i3 line 97
  31. def OAI.SnakyPrototype.Certificate21.required_670_i4 line 102
  32. def OAI.SnakyPrototype.Certificate21.envelope_670_i4 line 103
  33. def OAI.SnakyPrototype.Certificate21.childrenC_670_i4 line 104
  34. def OAI.SnakyPrototype.Certificate21.childrenD_670_i4 line 105
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i4 line 106
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i4 line 107
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i4 line 108
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i4 line 109
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i4 line 110
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i4 line 116
  41. def OAI.SnakyPrototype.Certificate21.required_670_i2 line 121
  42. def OAI.SnakyPrototype.Certificate21.envelope_670_i2 line 122
  43. def OAI.SnakyPrototype.Certificate21.childrenC_670_i2 line 123
  44. def OAI.SnakyPrototype.Certificate21.childrenD_670_i2 line 124
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i2 line 125
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i2 line 126
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i2 line 127
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i2 line 128
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i2 line 129
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i2 line 137
  51. def OAI.SnakyPrototype.Certificate21.required_670_i5 line 142
  52. def OAI.SnakyPrototype.Certificate21.envelope_670_i5 line 143
  53. def OAI.SnakyPrototype.Certificate21.childrenC_670_i5 line 144
  54. def OAI.SnakyPrototype.Certificate21.childrenD_670_i5 line 145
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i5 line 146
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i5 line 147
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i5 line 148
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i5 line 149
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i5 line 150
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i5 line 156
  61. def OAI.SnakyPrototype.Certificate21.required_670_i6 line 161
  62. def OAI.SnakyPrototype.Certificate21.envelope_670_i6 line 162
  63. def OAI.SnakyPrototype.Certificate21.childrenC_670_i6 line 163
  64. def OAI.SnakyPrototype.Certificate21.childrenD_670_i6 line 164
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i6 line 165
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i6 line 166
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i6 line 167
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i6 line 168
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i6 line 169
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i6 line 179
  71. def OAI.SnakyPrototype.Certificate21.required_670_i7 line 184
  72. def OAI.SnakyPrototype.Certificate21.envelope_670_i7 line 185
  73. def OAI.SnakyPrototype.Certificate21.childrenC_670_i7 line 186
  74. def OAI.SnakyPrototype.Certificate21.childrenD_670_i7 line 187
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i7 line 188
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i7 line 189
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i7 line 190
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i7 line 191
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i7 line 192
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i7 line 198
  81. def OAI.SnakyPrototype.Certificate21.required_670_i8 line 203
  82. def OAI.SnakyPrototype.Certificate21.envelope_670_i8 line 204
  83. def OAI.SnakyPrototype.Certificate21.childrenC_670_i8 line 205
  84. def OAI.SnakyPrototype.Certificate21.childrenD_670_i8 line 206
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i8 line 207
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i8 line 208
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i8 line 209
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i8 line 210
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i8 line 211
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i8 line 220
  91. def OAI.SnakyPrototype.Certificate21.required_670_i10 line 225
  92. def OAI.SnakyPrototype.Certificate21.envelope_670_i10 line 226
  93. def OAI.SnakyPrototype.Certificate21.childrenC_670_i10 line 227
  94. def OAI.SnakyPrototype.Certificate21.childrenD_670_i10 line 228
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i10 line 229
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i10 line 230
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i10 line 231
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i10 line 232
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i10 line 233
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i10 line 238
  101. def OAI.SnakyPrototype.Certificate21.required_670_i9 line 243
  102. def OAI.SnakyPrototype.Certificate21.envelope_670_i9 line 244
  103. def OAI.SnakyPrototype.Certificate21.childrenC_670_i9 line 245
  104. def OAI.SnakyPrototype.Certificate21.childrenD_670_i9 line 246
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_670_i9 line 247
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670_i9 line 248
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670_i9 line 249
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670_i9 line 250
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_670_i9 line 251
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_670_i9 line 259
  111. def OAI.SnakyPrototype.Certificate21.required_670 line 264
  112. def OAI.SnakyPrototype.Certificate21.envelope_670 line 265
  113. def OAI.SnakyPrototype.Certificate21.childrenC_670 line 266
  114. def OAI.SnakyPrototype.Certificate21.childrenD_670 line 267
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_670 line 268
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_670 line 269
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_670 line 270
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_670 line 271
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_670 line 272
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_670 line 287
  121. def OAI.SnakyPrototype.Certificate21.required_682_i0 line 292
  122. def OAI.SnakyPrototype.Certificate21.envelope_682_i0 line 293
  123. def OAI.SnakyPrototype.Certificate21.childrenC_682_i0 line 294
  124. def OAI.SnakyPrototype.Certificate21.childrenD_682_i0 line 295
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i0 line 296
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i0 line 297
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i0 line 298
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i0 line 299
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i0 line 300
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i0 line 307
  131. def OAI.SnakyPrototype.Certificate21.required_682_i5 line 312
  132. def OAI.SnakyPrototype.Certificate21.envelope_682_i5 line 313
  133. def OAI.SnakyPrototype.Certificate21.childrenC_682_i5 line 314
  134. def OAI.SnakyPrototype.Certificate21.childrenD_682_i5 line 315
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i5 line 316
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i5 line 317
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i5 line 318
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i5 line 319
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i5 line 320
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i5 line 326
  141. def OAI.SnakyPrototype.Certificate21.required_682_i6 line 331
  142. def OAI.SnakyPrototype.Certificate21.envelope_682_i6 line 332
  143. def OAI.SnakyPrototype.Certificate21.childrenC_682_i6 line 333
  144. def OAI.SnakyPrototype.Certificate21.childrenD_682_i6 line 334
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i6 line 335
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i6 line 336
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i6 line 337
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i6 line 338
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i6 line 339
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i6 line 344
  151. def OAI.SnakyPrototype.Certificate21.required_682_i4 line 349
  152. def OAI.SnakyPrototype.Certificate21.envelope_682_i4 line 350
  153. def OAI.SnakyPrototype.Certificate21.childrenC_682_i4 line 351
  154. def OAI.SnakyPrototype.Certificate21.childrenD_682_i4 line 352
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i4 line 353
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i4 line 354
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i4 line 355
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i4 line 356
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i4 line 357
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i4 line 364
  161. def OAI.SnakyPrototype.Certificate21.required_682_i3 line 369
  162. def OAI.SnakyPrototype.Certificate21.envelope_682_i3 line 370
  163. def OAI.SnakyPrototype.Certificate21.childrenC_682_i3 line 371
  164. def OAI.SnakyPrototype.Certificate21.childrenD_682_i3 line 372
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i3 line 373
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i3 line 374
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i3 line 375
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i3 line 376
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i3 line 377
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i3 line 385
  171. def OAI.SnakyPrototype.Certificate21.required_682_i2 line 390
  172. def OAI.SnakyPrototype.Certificate21.envelope_682_i2 line 391
  173. def OAI.SnakyPrototype.Certificate21.childrenC_682_i2 line 392
  174. def OAI.SnakyPrototype.Certificate21.childrenD_682_i2 line 393
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i2 line 394
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i2 line 395
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i2 line 396
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i2 line 397
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i2 line 398
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i2 line 405
  181. def OAI.SnakyPrototype.Certificate21.required_682_i8 line 410
  182. def OAI.SnakyPrototype.Certificate21.envelope_682_i8 line 411
  183. def OAI.SnakyPrototype.Certificate21.childrenC_682_i8 line 412
  184. def OAI.SnakyPrototype.Certificate21.childrenD_682_i8 line 413
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i8 line 414
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i8 line 415
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i8 line 416
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i8 line 417
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i8 line 418
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i8 line 425
  191. def OAI.SnakyPrototype.Certificate21.required_682_i7 line 430
  192. def OAI.SnakyPrototype.Certificate21.envelope_682_i7 line 431
  193. def OAI.SnakyPrototype.Certificate21.childrenC_682_i7 line 432
  194. def OAI.SnakyPrototype.Certificate21.childrenD_682_i7 line 433
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i7 line 434
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i7 line 435
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i7 line 436
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i7 line 437
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i7 line 438
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i7 line 447
  201. def OAI.SnakyPrototype.Certificate21.required_682_i1 line 452
  202. def OAI.SnakyPrototype.Certificate21.envelope_682_i1 line 453
  203. def OAI.SnakyPrototype.Certificate21.childrenC_682_i1 line 454
  204. def OAI.SnakyPrototype.Certificate21.childrenD_682_i1 line 455
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_682_i1 line 456
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682_i1 line 457
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682_i1 line 458
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682_i1 line 459
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_682_i1 line 460
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_682_i1 line 470
  211. def OAI.SnakyPrototype.Certificate21.required_682 line 475
  212. def OAI.SnakyPrototype.Certificate21.envelope_682 line 476
  213. def OAI.SnakyPrototype.Certificate21.childrenC_682 line 477
  214. def OAI.SnakyPrototype.Certificate21.childrenD_682 line 478
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_682 line 479
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_682 line 480
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_682 line 481
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_682 line 482
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_682 line 483
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_682 line 495
  221. def OAI.SnakyPrototype.Certificate21.height_670_i0 line 500
  222. def OAI.SnakyPrototype.Certificate21.childrenH_670_i0 line 501
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i0 line 502
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i0 line 503
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i0 line 505
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i0 line 509
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i0 line 511
  228. def OAI.SnakyPrototype.Certificate21.checked_670_i0 line 515
  229. def OAI.SnakyPrototype.Certificate21.height_670_i1 line 523
  230. def OAI.SnakyPrototype.Certificate21.childrenH_670_i1 line 524
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i1 line 525
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i1 line 526
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i1 line 528
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i1 line 532
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i1 line 534
  236. def OAI.SnakyPrototype.Certificate21.checked_670_i1 line 538
  237. def OAI.SnakyPrototype.Certificate21.height_670_i3 line 546
  238. def OAI.SnakyPrototype.Certificate21.childrenH_670_i3 line 547
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i3 line 548
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i3 line 549
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i3 line 551
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i3 line 555
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i3 line 557
  244. def OAI.SnakyPrototype.Certificate21.checked_670_i3 line 561
  245. def OAI.SnakyPrototype.Certificate21.height_670_i4 line 569
  246. def OAI.SnakyPrototype.Certificate21.childrenH_670_i4 line 570
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i4 line 571
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i4 line 572
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i4 line 574
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i4 line 578
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i4 line 580
  252. def OAI.SnakyPrototype.Certificate21.checked_670_i4 line 584
  253. def OAI.SnakyPrototype.Certificate21.height_670_i2 line 592
  254. def OAI.SnakyPrototype.Certificate21.childrenH_670_i2 line 593
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i2 line 594
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i2 line 595
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i2 line 597
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i2 line 601
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i2 line 603
  260. def OAI.SnakyPrototype.Certificate21.checked_670_i2 line 607
  261. def OAI.SnakyPrototype.Certificate21.height_670_i5 line 615
  262. def OAI.SnakyPrototype.Certificate21.childrenH_670_i5 line 616
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i5 line 617
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i5 line 618
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i5 line 620
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i5 line 624
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i5 line 626
  268. def OAI.SnakyPrototype.Certificate21.checked_670_i5 line 630
  269. def OAI.SnakyPrototype.Certificate21.height_670_i6 line 638
  270. def OAI.SnakyPrototype.Certificate21.childrenH_670_i6 line 639
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i6 line 640
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i6 line 641
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i6 line 643
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i6 line 647
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i6 line 649
  276. def OAI.SnakyPrototype.Certificate21.checked_670_i6 line 653
  277. def OAI.SnakyPrototype.Certificate21.height_670_i7 line 661
  278. def OAI.SnakyPrototype.Certificate21.childrenH_670_i7 line 662
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i7 line 663
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i7 line 664
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i7 line 666
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i7 line 670
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i7 line 672
  284. def OAI.SnakyPrototype.Certificate21.checked_670_i7 line 676
  285. def OAI.SnakyPrototype.Certificate21.height_670_i8 line 684
  286. def OAI.SnakyPrototype.Certificate21.childrenH_670_i8 line 685
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i8 line 686
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i8 line 687
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i8 line 689
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i8 line 693
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i8 line 695
  292. def OAI.SnakyPrototype.Certificate21.checked_670_i8 line 699
  293. def OAI.SnakyPrototype.Certificate21.height_670_i10 line 707
  294. def OAI.SnakyPrototype.Certificate21.childrenH_670_i10 line 708
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i10 line 709
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i10 line 710
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i10 line 712
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i10 line 716
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i10 line 718
  300. def OAI.SnakyPrototype.Certificate21.checked_670_i10 line 722
  301. def OAI.SnakyPrototype.Certificate21.height_670_i9 line 730
  302. def OAI.SnakyPrototype.Certificate21.childrenH_670_i9 line 731
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_670_i9 line 732
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_670_i9 line 733
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_670_i9 line 735
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670_i9 line 739
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670_i9 line 741
  308. def OAI.SnakyPrototype.Certificate21.checked_670_i9 line 745
  309. def OAI.SnakyPrototype.Certificate21.height_670 line 753
  310. def OAI.SnakyPrototype.Certificate21.childrenH_670 line 754
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_670 line 755
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_670 line 756
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_670 line 758
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_670 line 762
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_670 line 764
  316. def OAI.SnakyPrototype.Certificate21.checked_670 line 768
  317. def OAI.SnakyPrototype.Certificate21.height_682_i0 line 776
  318. def OAI.SnakyPrototype.Certificate21.childrenH_682_i0 line 777
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i0 line 778
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i0 line 779
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i0 line 781
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i0 line 785
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i0 line 787
  324. def OAI.SnakyPrototype.Certificate21.checked_682_i0 line 791
  325. def OAI.SnakyPrototype.Certificate21.height_682_i5 line 799
  326. def OAI.SnakyPrototype.Certificate21.childrenH_682_i5 line 800
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i5 line 801
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i5 line 802
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i5 line 804
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i5 line 808
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i5 line 810
  332. def OAI.SnakyPrototype.Certificate21.checked_682_i5 line 814
  333. def OAI.SnakyPrototype.Certificate21.height_682_i6 line 822
  334. def OAI.SnakyPrototype.Certificate21.childrenH_682_i6 line 823
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i6 line 824
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i6 line 825
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i6 line 827
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i6 line 831
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i6 line 833
  340. def OAI.SnakyPrototype.Certificate21.checked_682_i6 line 837
  341. def OAI.SnakyPrototype.Certificate21.height_682_i4 line 845
  342. def OAI.SnakyPrototype.Certificate21.childrenH_682_i4 line 846
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i4 line 847
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i4 line 848
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i4 line 850
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i4 line 854
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i4 line 856
  348. def OAI.SnakyPrototype.Certificate21.checked_682_i4 line 860
  349. def OAI.SnakyPrototype.Certificate21.height_682_i3 line 868
  350. def OAI.SnakyPrototype.Certificate21.childrenH_682_i3 line 869
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i3 line 870
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i3 line 871
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i3 line 873
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i3 line 877
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i3 line 879
  356. def OAI.SnakyPrototype.Certificate21.checked_682_i3 line 883
  357. def OAI.SnakyPrototype.Certificate21.height_682_i2 line 891
  358. def OAI.SnakyPrototype.Certificate21.childrenH_682_i2 line 892
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i2 line 893
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i2 line 894
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i2 line 896
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i2 line 900
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i2 line 902
  364. def OAI.SnakyPrototype.Certificate21.checked_682_i2 line 906
  365. def OAI.SnakyPrototype.Certificate21.height_682_i8 line 914
  366. def OAI.SnakyPrototype.Certificate21.childrenH_682_i8 line 915
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i8 line 916
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i8 line 917
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i8 line 919
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i8 line 923
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i8 line 925
  372. def OAI.SnakyPrototype.Certificate21.checked_682_i8 line 929
  373. def OAI.SnakyPrototype.Certificate21.height_682_i7 line 937
  374. def OAI.SnakyPrototype.Certificate21.childrenH_682_i7 line 938
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i7 line 939
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i7 line 940
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i7 line 942
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i7 line 946
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i7 line 948
  380. def OAI.SnakyPrototype.Certificate21.checked_682_i7 line 952
  381. def OAI.SnakyPrototype.Certificate21.height_682_i1 line 960
  382. def OAI.SnakyPrototype.Certificate21.childrenH_682_i1 line 961
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_682_i1 line 962
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_682_i1 line 963
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_682_i1 line 965
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682_i1 line 969
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682_i1 line 971
  388. def OAI.SnakyPrototype.Certificate21.checked_682_i1 line 975
  389. def OAI.SnakyPrototype.Certificate21.height_682 line 983
  390. def OAI.SnakyPrototype.Certificate21.childrenH_682 line 984
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_682 line 985
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_682 line 986
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_682 line 988
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_682 line 992
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_682 line 994
  396. def OAI.SnakyPrototype.Certificate21.checked_682 line 998