OAI/GameTheory/SnakyTwentyOne/Cards/Height07Part02.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_361 line 22
  2. def OAI.SnakyPrototype.Certificate21.envelope_361 line 23
  3. def OAI.SnakyPrototype.Certificate21.childrenC_361 line 24
  4. def OAI.SnakyPrototype.Certificate21.childrenD_361 line 25
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_361 line 26
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_361 line 27
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_361 line 28
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_361 line 29
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_361 line 30
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_361 line 36
  11. def OAI.SnakyPrototype.Certificate21.required_372_i0 line 41
  12. def OAI.SnakyPrototype.Certificate21.envelope_372_i0 line 42
  13. def OAI.SnakyPrototype.Certificate21.childrenC_372_i0 line 43
  14. def OAI.SnakyPrototype.Certificate21.childrenD_372_i0 line 44
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_372_i0 line 45
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_372_i0 line 46
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_372_i0 line 47
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_372_i0 line 48
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_372_i0 line 49
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_372_i0 line 54
  21. def OAI.SnakyPrototype.Certificate21.required_372 line 59
  22. def OAI.SnakyPrototype.Certificate21.envelope_372 line 60
  23. def OAI.SnakyPrototype.Certificate21.childrenC_372 line 61
  24. def OAI.SnakyPrototype.Certificate21.childrenD_372 line 62
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_372 line 63
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_372 line 64
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_372 line 65
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_372 line 66
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_372 line 67
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_372 line 72
  31. def OAI.SnakyPrototype.Certificate21.required_379 line 77
  32. def OAI.SnakyPrototype.Certificate21.envelope_379 line 78
  33. def OAI.SnakyPrototype.Certificate21.childrenC_379 line 79
  34. def OAI.SnakyPrototype.Certificate21.childrenD_379 line 80
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_379 line 81
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_379 line 82
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_379 line 83
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_379 line 84
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_379 line 85
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_379 line 91
  41. def OAI.SnakyPrototype.Certificate21.required_385 line 96
  42. def OAI.SnakyPrototype.Certificate21.envelope_385 line 97
  43. def OAI.SnakyPrototype.Certificate21.childrenC_385 line 98
  44. def OAI.SnakyPrototype.Certificate21.childrenD_385 line 99
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_385 line 100
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_385 line 101
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_385 line 102
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_385 line 103
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_385 line 104
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_385 line 109
  51. def OAI.SnakyPrototype.Certificate21.required_388 line 114
  52. def OAI.SnakyPrototype.Certificate21.envelope_388 line 115
  53. def OAI.SnakyPrototype.Certificate21.childrenC_388 line 116
  54. def OAI.SnakyPrototype.Certificate21.childrenD_388 line 117
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_388 line 118
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_388 line 119
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_388 line 120
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_388 line 121
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_388 line 122
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_388 line 127
  61. def OAI.SnakyPrototype.Certificate21.required_394 line 132
  62. def OAI.SnakyPrototype.Certificate21.envelope_394 line 133
  63. def OAI.SnakyPrototype.Certificate21.childrenC_394 line 134
  64. def OAI.SnakyPrototype.Certificate21.childrenD_394 line 135
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_394 line 136
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_394 line 137
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_394 line 138
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_394 line 139
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_394 line 140
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_394 line 146
  71. def OAI.SnakyPrototype.Certificate21.required_404_i1 line 151
  72. def OAI.SnakyPrototype.Certificate21.envelope_404_i1 line 152
  73. def OAI.SnakyPrototype.Certificate21.childrenC_404_i1 line 153
  74. def OAI.SnakyPrototype.Certificate21.childrenD_404_i1 line 154
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_404_i1 line 155
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_404_i1 line 156
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_404_i1 line 157
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_404_i1 line 158
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_404_i1 line 159
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_404_i1 line 164
  81. def OAI.SnakyPrototype.Certificate21.required_404_i0 line 169
  82. def OAI.SnakyPrototype.Certificate21.envelope_404_i0 line 170
  83. def OAI.SnakyPrototype.Certificate21.childrenC_404_i0 line 171
  84. def OAI.SnakyPrototype.Certificate21.childrenD_404_i0 line 172
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_404_i0 line 173
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_404_i0 line 174
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_404_i0 line 175
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_404_i0 line 176
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_404_i0 line 177
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_404_i0 line 182
  91. def OAI.SnakyPrototype.Certificate21.required_404 line 187
  92. def OAI.SnakyPrototype.Certificate21.envelope_404 line 188
  93. def OAI.SnakyPrototype.Certificate21.childrenC_404 line 189
  94. def OAI.SnakyPrototype.Certificate21.childrenD_404 line 190
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_404 line 191
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_404 line 192
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_404 line 193
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_404 line 194
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_404 line 195
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_404 line 200
  101. def OAI.SnakyPrototype.Certificate21.required_415 line 205
  102. def OAI.SnakyPrototype.Certificate21.envelope_415 line 206
  103. def OAI.SnakyPrototype.Certificate21.childrenC_415 line 207
  104. def OAI.SnakyPrototype.Certificate21.childrenD_415 line 208
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_415 line 209
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_415 line 210
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_415 line 211
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_415 line 212
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_415 line 213
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_415 line 218
  111. def OAI.SnakyPrototype.Certificate21.required_418_i2 line 223
  112. def OAI.SnakyPrototype.Certificate21.envelope_418_i2 line 224
  113. def OAI.SnakyPrototype.Certificate21.childrenC_418_i2 line 225
  114. def OAI.SnakyPrototype.Certificate21.childrenD_418_i2 line 226
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_418_i2 line 227
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_418_i2 line 228
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_418_i2 line 229
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_418_i2 line 230
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_418_i2 line 231
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_418_i2 line 236
  121. def OAI.SnakyPrototype.Certificate21.required_418_i1 line 241
  122. def OAI.SnakyPrototype.Certificate21.envelope_418_i1 line 242
  123. def OAI.SnakyPrototype.Certificate21.childrenC_418_i1 line 243
  124. def OAI.SnakyPrototype.Certificate21.childrenD_418_i1 line 244
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_418_i1 line 245
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_418_i1 line 246
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_418_i1 line 247
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_418_i1 line 248
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_418_i1 line 249
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_418_i1 line 256
  131. def OAI.SnakyPrototype.Certificate21.required_418_i0 line 261
  132. def OAI.SnakyPrototype.Certificate21.envelope_418_i0 line 262
  133. def OAI.SnakyPrototype.Certificate21.childrenC_418_i0 line 263
  134. def OAI.SnakyPrototype.Certificate21.childrenD_418_i0 line 264
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_418_i0 line 265
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_418_i0 line 266
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_418_i0 line 267
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_418_i0 line 268
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_418_i0 line 269
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_418_i0 line 274
  141. def OAI.SnakyPrototype.Certificate21.required_418 line 279
  142. def OAI.SnakyPrototype.Certificate21.envelope_418 line 280
  143. def OAI.SnakyPrototype.Certificate21.childrenC_418 line 281
  144. def OAI.SnakyPrototype.Certificate21.childrenD_418 line 282
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_418 line 283
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_418 line 284
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_418 line 285
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_418 line 286
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_418 line 287
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_418 line 292
  151. def OAI.SnakyPrototype.Certificate21.required_422_i0 line 297
  152. def OAI.SnakyPrototype.Certificate21.envelope_422_i0 line 298
  153. def OAI.SnakyPrototype.Certificate21.childrenC_422_i0 line 299
  154. def OAI.SnakyPrototype.Certificate21.childrenD_422_i0 line 300
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_422_i0 line 301
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_422_i0 line 302
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_422_i0 line 303
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_422_i0 line 304
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_422_i0 line 305
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_422_i0 line 310
  161. def OAI.SnakyPrototype.Certificate21.required_422 line 315
  162. def OAI.SnakyPrototype.Certificate21.envelope_422 line 316
  163. def OAI.SnakyPrototype.Certificate21.childrenC_422 line 317
  164. def OAI.SnakyPrototype.Certificate21.childrenD_422 line 318
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_422 line 319
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_422 line 320
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_422 line 321
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_422 line 322
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_422 line 323
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_422 line 328
  171. def OAI.SnakyPrototype.Certificate21.required_430 line 333
  172. def OAI.SnakyPrototype.Certificate21.envelope_430 line 334
  173. def OAI.SnakyPrototype.Certificate21.childrenC_430 line 335
  174. def OAI.SnakyPrototype.Certificate21.childrenD_430 line 336
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_430 line 337
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_430 line 338
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_430 line 339
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_430 line 340
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_430 line 341
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_430 line 349
  181. def OAI.SnakyPrototype.Certificate21.required_431 line 354
  182. def OAI.SnakyPrototype.Certificate21.envelope_431 line 355
  183. def OAI.SnakyPrototype.Certificate21.childrenC_431 line 356
  184. def OAI.SnakyPrototype.Certificate21.childrenD_431 line 357
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_431 line 358
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_431 line 359
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_431 line 360
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_431 line 361
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_431 line 362
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_431 line 368
  191. def OAI.SnakyPrototype.Certificate21.required_436 line 373
  192. def OAI.SnakyPrototype.Certificate21.envelope_436 line 374
  193. def OAI.SnakyPrototype.Certificate21.childrenC_436 line 375
  194. def OAI.SnakyPrototype.Certificate21.childrenD_436 line 376
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_436 line 377
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_436 line 378
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_436 line 379
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_436 line 380
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_436 line 381
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_436 line 388
  201. def OAI.SnakyPrototype.Certificate21.required_437 line 393
  202. def OAI.SnakyPrototype.Certificate21.envelope_437 line 394
  203. def OAI.SnakyPrototype.Certificate21.childrenC_437 line 395
  204. def OAI.SnakyPrototype.Certificate21.childrenD_437 line 396
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_437 line 397
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_437 line 398
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_437 line 399
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_437 line 400
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_437 line 401
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_437 line 408
  211. def OAI.SnakyPrototype.Certificate21.required_446_i0 line 413
  212. def OAI.SnakyPrototype.Certificate21.envelope_446_i0 line 414
  213. def OAI.SnakyPrototype.Certificate21.childrenC_446_i0 line 415
  214. def OAI.SnakyPrototype.Certificate21.childrenD_446_i0 line 416
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_446_i0 line 417
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_446_i0 line 418
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_446_i0 line 419
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_446_i0 line 420
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_446_i0 line 421
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_446_i0 line 426
  221. def OAI.SnakyPrototype.Certificate21.required_446 line 431
  222. def OAI.SnakyPrototype.Certificate21.envelope_446 line 432
  223. def OAI.SnakyPrototype.Certificate21.childrenC_446 line 433
  224. def OAI.SnakyPrototype.Certificate21.childrenD_446 line 434
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_446 line 435
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_446 line 436
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_446 line 437
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_446 line 438
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_446 line 439
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_446 line 444
  231. def OAI.SnakyPrototype.Certificate21.height_361 line 449
  232. def OAI.SnakyPrototype.Certificate21.childrenH_361 line 450
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_361 line 451
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_361 line 452
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_361 line 454
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_361 line 458
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_361 line 460
  238. def OAI.SnakyPrototype.Certificate21.checked_361 line 464
  239. def OAI.SnakyPrototype.Certificate21.height_372_i0 line 472
  240. def OAI.SnakyPrototype.Certificate21.childrenH_372_i0 line 473
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_372_i0 line 474
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_372_i0 line 475
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_372_i0 line 477
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_372_i0 line 481
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_372_i0 line 483
  246. def OAI.SnakyPrototype.Certificate21.checked_372_i0 line 487
  247. def OAI.SnakyPrototype.Certificate21.height_372 line 495
  248. def OAI.SnakyPrototype.Certificate21.childrenH_372 line 496
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_372 line 497
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_372 line 498
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_372 line 500
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_372 line 504
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_372 line 506
  254. def OAI.SnakyPrototype.Certificate21.checked_372 line 510
  255. def OAI.SnakyPrototype.Certificate21.height_379 line 518
  256. def OAI.SnakyPrototype.Certificate21.childrenH_379 line 519
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_379 line 520
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_379 line 521
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_379 line 523
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_379 line 527
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_379 line 529
  262. def OAI.SnakyPrototype.Certificate21.checked_379 line 533
  263. def OAI.SnakyPrototype.Certificate21.height_385 line 541
  264. def OAI.SnakyPrototype.Certificate21.childrenH_385 line 542
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_385 line 543
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_385 line 544
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_385 line 546
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_385 line 550
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_385 line 552
  270. def OAI.SnakyPrototype.Certificate21.checked_385 line 556
  271. def OAI.SnakyPrototype.Certificate21.height_388 line 564
  272. def OAI.SnakyPrototype.Certificate21.childrenH_388 line 565
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_388 line 566
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_388 line 567
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_388 line 569
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_388 line 573
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_388 line 575
  278. def OAI.SnakyPrototype.Certificate21.checked_388 line 579
  279. def OAI.SnakyPrototype.Certificate21.height_394 line 587
  280. def OAI.SnakyPrototype.Certificate21.childrenH_394 line 588
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_394 line 589
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_394 line 590
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_394 line 592
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_394 line 596
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_394 line 598
  286. def OAI.SnakyPrototype.Certificate21.checked_394 line 602
  287. def OAI.SnakyPrototype.Certificate21.height_404_i1 line 610
  288. def OAI.SnakyPrototype.Certificate21.childrenH_404_i1 line 611
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_404_i1 line 612
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_404_i1 line 613
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_404_i1 line 615
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_404_i1 line 619
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_404_i1 line 621
  294. def OAI.SnakyPrototype.Certificate21.checked_404_i1 line 625
  295. def OAI.SnakyPrototype.Certificate21.height_404_i0 line 633
  296. def OAI.SnakyPrototype.Certificate21.childrenH_404_i0 line 634
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_404_i0 line 635
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_404_i0 line 636
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_404_i0 line 638
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_404_i0 line 642
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_404_i0 line 644
  302. def OAI.SnakyPrototype.Certificate21.checked_404_i0 line 648
  303. def OAI.SnakyPrototype.Certificate21.height_404 line 656
  304. def OAI.SnakyPrototype.Certificate21.childrenH_404 line 657
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_404 line 658
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_404 line 659
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_404 line 661
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_404 line 665
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_404 line 667
  310. def OAI.SnakyPrototype.Certificate21.checked_404 line 671
  311. def OAI.SnakyPrototype.Certificate21.height_415 line 679
  312. def OAI.SnakyPrototype.Certificate21.childrenH_415 line 680
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_415 line 681
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_415 line 682
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_415 line 684
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_415 line 688
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_415 line 690
  318. def OAI.SnakyPrototype.Certificate21.checked_415 line 694
  319. def OAI.SnakyPrototype.Certificate21.height_418_i2 line 702
  320. def OAI.SnakyPrototype.Certificate21.childrenH_418_i2 line 703
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_418_i2 line 704
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_418_i2 line 705
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_418_i2 line 707
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_418_i2 line 711
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_418_i2 line 713
  326. def OAI.SnakyPrototype.Certificate21.checked_418_i2 line 717
  327. def OAI.SnakyPrototype.Certificate21.height_418_i1 line 725
  328. def OAI.SnakyPrototype.Certificate21.childrenH_418_i1 line 726
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_418_i1 line 727
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_418_i1 line 728
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_418_i1 line 730
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_418_i1 line 734
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_418_i1 line 736
  334. def OAI.SnakyPrototype.Certificate21.checked_418_i1 line 740
  335. def OAI.SnakyPrototype.Certificate21.height_418_i0 line 748
  336. def OAI.SnakyPrototype.Certificate21.childrenH_418_i0 line 749
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_418_i0 line 750
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_418_i0 line 751
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_418_i0 line 753
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_418_i0 line 757
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_418_i0 line 759
  342. def OAI.SnakyPrototype.Certificate21.checked_418_i0 line 763
  343. def OAI.SnakyPrototype.Certificate21.height_418 line 771
  344. def OAI.SnakyPrototype.Certificate21.childrenH_418 line 772
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_418 line 773
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_418 line 774
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_418 line 776
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_418 line 780
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_418 line 782
  350. def OAI.SnakyPrototype.Certificate21.checked_418 line 786
  351. def OAI.SnakyPrototype.Certificate21.height_422_i0 line 794
  352. def OAI.SnakyPrototype.Certificate21.childrenH_422_i0 line 795
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_422_i0 line 796
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_422_i0 line 797
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_422_i0 line 799
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_422_i0 line 803
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_422_i0 line 805
  358. def OAI.SnakyPrototype.Certificate21.checked_422_i0 line 809
  359. def OAI.SnakyPrototype.Certificate21.height_422 line 817
  360. def OAI.SnakyPrototype.Certificate21.childrenH_422 line 818
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_422 line 819
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_422 line 820
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_422 line 822
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_422 line 826
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_422 line 828
  366. def OAI.SnakyPrototype.Certificate21.checked_422 line 832
  367. def OAI.SnakyPrototype.Certificate21.height_430 line 840
  368. def OAI.SnakyPrototype.Certificate21.childrenH_430 line 841
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_430 line 842
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_430 line 843
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_430 line 845
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_430 line 849
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_430 line 851
  374. def OAI.SnakyPrototype.Certificate21.checked_430 line 855
  375. def OAI.SnakyPrototype.Certificate21.height_431 line 863
  376. def OAI.SnakyPrototype.Certificate21.childrenH_431 line 864
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_431 line 865
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_431 line 866
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_431 line 868
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_431 line 872
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_431 line 874
  382. def OAI.SnakyPrototype.Certificate21.checked_431 line 878
  383. def OAI.SnakyPrototype.Certificate21.height_436 line 886
  384. def OAI.SnakyPrototype.Certificate21.childrenH_436 line 887
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_436 line 888
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_436 line 889
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_436 line 891
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_436 line 895
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_436 line 897
  390. def OAI.SnakyPrototype.Certificate21.checked_436 line 901
  391. def OAI.SnakyPrototype.Certificate21.height_437 line 909
  392. def OAI.SnakyPrototype.Certificate21.childrenH_437 line 910
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_437 line 911
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_437 line 912
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_437 line 914
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_437 line 918
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_437 line 920
  398. def OAI.SnakyPrototype.Certificate21.checked_437 line 924
  399. def OAI.SnakyPrototype.Certificate21.height_446_i0 line 932
  400. def OAI.SnakyPrototype.Certificate21.childrenH_446_i0 line 933
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_446_i0 line 934
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_446_i0 line 935
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_446_i0 line 937
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_446_i0 line 941
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_446_i0 line 943
  406. def OAI.SnakyPrototype.Certificate21.checked_446_i0 line 947
  407. def OAI.SnakyPrototype.Certificate21.height_446 line 955
  408. def OAI.SnakyPrototype.Certificate21.childrenH_446 line 956
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_446 line 957
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_446 line 958
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_446 line 960
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_446 line 964
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_446 line 966
  414. def OAI.SnakyPrototype.Certificate21.checked_446 line 970