OAI/GameTheory/SnakyTwentyOne/Cards/Height06Part03.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_336_i1 line 21
  2. def OAI.SnakyPrototype.Certificate21.envelope_336_i1 line 22
  3. def OAI.SnakyPrototype.Certificate21.childrenC_336_i1 line 23
  4. def OAI.SnakyPrototype.Certificate21.childrenD_336_i1 line 24
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_336_i1 line 25
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_336_i1 line 26
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_336_i1 line 27
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_336_i1 line 28
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_336_i1 line 29
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_336_i1 line 34
  11. def OAI.SnakyPrototype.Certificate21.required_336_i0 line 39
  12. def OAI.SnakyPrototype.Certificate21.envelope_336_i0 line 40
  13. def OAI.SnakyPrototype.Certificate21.childrenC_336_i0 line 41
  14. def OAI.SnakyPrototype.Certificate21.childrenD_336_i0 line 42
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_336_i0 line 43
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_336_i0 line 44
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_336_i0 line 45
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_336_i0 line 46
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_336_i0 line 47
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_336_i0 line 52
  21. def OAI.SnakyPrototype.Certificate21.required_336 line 57
  22. def OAI.SnakyPrototype.Certificate21.envelope_336 line 58
  23. def OAI.SnakyPrototype.Certificate21.childrenC_336 line 59
  24. def OAI.SnakyPrototype.Certificate21.childrenD_336 line 60
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_336 line 61
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_336 line 62
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_336 line 63
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_336 line 64
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_336 line 65
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_336 line 71
  31. def OAI.SnakyPrototype.Certificate21.required_340_i0 line 76
  32. def OAI.SnakyPrototype.Certificate21.envelope_340_i0 line 77
  33. def OAI.SnakyPrototype.Certificate21.childrenC_340_i0 line 78
  34. def OAI.SnakyPrototype.Certificate21.childrenD_340_i0 line 79
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_340_i0 line 80
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_340_i0 line 81
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_340_i0 line 82
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_340_i0 line 83
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_340_i0 line 84
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_340_i0 line 89
  41. def OAI.SnakyPrototype.Certificate21.required_340 line 94
  42. def OAI.SnakyPrototype.Certificate21.envelope_340 line 95
  43. def OAI.SnakyPrototype.Certificate21.childrenC_340 line 96
  44. def OAI.SnakyPrototype.Certificate21.childrenD_340 line 97
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_340 line 98
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_340 line 99
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_340 line 100
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_340 line 101
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_340 line 102
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_340 line 108
  51. def OAI.SnakyPrototype.Certificate21.required_343 line 113
  52. def OAI.SnakyPrototype.Certificate21.envelope_343 line 114
  53. def OAI.SnakyPrototype.Certificate21.childrenC_343 line 115
  54. def OAI.SnakyPrototype.Certificate21.childrenD_343 line 116
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_343 line 117
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_343 line 118
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_343 line 119
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_343 line 120
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_343 line 121
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_343 line 126
  61. def OAI.SnakyPrototype.Certificate21.required_346 line 131
  62. def OAI.SnakyPrototype.Certificate21.envelope_346 line 132
  63. def OAI.SnakyPrototype.Certificate21.childrenC_346 line 133
  64. def OAI.SnakyPrototype.Certificate21.childrenD_346 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_346 line 135
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_346 line 136
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_346 line 137
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_346 line 138
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_346 line 139
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_346 line 144
  71. def OAI.SnakyPrototype.Certificate21.required_348_i0 line 149
  72. def OAI.SnakyPrototype.Certificate21.envelope_348_i0 line 150
  73. def OAI.SnakyPrototype.Certificate21.childrenC_348_i0 line 151
  74. def OAI.SnakyPrototype.Certificate21.childrenD_348_i0 line 152
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_348_i0 line 153
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_348_i0 line 154
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_348_i0 line 155
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_348_i0 line 156
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_348_i0 line 157
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_348_i0 line 162
  81. def OAI.SnakyPrototype.Certificate21.required_348 line 167
  82. def OAI.SnakyPrototype.Certificate21.envelope_348 line 168
  83. def OAI.SnakyPrototype.Certificate21.childrenC_348 line 169
  84. def OAI.SnakyPrototype.Certificate21.childrenD_348 line 170
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_348 line 171
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_348 line 172
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_348 line 173
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_348 line 174
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_348 line 175
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_348 line 180
  91. def OAI.SnakyPrototype.Certificate21.required_349_i0 line 185
  92. def OAI.SnakyPrototype.Certificate21.envelope_349_i0 line 186
  93. def OAI.SnakyPrototype.Certificate21.childrenC_349_i0 line 187
  94. def OAI.SnakyPrototype.Certificate21.childrenD_349_i0 line 188
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_349_i0 line 189
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_349_i0 line 190
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_349_i0 line 191
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_349_i0 line 192
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_349_i0 line 193
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_349_i0 line 198
  101. def OAI.SnakyPrototype.Certificate21.required_349 line 203
  102. def OAI.SnakyPrototype.Certificate21.envelope_349 line 204
  103. def OAI.SnakyPrototype.Certificate21.childrenC_349 line 205
  104. def OAI.SnakyPrototype.Certificate21.childrenD_349 line 206
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_349 line 207
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_349 line 208
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_349 line 209
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_349 line 210
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_349 line 211
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_349 line 218
  111. def OAI.SnakyPrototype.Certificate21.required_358 line 223
  112. def OAI.SnakyPrototype.Certificate21.envelope_358 line 224
  113. def OAI.SnakyPrototype.Certificate21.childrenC_358 line 225
  114. def OAI.SnakyPrototype.Certificate21.childrenD_358 line 226
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_358 line 227
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_358 line 228
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_358 line 229
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_358 line 230
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_358 line 231
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_358 line 236
  121. def OAI.SnakyPrototype.Certificate21.required_360_i0 line 241
  122. def OAI.SnakyPrototype.Certificate21.envelope_360_i0 line 242
  123. def OAI.SnakyPrototype.Certificate21.childrenC_360_i0 line 243
  124. def OAI.SnakyPrototype.Certificate21.childrenD_360_i0 line 244
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_360_i0 line 245
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_360_i0 line 246
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_360_i0 line 247
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_360_i0 line 248
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_360_i0 line 249
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_360_i0 line 254
  131. def OAI.SnakyPrototype.Certificate21.required_360 line 259
  132. def OAI.SnakyPrototype.Certificate21.envelope_360 line 260
  133. def OAI.SnakyPrototype.Certificate21.childrenC_360 line 261
  134. def OAI.SnakyPrototype.Certificate21.childrenD_360 line 262
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_360 line 263
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_360 line 264
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_360 line 265
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_360 line 266
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_360 line 267
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_360 line 273
  141. def OAI.SnakyPrototype.Certificate21.required_363 line 278
  142. def OAI.SnakyPrototype.Certificate21.envelope_363 line 279
  143. def OAI.SnakyPrototype.Certificate21.childrenC_363 line 280
  144. def OAI.SnakyPrototype.Certificate21.childrenD_363 line 281
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_363 line 282
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_363 line 283
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_363 line 284
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_363 line 285
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_363 line 286
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_363 line 291
  151. def OAI.SnakyPrototype.Certificate21.required_364 line 296
  152. def OAI.SnakyPrototype.Certificate21.envelope_364 line 297
  153. def OAI.SnakyPrototype.Certificate21.childrenC_364 line 298
  154. def OAI.SnakyPrototype.Certificate21.childrenD_364 line 299
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_364 line 300
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_364 line 301
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_364 line 302
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_364 line 303
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_364 line 304
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_364 line 309
  161. def OAI.SnakyPrototype.Certificate21.required_367 line 314
  162. def OAI.SnakyPrototype.Certificate21.envelope_367 line 315
  163. def OAI.SnakyPrototype.Certificate21.childrenC_367 line 316
  164. def OAI.SnakyPrototype.Certificate21.childrenD_367 line 317
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_367 line 318
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_367 line 319
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_367 line 320
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_367 line 321
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_367 line 322
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_367 line 328
  171. def OAI.SnakyPrototype.Certificate21.required_369_i0 line 333
  172. def OAI.SnakyPrototype.Certificate21.envelope_369_i0 line 334
  173. def OAI.SnakyPrototype.Certificate21.childrenC_369_i0 line 335
  174. def OAI.SnakyPrototype.Certificate21.childrenD_369_i0 line 336
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_369_i0 line 337
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_369_i0 line 338
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_369_i0 line 339
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_369_i0 line 340
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_369_i0 line 341
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_369_i0 line 347
  181. def OAI.SnakyPrototype.Certificate21.required_369 line 352
  182. def OAI.SnakyPrototype.Certificate21.envelope_369 line 353
  183. def OAI.SnakyPrototype.Certificate21.childrenC_369 line 354
  184. def OAI.SnakyPrototype.Certificate21.childrenD_369 line 355
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_369 line 356
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_369 line 357
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_369 line 358
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_369 line 359
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_369 line 360
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_369 line 367
  191. def OAI.SnakyPrototype.Certificate21.required_371_i2 line 372
  192. def OAI.SnakyPrototype.Certificate21.envelope_371_i2 line 373
  193. def OAI.SnakyPrototype.Certificate21.childrenC_371_i2 line 374
  194. def OAI.SnakyPrototype.Certificate21.childrenD_371_i2 line 375
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_371_i2 line 376
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_371_i2 line 377
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_371_i2 line 378
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_371_i2 line 379
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_371_i2 line 380
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_371_i2 line 385
  201. def OAI.SnakyPrototype.Certificate21.required_371_i1 line 390
  202. def OAI.SnakyPrototype.Certificate21.envelope_371_i1 line 391
  203. def OAI.SnakyPrototype.Certificate21.childrenC_371_i1 line 392
  204. def OAI.SnakyPrototype.Certificate21.childrenD_371_i1 line 393
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_371_i1 line 394
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_371_i1 line 395
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_371_i1 line 396
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_371_i1 line 397
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_371_i1 line 398
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_371_i1 line 403
  211. def OAI.SnakyPrototype.Certificate21.required_371_i0 line 408
  212. def OAI.SnakyPrototype.Certificate21.envelope_371_i0 line 409
  213. def OAI.SnakyPrototype.Certificate21.childrenC_371_i0 line 410
  214. def OAI.SnakyPrototype.Certificate21.childrenD_371_i0 line 411
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_371_i0 line 412
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_371_i0 line 413
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_371_i0 line 414
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_371_i0 line 415
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_371_i0 line 416
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_371_i0 line 421
  221. def OAI.SnakyPrototype.Certificate21.required_371 line 426
  222. def OAI.SnakyPrototype.Certificate21.envelope_371 line 427
  223. def OAI.SnakyPrototype.Certificate21.childrenC_371 line 428
  224. def OAI.SnakyPrototype.Certificate21.childrenD_371 line 429
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_371 line 430
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_371 line 431
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_371 line 432
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_371 line 433
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_371 line 434
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_371 line 441
  231. def OAI.SnakyPrototype.Certificate21.height_336_i1 line 446
  232. def OAI.SnakyPrototype.Certificate21.childrenH_336_i1 line 447
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_336_i1 line 448
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_336_i1 line 449
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_336_i1 line 451
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_336_i1 line 455
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_336_i1 line 457
  238. def OAI.SnakyPrototype.Certificate21.checked_336_i1 line 461
  239. def OAI.SnakyPrototype.Certificate21.height_336_i0 line 469
  240. def OAI.SnakyPrototype.Certificate21.childrenH_336_i0 line 470
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_336_i0 line 471
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_336_i0 line 472
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_336_i0 line 474
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_336_i0 line 478
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_336_i0 line 480
  246. def OAI.SnakyPrototype.Certificate21.checked_336_i0 line 484
  247. def OAI.SnakyPrototype.Certificate21.height_336 line 492
  248. def OAI.SnakyPrototype.Certificate21.childrenH_336 line 493
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_336 line 494
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_336 line 495
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_336 line 497
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_336 line 501
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_336 line 503
  254. def OAI.SnakyPrototype.Certificate21.checked_336 line 507
  255. def OAI.SnakyPrototype.Certificate21.height_340_i0 line 515
  256. def OAI.SnakyPrototype.Certificate21.childrenH_340_i0 line 516
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_340_i0 line 517
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_340_i0 line 518
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_340_i0 line 520
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_340_i0 line 524
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_340_i0 line 526
  262. def OAI.SnakyPrototype.Certificate21.checked_340_i0 line 530
  263. def OAI.SnakyPrototype.Certificate21.height_340 line 538
  264. def OAI.SnakyPrototype.Certificate21.childrenH_340 line 539
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_340 line 540
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_340 line 541
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_340 line 543
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_340 line 547
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_340 line 549
  270. def OAI.SnakyPrototype.Certificate21.checked_340 line 553
  271. def OAI.SnakyPrototype.Certificate21.height_343 line 561
  272. def OAI.SnakyPrototype.Certificate21.childrenH_343 line 562
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_343 line 563
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_343 line 564
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_343 line 566
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_343 line 570
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_343 line 572
  278. def OAI.SnakyPrototype.Certificate21.checked_343 line 576
  279. def OAI.SnakyPrototype.Certificate21.height_346 line 584
  280. def OAI.SnakyPrototype.Certificate21.childrenH_346 line 585
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_346 line 586
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_346 line 587
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_346 line 589
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_346 line 593
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_346 line 595
  286. def OAI.SnakyPrototype.Certificate21.checked_346 line 599
  287. def OAI.SnakyPrototype.Certificate21.height_348_i0 line 607
  288. def OAI.SnakyPrototype.Certificate21.childrenH_348_i0 line 608
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_348_i0 line 609
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_348_i0 line 610
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_348_i0 line 612
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_348_i0 line 616
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_348_i0 line 618
  294. def OAI.SnakyPrototype.Certificate21.checked_348_i0 line 622
  295. def OAI.SnakyPrototype.Certificate21.height_348 line 630
  296. def OAI.SnakyPrototype.Certificate21.childrenH_348 line 631
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_348 line 632
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_348 line 633
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_348 line 635
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_348 line 639
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_348 line 641
  302. def OAI.SnakyPrototype.Certificate21.checked_348 line 645
  303. def OAI.SnakyPrototype.Certificate21.height_349_i0 line 653
  304. def OAI.SnakyPrototype.Certificate21.childrenH_349_i0 line 654
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_349_i0 line 655
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_349_i0 line 656
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_349_i0 line 658
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_349_i0 line 662
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_349_i0 line 664
  310. def OAI.SnakyPrototype.Certificate21.checked_349_i0 line 668
  311. def OAI.SnakyPrototype.Certificate21.height_349 line 676
  312. def OAI.SnakyPrototype.Certificate21.childrenH_349 line 677
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_349 line 678
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_349 line 679
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_349 line 681
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_349 line 685
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_349 line 687
  318. def OAI.SnakyPrototype.Certificate21.checked_349 line 691
  319. def OAI.SnakyPrototype.Certificate21.height_358 line 699
  320. def OAI.SnakyPrototype.Certificate21.childrenH_358 line 700
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_358 line 701
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_358 line 702
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_358 line 704
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_358 line 708
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_358 line 710
  326. def OAI.SnakyPrototype.Certificate21.checked_358 line 714
  327. def OAI.SnakyPrototype.Certificate21.height_360_i0 line 722
  328. def OAI.SnakyPrototype.Certificate21.childrenH_360_i0 line 723
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_360_i0 line 724
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_360_i0 line 725
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_360_i0 line 727
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_360_i0 line 731
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_360_i0 line 733
  334. def OAI.SnakyPrototype.Certificate21.checked_360_i0 line 737
  335. def OAI.SnakyPrototype.Certificate21.height_360 line 745
  336. def OAI.SnakyPrototype.Certificate21.childrenH_360 line 746
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_360 line 747
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_360 line 748
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_360 line 750
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_360 line 754
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_360 line 756
  342. def OAI.SnakyPrototype.Certificate21.checked_360 line 760
  343. def OAI.SnakyPrototype.Certificate21.height_363 line 768
  344. def OAI.SnakyPrototype.Certificate21.childrenH_363 line 769
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_363 line 770
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_363 line 771
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_363 line 773
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_363 line 777
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_363 line 779
  350. def OAI.SnakyPrototype.Certificate21.checked_363 line 783
  351. def OAI.SnakyPrototype.Certificate21.height_364 line 791
  352. def OAI.SnakyPrototype.Certificate21.childrenH_364 line 792
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_364 line 793
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_364 line 794
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_364 line 796
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_364 line 800
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_364 line 802
  358. def OAI.SnakyPrototype.Certificate21.checked_364 line 806
  359. def OAI.SnakyPrototype.Certificate21.height_367 line 814
  360. def OAI.SnakyPrototype.Certificate21.childrenH_367 line 815
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_367 line 816
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_367 line 817
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_367 line 819
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_367 line 823
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_367 line 825
  366. def OAI.SnakyPrototype.Certificate21.checked_367 line 829
  367. def OAI.SnakyPrototype.Certificate21.height_369_i0 line 837
  368. def OAI.SnakyPrototype.Certificate21.childrenH_369_i0 line 838
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_369_i0 line 839
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_369_i0 line 840
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_369_i0 line 842
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_369_i0 line 846
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_369_i0 line 848
  374. def OAI.SnakyPrototype.Certificate21.checked_369_i0 line 852
  375. def OAI.SnakyPrototype.Certificate21.height_369 line 860
  376. def OAI.SnakyPrototype.Certificate21.childrenH_369 line 861
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_369 line 862
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_369 line 863
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_369 line 865
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_369 line 869
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_369 line 871
  382. def OAI.SnakyPrototype.Certificate21.checked_369 line 875
  383. def OAI.SnakyPrototype.Certificate21.height_371_i2 line 883
  384. def OAI.SnakyPrototype.Certificate21.childrenH_371_i2 line 884
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_371_i2 line 885
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_371_i2 line 886
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_371_i2 line 888
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_371_i2 line 892
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_371_i2 line 894
  390. def OAI.SnakyPrototype.Certificate21.checked_371_i2 line 898
  391. def OAI.SnakyPrototype.Certificate21.height_371_i1 line 906
  392. def OAI.SnakyPrototype.Certificate21.childrenH_371_i1 line 907
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_371_i1 line 908
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_371_i1 line 909
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_371_i1 line 911
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_371_i1 line 915
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_371_i1 line 917
  398. def OAI.SnakyPrototype.Certificate21.checked_371_i1 line 921
  399. def OAI.SnakyPrototype.Certificate21.height_371_i0 line 929
  400. def OAI.SnakyPrototype.Certificate21.childrenH_371_i0 line 930
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_371_i0 line 931
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_371_i0 line 932
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_371_i0 line 934
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_371_i0 line 938
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_371_i0 line 940
  406. def OAI.SnakyPrototype.Certificate21.checked_371_i0 line 944
  407. def OAI.SnakyPrototype.Certificate21.height_371 line 952
  408. def OAI.SnakyPrototype.Certificate21.childrenH_371 line 953
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_371 line 954
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_371 line 955
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_371 line 957
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_371 line 961
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_371 line 963
  414. def OAI.SnakyPrototype.Certificate21.checked_371 line 967