OAI/GameTheory/SnakyTwentyOne/Cards/Height14Part03.lean

GitHub source file

360 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_645_i0 line 29
  2. def OAI.SnakyPrototype.Certificate21.envelope_645_i0 line 30
  3. def OAI.SnakyPrototype.Certificate21.childrenC_645_i0 line 31
  4. def OAI.SnakyPrototype.Certificate21.childrenD_645_i0 line 32
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_645_i0 line 33
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_645_i0 line 34
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_645_i0 line 35
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_645_i0 line 36
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_645_i0 line 37
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_645_i0 line 44
  11. def OAI.SnakyPrototype.Certificate21.required_645_i1 line 49
  12. def OAI.SnakyPrototype.Certificate21.envelope_645_i1 line 50
  13. def OAI.SnakyPrototype.Certificate21.childrenC_645_i1 line 51
  14. def OAI.SnakyPrototype.Certificate21.childrenD_645_i1 line 52
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_645_i1 line 53
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_645_i1 line 54
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_645_i1 line 55
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_645_i1 line 56
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_645_i1 line 57
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_645_i1 line 66
  21. def OAI.SnakyPrototype.Certificate21.required_645 line 71
  22. def OAI.SnakyPrototype.Certificate21.envelope_645 line 72
  23. def OAI.SnakyPrototype.Certificate21.childrenC_645 line 73
  24. def OAI.SnakyPrototype.Certificate21.childrenD_645 line 74
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_645 line 75
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_645 line 76
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_645 line 77
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_645 line 78
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_645 line 79
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_645 line 92
  31. def OAI.SnakyPrototype.Certificate21.required_669_i5 line 97
  32. def OAI.SnakyPrototype.Certificate21.envelope_669_i5 line 98
  33. def OAI.SnakyPrototype.Certificate21.childrenC_669_i5 line 99
  34. def OAI.SnakyPrototype.Certificate21.childrenD_669_i5 line 100
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i5 line 101
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i5 line 102
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i5 line 103
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i5 line 104
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i5 line 105
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i5 line 110
  41. def OAI.SnakyPrototype.Certificate21.required_669_i4 line 115
  42. def OAI.SnakyPrototype.Certificate21.envelope_669_i4 line 116
  43. def OAI.SnakyPrototype.Certificate21.childrenC_669_i4 line 117
  44. def OAI.SnakyPrototype.Certificate21.childrenD_669_i4 line 118
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i4 line 119
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i4 line 120
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i4 line 121
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i4 line 122
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i4 line 123
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i4 line 128
  51. def OAI.SnakyPrototype.Certificate21.required_669_i6 line 133
  52. def OAI.SnakyPrototype.Certificate21.envelope_669_i6 line 134
  53. def OAI.SnakyPrototype.Certificate21.childrenC_669_i6 line 135
  54. def OAI.SnakyPrototype.Certificate21.childrenD_669_i6 line 136
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i6 line 137
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i6 line 138
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i6 line 139
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i6 line 140
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i6 line 141
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i6 line 146
  61. def OAI.SnakyPrototype.Certificate21.required_669_i7 line 151
  62. def OAI.SnakyPrototype.Certificate21.envelope_669_i7 line 152
  63. def OAI.SnakyPrototype.Certificate21.childrenC_669_i7 line 153
  64. def OAI.SnakyPrototype.Certificate21.childrenD_669_i7 line 154
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i7 line 155
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i7 line 156
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i7 line 157
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i7 line 158
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i7 line 159
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i7 line 164
  71. def OAI.SnakyPrototype.Certificate21.required_669_i3 line 169
  72. def OAI.SnakyPrototype.Certificate21.envelope_669_i3 line 170
  73. def OAI.SnakyPrototype.Certificate21.childrenC_669_i3 line 171
  74. def OAI.SnakyPrototype.Certificate21.childrenD_669_i3 line 172
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i3 line 173
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i3 line 174
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i3 line 175
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i3 line 176
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i3 line 177
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i3 line 184
  81. def OAI.SnakyPrototype.Certificate21.required_669_i2 line 189
  82. def OAI.SnakyPrototype.Certificate21.envelope_669_i2 line 190
  83. def OAI.SnakyPrototype.Certificate21.childrenC_669_i2 line 191
  84. def OAI.SnakyPrototype.Certificate21.childrenD_669_i2 line 192
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i2 line 193
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i2 line 194
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i2 line 195
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i2 line 196
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i2 line 197
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i2 line 202
  91. def OAI.SnakyPrototype.Certificate21.required_669_i1 line 207
  92. def OAI.SnakyPrototype.Certificate21.envelope_669_i1 line 208
  93. def OAI.SnakyPrototype.Certificate21.childrenC_669_i1 line 209
  94. def OAI.SnakyPrototype.Certificate21.childrenD_669_i1 line 210
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i1 line 211
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i1 line 212
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i1 line 213
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i1 line 214
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i1 line 215
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i1 line 220
  101. def OAI.SnakyPrototype.Certificate21.required_669_i0 line 225
  102. def OAI.SnakyPrototype.Certificate21.envelope_669_i0 line 226
  103. def OAI.SnakyPrototype.Certificate21.childrenC_669_i0 line 227
  104. def OAI.SnakyPrototype.Certificate21.childrenD_669_i0 line 228
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_669_i0 line 229
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669_i0 line 230
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669_i0 line 231
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669_i0 line 232
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_669_i0 line 233
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_669_i0 line 240
  111. def OAI.SnakyPrototype.Certificate21.required_669 line 245
  112. def OAI.SnakyPrototype.Certificate21.envelope_669 line 246
  113. def OAI.SnakyPrototype.Certificate21.childrenC_669 line 247
  114. def OAI.SnakyPrototype.Certificate21.childrenD_669 line 248
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_669 line 249
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_669 line 250
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_669 line 251
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_669 line 252
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_669 line 253
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_669 line 260
  121. def OAI.SnakyPrototype.Certificate21.required_693_i1 line 265
  122. def OAI.SnakyPrototype.Certificate21.envelope_693_i1 line 266
  123. def OAI.SnakyPrototype.Certificate21.childrenC_693_i1 line 267
  124. def OAI.SnakyPrototype.Certificate21.childrenD_693_i1 line 268
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i1 line 269
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i1 line 270
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i1 line 271
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i1 line 272
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i1 line 273
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i1 line 278
  131. def OAI.SnakyPrototype.Certificate21.required_693_i2 line 283
  132. def OAI.SnakyPrototype.Certificate21.envelope_693_i2 line 284
  133. def OAI.SnakyPrototype.Certificate21.childrenC_693_i2 line 285
  134. def OAI.SnakyPrototype.Certificate21.childrenD_693_i2 line 286
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i2 line 287
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i2 line 288
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i2 line 289
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i2 line 290
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i2 line 291
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i2 line 297
  141. def OAI.SnakyPrototype.Certificate21.required_693_i4 line 302
  142. def OAI.SnakyPrototype.Certificate21.envelope_693_i4 line 303
  143. def OAI.SnakyPrototype.Certificate21.childrenC_693_i4 line 304
  144. def OAI.SnakyPrototype.Certificate21.childrenD_693_i4 line 305
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i4 line 306
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i4 line 307
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i4 line 308
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i4 line 309
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i4 line 310
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i4 line 315
  151. def OAI.SnakyPrototype.Certificate21.required_693_i3 line 320
  152. def OAI.SnakyPrototype.Certificate21.envelope_693_i3 line 321
  153. def OAI.SnakyPrototype.Certificate21.childrenC_693_i3 line 322
  154. def OAI.SnakyPrototype.Certificate21.childrenD_693_i3 line 323
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i3 line 324
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i3 line 325
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i3 line 326
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i3 line 327
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i3 line 328
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i3 line 335
  161. def OAI.SnakyPrototype.Certificate21.required_693_i6 line 340
  162. def OAI.SnakyPrototype.Certificate21.envelope_693_i6 line 341
  163. def OAI.SnakyPrototype.Certificate21.childrenC_693_i6 line 342
  164. def OAI.SnakyPrototype.Certificate21.childrenD_693_i6 line 343
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i6 line 344
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i6 line 345
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i6 line 346
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i6 line 347
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i6 line 348
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i6 line 354
  171. def OAI.SnakyPrototype.Certificate21.required_693_i5 line 359
  172. def OAI.SnakyPrototype.Certificate21.envelope_693_i5 line 360
  173. def OAI.SnakyPrototype.Certificate21.childrenC_693_i5 line 361
  174. def OAI.SnakyPrototype.Certificate21.childrenD_693_i5 line 362
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i5 line 363
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i5 line 364
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i5 line 365
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i5 line 366
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i5 line 367
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i5 line 373
  181. def OAI.SnakyPrototype.Certificate21.required_693_i0 line 378
  182. def OAI.SnakyPrototype.Certificate21.envelope_693_i0 line 379
  183. def OAI.SnakyPrototype.Certificate21.childrenC_693_i0 line 380
  184. def OAI.SnakyPrototype.Certificate21.childrenD_693_i0 line 381
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_693_i0 line 382
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693_i0 line 383
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693_i0 line 384
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693_i0 line 385
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_693_i0 line 386
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_693_i0 line 394
  191. def OAI.SnakyPrototype.Certificate21.required_693 line 399
  192. def OAI.SnakyPrototype.Certificate21.envelope_693 line 400
  193. def OAI.SnakyPrototype.Certificate21.childrenC_693 line 401
  194. def OAI.SnakyPrototype.Certificate21.childrenD_693 line 402
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_693 line 403
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_693 line 404
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_693 line 405
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_693 line 406
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_693 line 407
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_693 line 414
  201. def OAI.SnakyPrototype.Certificate21.height_645_i0 line 419
  202. def OAI.SnakyPrototype.Certificate21.childrenH_645_i0 line 420
  203. theorem OAI.SnakyPrototype.Certificate21.height_exact_645_i0 line 421
  204. theorem OAI.SnakyPrototype.Certificate21.required_origin_645_i0 line 422
  205. theorem OAI.SnakyPrototype.Certificate21.required_exact_645_i0 line 424
  206. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_645_i0 line 428
  207. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_645_i0 line 430
  208. def OAI.SnakyPrototype.Certificate21.checked_645_i0 line 434
  209. def OAI.SnakyPrototype.Certificate21.height_645_i1 line 442
  210. def OAI.SnakyPrototype.Certificate21.childrenH_645_i1 line 443
  211. theorem OAI.SnakyPrototype.Certificate21.height_exact_645_i1 line 444
  212. theorem OAI.SnakyPrototype.Certificate21.required_origin_645_i1 line 445
  213. theorem OAI.SnakyPrototype.Certificate21.required_exact_645_i1 line 447
  214. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_645_i1 line 451
  215. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_645_i1 line 453
  216. def OAI.SnakyPrototype.Certificate21.checked_645_i1 line 457
  217. def OAI.SnakyPrototype.Certificate21.height_645 line 465
  218. def OAI.SnakyPrototype.Certificate21.childrenH_645 line 466
  219. theorem OAI.SnakyPrototype.Certificate21.height_exact_645 line 467
  220. theorem OAI.SnakyPrototype.Certificate21.required_origin_645 line 468
  221. theorem OAI.SnakyPrototype.Certificate21.required_exact_645 line 470
  222. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_645 line 474
  223. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_645 line 476
  224. def OAI.SnakyPrototype.Certificate21.checked_645 line 480
  225. def OAI.SnakyPrototype.Certificate21.height_669_i5 line 488
  226. def OAI.SnakyPrototype.Certificate21.childrenH_669_i5 line 489
  227. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i5 line 490
  228. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i5 line 491
  229. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i5 line 493
  230. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i5 line 497
  231. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i5 line 499
  232. def OAI.SnakyPrototype.Certificate21.checked_669_i5 line 503
  233. def OAI.SnakyPrototype.Certificate21.height_669_i4 line 511
  234. def OAI.SnakyPrototype.Certificate21.childrenH_669_i4 line 512
  235. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i4 line 513
  236. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i4 line 514
  237. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i4 line 516
  238. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i4 line 520
  239. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i4 line 522
  240. def OAI.SnakyPrototype.Certificate21.checked_669_i4 line 526
  241. def OAI.SnakyPrototype.Certificate21.height_669_i6 line 534
  242. def OAI.SnakyPrototype.Certificate21.childrenH_669_i6 line 535
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i6 line 536
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i6 line 537
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i6 line 539
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i6 line 543
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i6 line 545
  248. def OAI.SnakyPrototype.Certificate21.checked_669_i6 line 549
  249. def OAI.SnakyPrototype.Certificate21.height_669_i7 line 557
  250. def OAI.SnakyPrototype.Certificate21.childrenH_669_i7 line 558
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i7 line 559
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i7 line 560
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i7 line 562
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i7 line 566
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i7 line 568
  256. def OAI.SnakyPrototype.Certificate21.checked_669_i7 line 572
  257. def OAI.SnakyPrototype.Certificate21.height_669_i3 line 580
  258. def OAI.SnakyPrototype.Certificate21.childrenH_669_i3 line 581
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i3 line 582
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i3 line 583
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i3 line 585
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i3 line 589
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i3 line 591
  264. def OAI.SnakyPrototype.Certificate21.checked_669_i3 line 595
  265. def OAI.SnakyPrototype.Certificate21.height_669_i2 line 603
  266. def OAI.SnakyPrototype.Certificate21.childrenH_669_i2 line 604
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i2 line 605
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i2 line 606
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i2 line 608
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i2 line 612
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i2 line 614
  272. def OAI.SnakyPrototype.Certificate21.checked_669_i2 line 618
  273. def OAI.SnakyPrototype.Certificate21.height_669_i1 line 626
  274. def OAI.SnakyPrototype.Certificate21.childrenH_669_i1 line 627
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i1 line 628
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i1 line 629
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i1 line 631
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i1 line 635
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i1 line 637
  280. def OAI.SnakyPrototype.Certificate21.checked_669_i1 line 641
  281. def OAI.SnakyPrototype.Certificate21.height_669_i0 line 649
  282. def OAI.SnakyPrototype.Certificate21.childrenH_669_i0 line 650
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_669_i0 line 651
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_669_i0 line 652
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_669_i0 line 654
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669_i0 line 658
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669_i0 line 660
  288. def OAI.SnakyPrototype.Certificate21.checked_669_i0 line 664
  289. def OAI.SnakyPrototype.Certificate21.height_669 line 672
  290. def OAI.SnakyPrototype.Certificate21.childrenH_669 line 673
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_669 line 674
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_669 line 675
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_669 line 677
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_669 line 681
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_669 line 683
  296. def OAI.SnakyPrototype.Certificate21.checked_669 line 687
  297. def OAI.SnakyPrototype.Certificate21.height_693_i1 line 695
  298. def OAI.SnakyPrototype.Certificate21.childrenH_693_i1 line 696
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i1 line 697
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i1 line 698
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i1 line 700
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i1 line 704
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i1 line 706
  304. def OAI.SnakyPrototype.Certificate21.checked_693_i1 line 710
  305. def OAI.SnakyPrototype.Certificate21.height_693_i2 line 718
  306. def OAI.SnakyPrototype.Certificate21.childrenH_693_i2 line 719
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i2 line 720
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i2 line 721
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i2 line 723
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i2 line 727
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i2 line 729
  312. def OAI.SnakyPrototype.Certificate21.checked_693_i2 line 733
  313. def OAI.SnakyPrototype.Certificate21.height_693_i4 line 741
  314. def OAI.SnakyPrototype.Certificate21.childrenH_693_i4 line 742
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i4 line 743
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i4 line 744
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i4 line 746
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i4 line 750
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i4 line 752
  320. def OAI.SnakyPrototype.Certificate21.checked_693_i4 line 756
  321. def OAI.SnakyPrototype.Certificate21.height_693_i3 line 764
  322. def OAI.SnakyPrototype.Certificate21.childrenH_693_i3 line 765
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i3 line 766
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i3 line 767
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i3 line 769
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i3 line 773
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i3 line 775
  328. def OAI.SnakyPrototype.Certificate21.checked_693_i3 line 779
  329. def OAI.SnakyPrototype.Certificate21.height_693_i6 line 787
  330. def OAI.SnakyPrototype.Certificate21.childrenH_693_i6 line 788
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i6 line 789
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i6 line 790
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i6 line 792
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i6 line 796
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i6 line 798
  336. def OAI.SnakyPrototype.Certificate21.checked_693_i6 line 802
  337. def OAI.SnakyPrototype.Certificate21.height_693_i5 line 810
  338. def OAI.SnakyPrototype.Certificate21.childrenH_693_i5 line 811
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i5 line 812
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i5 line 813
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i5 line 815
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i5 line 819
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i5 line 821
  344. def OAI.SnakyPrototype.Certificate21.checked_693_i5 line 825
  345. def OAI.SnakyPrototype.Certificate21.height_693_i0 line 833
  346. def OAI.SnakyPrototype.Certificate21.childrenH_693_i0 line 834
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_693_i0 line 835
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_693_i0 line 836
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_693_i0 line 838
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693_i0 line 842
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693_i0 line 844
  352. def OAI.SnakyPrototype.Certificate21.checked_693_i0 line 848
  353. def OAI.SnakyPrototype.Certificate21.height_693 line 856
  354. def OAI.SnakyPrototype.Certificate21.childrenH_693 line 857
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_693 line 858
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_693 line 859
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_693 line 861
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_693 line 865
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_693 line 867
  360. def OAI.SnakyPrototype.Certificate21.checked_693 line 871