OAI/GameTheory/SnakyTwentyOne/Cards/Height09Part06.lean

GitHub source file

342 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_595_i6 line 19
  2. def OAI.SnakyPrototype.Certificate21.envelope_595_i6 line 20
  3. def OAI.SnakyPrototype.Certificate21.childrenC_595_i6 line 21
  4. def OAI.SnakyPrototype.Certificate21.childrenD_595_i6 line 22
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i6 line 23
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i6 line 24
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i6 line 25
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i6 line 26
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i6 line 27
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i6 line 32
  11. def OAI.SnakyPrototype.Certificate21.required_595_i5 line 37
  12. def OAI.SnakyPrototype.Certificate21.envelope_595_i5 line 38
  13. def OAI.SnakyPrototype.Certificate21.childrenC_595_i5 line 39
  14. def OAI.SnakyPrototype.Certificate21.childrenD_595_i5 line 40
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i5 line 41
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i5 line 42
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i5 line 43
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i5 line 44
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i5 line 45
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i5 line 50
  21. def OAI.SnakyPrototype.Certificate21.required_595_i4 line 55
  22. def OAI.SnakyPrototype.Certificate21.envelope_595_i4 line 56
  23. def OAI.SnakyPrototype.Certificate21.childrenC_595_i4 line 57
  24. def OAI.SnakyPrototype.Certificate21.childrenD_595_i4 line 58
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i4 line 59
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i4 line 60
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i4 line 61
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i4 line 62
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i4 line 63
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i4 line 68
  31. def OAI.SnakyPrototype.Certificate21.required_595_i3 line 73
  32. def OAI.SnakyPrototype.Certificate21.envelope_595_i3 line 74
  33. def OAI.SnakyPrototype.Certificate21.childrenC_595_i3 line 75
  34. def OAI.SnakyPrototype.Certificate21.childrenD_595_i3 line 76
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i3 line 77
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i3 line 78
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i3 line 79
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i3 line 80
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i3 line 81
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i3 line 86
  41. def OAI.SnakyPrototype.Certificate21.required_595_i7 line 91
  42. def OAI.SnakyPrototype.Certificate21.envelope_595_i7 line 92
  43. def OAI.SnakyPrototype.Certificate21.childrenC_595_i7 line 93
  44. def OAI.SnakyPrototype.Certificate21.childrenD_595_i7 line 94
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i7 line 95
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i7 line 96
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i7 line 97
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i7 line 98
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i7 line 99
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i7 line 104
  51. def OAI.SnakyPrototype.Certificate21.required_595_i9 line 109
  52. def OAI.SnakyPrototype.Certificate21.envelope_595_i9 line 110
  53. def OAI.SnakyPrototype.Certificate21.childrenC_595_i9 line 111
  54. def OAI.SnakyPrototype.Certificate21.childrenD_595_i9 line 112
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i9 line 113
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i9 line 114
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i9 line 115
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i9 line 116
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i9 line 117
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i9 line 122
  61. def OAI.SnakyPrototype.Certificate21.required_595_i8 line 127
  62. def OAI.SnakyPrototype.Certificate21.envelope_595_i8 line 128
  63. def OAI.SnakyPrototype.Certificate21.childrenC_595_i8 line 129
  64. def OAI.SnakyPrototype.Certificate21.childrenD_595_i8 line 130
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i8 line 131
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i8 line 132
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i8 line 133
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i8 line 134
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i8 line 135
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i8 line 140
  71. def OAI.SnakyPrototype.Certificate21.required_595_i10 line 145
  72. def OAI.SnakyPrototype.Certificate21.envelope_595_i10 line 146
  73. def OAI.SnakyPrototype.Certificate21.childrenC_595_i10 line 147
  74. def OAI.SnakyPrototype.Certificate21.childrenD_595_i10 line 148
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i10 line 149
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i10 line 150
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i10 line 151
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i10 line 152
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i10 line 153
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i10 line 158
  81. def OAI.SnakyPrototype.Certificate21.required_595_i2 line 163
  82. def OAI.SnakyPrototype.Certificate21.envelope_595_i2 line 164
  83. def OAI.SnakyPrototype.Certificate21.childrenC_595_i2 line 165
  84. def OAI.SnakyPrototype.Certificate21.childrenD_595_i2 line 166
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i2 line 167
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i2 line 168
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i2 line 169
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i2 line 170
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i2 line 171
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i2 line 179
  91. def OAI.SnakyPrototype.Certificate21.required_595_i1 line 184
  92. def OAI.SnakyPrototype.Certificate21.envelope_595_i1 line 185
  93. def OAI.SnakyPrototype.Certificate21.childrenC_595_i1 line 186
  94. def OAI.SnakyPrototype.Certificate21.childrenD_595_i1 line 187
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i1 line 188
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i1 line 189
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i1 line 190
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i1 line 191
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i1 line 192
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i1 line 197
  101. def OAI.SnakyPrototype.Certificate21.required_595_i0 line 202
  102. def OAI.SnakyPrototype.Certificate21.envelope_595_i0 line 203
  103. def OAI.SnakyPrototype.Certificate21.childrenC_595_i0 line 204
  104. def OAI.SnakyPrototype.Certificate21.childrenD_595_i0 line 205
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_595_i0 line 206
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595_i0 line 207
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595_i0 line 208
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595_i0 line 209
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_595_i0 line 210
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_595_i0 line 215
  111. def OAI.SnakyPrototype.Certificate21.required_595 line 220
  112. def OAI.SnakyPrototype.Certificate21.envelope_595 line 221
  113. def OAI.SnakyPrototype.Certificate21.childrenC_595 line 222
  114. def OAI.SnakyPrototype.Certificate21.childrenD_595 line 223
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_595 line 224
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_595 line 225
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_595 line 226
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_595 line 227
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_595 line 228
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_595 line 233
  121. def OAI.SnakyPrototype.Certificate21.required_614_i1 line 238
  122. def OAI.SnakyPrototype.Certificate21.envelope_614_i1 line 239
  123. def OAI.SnakyPrototype.Certificate21.childrenC_614_i1 line 240
  124. def OAI.SnakyPrototype.Certificate21.childrenD_614_i1 line 241
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_614_i1 line 242
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614_i1 line 243
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614_i1 line 244
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614_i1 line 245
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_614_i1 line 246
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_614_i1 line 251
  131. def OAI.SnakyPrototype.Certificate21.required_614_i2 line 256
  132. def OAI.SnakyPrototype.Certificate21.envelope_614_i2 line 257
  133. def OAI.SnakyPrototype.Certificate21.childrenC_614_i2 line 258
  134. def OAI.SnakyPrototype.Certificate21.childrenD_614_i2 line 259
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_614_i2 line 260
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614_i2 line 261
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614_i2 line 262
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614_i2 line 263
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_614_i2 line 264
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_614_i2 line 269
  141. def OAI.SnakyPrototype.Certificate21.required_614_i4 line 274
  142. def OAI.SnakyPrototype.Certificate21.envelope_614_i4 line 275
  143. def OAI.SnakyPrototype.Certificate21.childrenC_614_i4 line 276
  144. def OAI.SnakyPrototype.Certificate21.childrenD_614_i4 line 277
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_614_i4 line 278
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614_i4 line 279
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614_i4 line 280
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614_i4 line 281
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_614_i4 line 282
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_614_i4 line 287
  151. def OAI.SnakyPrototype.Certificate21.required_614_i3 line 292
  152. def OAI.SnakyPrototype.Certificate21.envelope_614_i3 line 293
  153. def OAI.SnakyPrototype.Certificate21.childrenC_614_i3 line 294
  154. def OAI.SnakyPrototype.Certificate21.childrenD_614_i3 line 295
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_614_i3 line 296
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614_i3 line 297
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614_i3 line 298
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614_i3 line 299
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_614_i3 line 300
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_614_i3 line 305
  161. def OAI.SnakyPrototype.Certificate21.required_614_i5 line 310
  162. def OAI.SnakyPrototype.Certificate21.envelope_614_i5 line 311
  163. def OAI.SnakyPrototype.Certificate21.childrenC_614_i5 line 312
  164. def OAI.SnakyPrototype.Certificate21.childrenD_614_i5 line 313
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_614_i5 line 314
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614_i5 line 315
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614_i5 line 316
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614_i5 line 317
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_614_i5 line 318
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_614_i5 line 323
  171. def OAI.SnakyPrototype.Certificate21.required_614_i0 line 328
  172. def OAI.SnakyPrototype.Certificate21.envelope_614_i0 line 329
  173. def OAI.SnakyPrototype.Certificate21.childrenC_614_i0 line 330
  174. def OAI.SnakyPrototype.Certificate21.childrenD_614_i0 line 331
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_614_i0 line 332
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614_i0 line 333
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614_i0 line 334
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614_i0 line 335
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_614_i0 line 336
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_614_i0 line 345
  181. def OAI.SnakyPrototype.Certificate21.required_614 line 350
  182. def OAI.SnakyPrototype.Certificate21.envelope_614 line 351
  183. def OAI.SnakyPrototype.Certificate21.childrenC_614 line 352
  184. def OAI.SnakyPrototype.Certificate21.childrenD_614 line 353
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_614 line 354
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_614 line 355
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_614 line 356
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_614 line 357
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_614 line 358
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_614 line 364
  191. def OAI.SnakyPrototype.Certificate21.height_595_i6 line 369
  192. def OAI.SnakyPrototype.Certificate21.childrenH_595_i6 line 370
  193. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i6 line 371
  194. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i6 line 372
  195. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i6 line 374
  196. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i6 line 378
  197. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i6 line 380
  198. def OAI.SnakyPrototype.Certificate21.checked_595_i6 line 384
  199. def OAI.SnakyPrototype.Certificate21.height_595_i5 line 392
  200. def OAI.SnakyPrototype.Certificate21.childrenH_595_i5 line 393
  201. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i5 line 394
  202. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i5 line 395
  203. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i5 line 397
  204. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i5 line 401
  205. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i5 line 403
  206. def OAI.SnakyPrototype.Certificate21.checked_595_i5 line 407
  207. def OAI.SnakyPrototype.Certificate21.height_595_i4 line 415
  208. def OAI.SnakyPrototype.Certificate21.childrenH_595_i4 line 416
  209. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i4 line 417
  210. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i4 line 418
  211. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i4 line 420
  212. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i4 line 424
  213. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i4 line 426
  214. def OAI.SnakyPrototype.Certificate21.checked_595_i4 line 430
  215. def OAI.SnakyPrototype.Certificate21.height_595_i3 line 438
  216. def OAI.SnakyPrototype.Certificate21.childrenH_595_i3 line 439
  217. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i3 line 440
  218. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i3 line 441
  219. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i3 line 443
  220. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i3 line 447
  221. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i3 line 449
  222. def OAI.SnakyPrototype.Certificate21.checked_595_i3 line 453
  223. def OAI.SnakyPrototype.Certificate21.height_595_i7 line 461
  224. def OAI.SnakyPrototype.Certificate21.childrenH_595_i7 line 462
  225. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i7 line 463
  226. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i7 line 464
  227. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i7 line 466
  228. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i7 line 470
  229. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i7 line 472
  230. def OAI.SnakyPrototype.Certificate21.checked_595_i7 line 476
  231. def OAI.SnakyPrototype.Certificate21.height_595_i9 line 484
  232. def OAI.SnakyPrototype.Certificate21.childrenH_595_i9 line 485
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i9 line 486
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i9 line 487
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i9 line 489
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i9 line 493
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i9 line 495
  238. def OAI.SnakyPrototype.Certificate21.checked_595_i9 line 499
  239. def OAI.SnakyPrototype.Certificate21.height_595_i8 line 507
  240. def OAI.SnakyPrototype.Certificate21.childrenH_595_i8 line 508
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i8 line 509
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i8 line 510
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i8 line 512
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i8 line 516
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i8 line 518
  246. def OAI.SnakyPrototype.Certificate21.checked_595_i8 line 522
  247. def OAI.SnakyPrototype.Certificate21.height_595_i10 line 530
  248. def OAI.SnakyPrototype.Certificate21.childrenH_595_i10 line 531
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i10 line 532
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i10 line 533
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i10 line 535
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i10 line 539
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i10 line 541
  254. def OAI.SnakyPrototype.Certificate21.checked_595_i10 line 545
  255. def OAI.SnakyPrototype.Certificate21.height_595_i2 line 553
  256. def OAI.SnakyPrototype.Certificate21.childrenH_595_i2 line 554
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i2 line 555
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i2 line 556
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i2 line 558
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i2 line 562
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i2 line 564
  262. def OAI.SnakyPrototype.Certificate21.checked_595_i2 line 568
  263. def OAI.SnakyPrototype.Certificate21.height_595_i1 line 576
  264. def OAI.SnakyPrototype.Certificate21.childrenH_595_i1 line 577
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i1 line 578
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i1 line 579
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i1 line 581
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i1 line 585
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i1 line 587
  270. def OAI.SnakyPrototype.Certificate21.checked_595_i1 line 591
  271. def OAI.SnakyPrototype.Certificate21.height_595_i0 line 599
  272. def OAI.SnakyPrototype.Certificate21.childrenH_595_i0 line 600
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_595_i0 line 601
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_595_i0 line 602
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_595_i0 line 604
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595_i0 line 608
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595_i0 line 610
  278. def OAI.SnakyPrototype.Certificate21.checked_595_i0 line 614
  279. def OAI.SnakyPrototype.Certificate21.height_595 line 622
  280. def OAI.SnakyPrototype.Certificate21.childrenH_595 line 623
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_595 line 624
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_595 line 625
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_595 line 627
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_595 line 631
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_595 line 633
  286. def OAI.SnakyPrototype.Certificate21.checked_595 line 637
  287. def OAI.SnakyPrototype.Certificate21.height_614_i1 line 645
  288. def OAI.SnakyPrototype.Certificate21.childrenH_614_i1 line 646
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_614_i1 line 647
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_614_i1 line 648
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_614_i1 line 650
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614_i1 line 654
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614_i1 line 656
  294. def OAI.SnakyPrototype.Certificate21.checked_614_i1 line 660
  295. def OAI.SnakyPrototype.Certificate21.height_614_i2 line 668
  296. def OAI.SnakyPrototype.Certificate21.childrenH_614_i2 line 669
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_614_i2 line 670
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_614_i2 line 671
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_614_i2 line 673
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614_i2 line 677
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614_i2 line 679
  302. def OAI.SnakyPrototype.Certificate21.checked_614_i2 line 683
  303. def OAI.SnakyPrototype.Certificate21.height_614_i4 line 691
  304. def OAI.SnakyPrototype.Certificate21.childrenH_614_i4 line 692
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_614_i4 line 693
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_614_i4 line 694
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_614_i4 line 696
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614_i4 line 700
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614_i4 line 702
  310. def OAI.SnakyPrototype.Certificate21.checked_614_i4 line 706
  311. def OAI.SnakyPrototype.Certificate21.height_614_i3 line 714
  312. def OAI.SnakyPrototype.Certificate21.childrenH_614_i3 line 715
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_614_i3 line 716
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_614_i3 line 717
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_614_i3 line 719
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614_i3 line 723
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614_i3 line 725
  318. def OAI.SnakyPrototype.Certificate21.checked_614_i3 line 729
  319. def OAI.SnakyPrototype.Certificate21.height_614_i5 line 737
  320. def OAI.SnakyPrototype.Certificate21.childrenH_614_i5 line 738
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_614_i5 line 739
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_614_i5 line 740
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_614_i5 line 742
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614_i5 line 746
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614_i5 line 748
  326. def OAI.SnakyPrototype.Certificate21.checked_614_i5 line 752
  327. def OAI.SnakyPrototype.Certificate21.height_614_i0 line 760
  328. def OAI.SnakyPrototype.Certificate21.childrenH_614_i0 line 761
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_614_i0 line 762
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_614_i0 line 763
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_614_i0 line 765
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614_i0 line 769
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614_i0 line 771
  334. def OAI.SnakyPrototype.Certificate21.checked_614_i0 line 775
  335. def OAI.SnakyPrototype.Certificate21.height_614 line 783
  336. def OAI.SnakyPrototype.Certificate21.childrenH_614 line 784
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_614 line 785
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_614 line 786
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_614 line 788
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_614 line 792
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_614 line 794
  342. def OAI.SnakyPrototype.Certificate21.checked_614 line 798