OAI/GameTheory/SnakyTwentyOne/Cards/Height05Part04.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_356_i0 line 16
  2. def OAI.SnakyPrototype.Certificate21.envelope_356_i0 line 17
  3. def OAI.SnakyPrototype.Certificate21.childrenC_356_i0 line 18
  4. def OAI.SnakyPrototype.Certificate21.childrenD_356_i0 line 19
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_356_i0 line 20
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_356_i0 line 21
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_356_i0 line 22
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_356_i0 line 23
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_356_i0 line 24
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_356_i0 line 29
  11. def OAI.SnakyPrototype.Certificate21.required_356 line 34
  12. def OAI.SnakyPrototype.Certificate21.envelope_356 line 35
  13. def OAI.SnakyPrototype.Certificate21.childrenC_356 line 36
  14. def OAI.SnakyPrototype.Certificate21.childrenD_356 line 37
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_356 line 38
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_356 line 39
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_356 line 40
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_356 line 41
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_356 line 42
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_356 line 48
  21. def OAI.SnakyPrototype.Certificate21.required_357_i2 line 53
  22. def OAI.SnakyPrototype.Certificate21.envelope_357_i2 line 54
  23. def OAI.SnakyPrototype.Certificate21.childrenC_357_i2 line 55
  24. def OAI.SnakyPrototype.Certificate21.childrenD_357_i2 line 56
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_357_i2 line 57
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_357_i2 line 58
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_357_i2 line 59
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_357_i2 line 60
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_357_i2 line 61
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_357_i2 line 66
  31. def OAI.SnakyPrototype.Certificate21.required_357_i1 line 71
  32. def OAI.SnakyPrototype.Certificate21.envelope_357_i1 line 72
  33. def OAI.SnakyPrototype.Certificate21.childrenC_357_i1 line 73
  34. def OAI.SnakyPrototype.Certificate21.childrenD_357_i1 line 74
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_357_i1 line 75
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_357_i1 line 76
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_357_i1 line 77
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_357_i1 line 78
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_357_i1 line 79
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_357_i1 line 84
  41. def OAI.SnakyPrototype.Certificate21.required_357_i0 line 89
  42. def OAI.SnakyPrototype.Certificate21.envelope_357_i0 line 90
  43. def OAI.SnakyPrototype.Certificate21.childrenC_357_i0 line 91
  44. def OAI.SnakyPrototype.Certificate21.childrenD_357_i0 line 92
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_357_i0 line 93
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_357_i0 line 94
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_357_i0 line 95
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_357_i0 line 96
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_357_i0 line 97
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_357_i0 line 102
  51. def OAI.SnakyPrototype.Certificate21.required_357 line 107
  52. def OAI.SnakyPrototype.Certificate21.envelope_357 line 108
  53. def OAI.SnakyPrototype.Certificate21.childrenC_357 line 109
  54. def OAI.SnakyPrototype.Certificate21.childrenD_357 line 110
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_357 line 111
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_357 line 112
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_357 line 113
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_357 line 114
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_357 line 115
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_357 line 120
  61. def OAI.SnakyPrototype.Certificate21.required_359_i0 line 125
  62. def OAI.SnakyPrototype.Certificate21.envelope_359_i0 line 126
  63. def OAI.SnakyPrototype.Certificate21.childrenC_359_i0 line 127
  64. def OAI.SnakyPrototype.Certificate21.childrenD_359_i0 line 128
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_359_i0 line 129
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_359_i0 line 130
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_359_i0 line 131
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_359_i0 line 132
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_359_i0 line 133
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_359_i0 line 138
  71. def OAI.SnakyPrototype.Certificate21.required_359 line 143
  72. def OAI.SnakyPrototype.Certificate21.envelope_359 line 144
  73. def OAI.SnakyPrototype.Certificate21.childrenC_359 line 145
  74. def OAI.SnakyPrototype.Certificate21.childrenD_359 line 146
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_359 line 147
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_359 line 148
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_359 line 149
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_359 line 150
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_359 line 151
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_359 line 158
  81. def OAI.SnakyPrototype.Certificate21.required_362_i0 line 163
  82. def OAI.SnakyPrototype.Certificate21.envelope_362_i0 line 164
  83. def OAI.SnakyPrototype.Certificate21.childrenC_362_i0 line 165
  84. def OAI.SnakyPrototype.Certificate21.childrenD_362_i0 line 166
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_362_i0 line 167
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_362_i0 line 168
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_362_i0 line 169
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_362_i0 line 170
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_362_i0 line 171
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_362_i0 line 176
  91. def OAI.SnakyPrototype.Certificate21.required_362 line 181
  92. def OAI.SnakyPrototype.Certificate21.envelope_362 line 182
  93. def OAI.SnakyPrototype.Certificate21.childrenC_362 line 183
  94. def OAI.SnakyPrototype.Certificate21.childrenD_362 line 184
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_362 line 185
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_362 line 186
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_362 line 187
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_362 line 188
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_362 line 189
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_362 line 194
  101. def OAI.SnakyPrototype.Certificate21.required_366 line 199
  102. def OAI.SnakyPrototype.Certificate21.envelope_366 line 200
  103. def OAI.SnakyPrototype.Certificate21.childrenC_366 line 201
  104. def OAI.SnakyPrototype.Certificate21.childrenD_366 line 202
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_366 line 203
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_366 line 204
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_366 line 205
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_366 line 206
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_366 line 207
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_366 line 212
  111. def OAI.SnakyPrototype.Certificate21.required_370_i0 line 217
  112. def OAI.SnakyPrototype.Certificate21.envelope_370_i0 line 218
  113. def OAI.SnakyPrototype.Certificate21.childrenC_370_i0 line 219
  114. def OAI.SnakyPrototype.Certificate21.childrenD_370_i0 line 220
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_370_i0 line 221
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_370_i0 line 222
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_370_i0 line 223
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_370_i0 line 224
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_370_i0 line 225
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_370_i0 line 230
  121. def OAI.SnakyPrototype.Certificate21.required_370 line 235
  122. def OAI.SnakyPrototype.Certificate21.envelope_370 line 236
  123. def OAI.SnakyPrototype.Certificate21.childrenC_370 line 237
  124. def OAI.SnakyPrototype.Certificate21.childrenD_370 line 238
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_370 line 239
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_370 line 240
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_370 line 241
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_370 line 242
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_370 line 243
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_370 line 248
  131. def OAI.SnakyPrototype.Certificate21.required_377 line 253
  132. def OAI.SnakyPrototype.Certificate21.envelope_377 line 254
  133. def OAI.SnakyPrototype.Certificate21.childrenC_377 line 255
  134. def OAI.SnakyPrototype.Certificate21.childrenD_377 line 256
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_377 line 257
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_377 line 258
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_377 line 259
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_377 line 260
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_377 line 261
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_377 line 267
  141. def OAI.SnakyPrototype.Certificate21.required_382 line 272
  142. def OAI.SnakyPrototype.Certificate21.envelope_382 line 273
  143. def OAI.SnakyPrototype.Certificate21.childrenC_382 line 274
  144. def OAI.SnakyPrototype.Certificate21.childrenD_382 line 275
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_382 line 276
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_382 line 277
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_382 line 278
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_382 line 279
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_382 line 280
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_382 line 285
  151. def OAI.SnakyPrototype.Certificate21.required_383_i0 line 290
  152. def OAI.SnakyPrototype.Certificate21.envelope_383_i0 line 291
  153. def OAI.SnakyPrototype.Certificate21.childrenC_383_i0 line 292
  154. def OAI.SnakyPrototype.Certificate21.childrenD_383_i0 line 293
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_383_i0 line 294
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_383_i0 line 295
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_383_i0 line 296
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_383_i0 line 297
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_383_i0 line 298
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_383_i0 line 303
  161. def OAI.SnakyPrototype.Certificate21.required_383 line 308
  162. def OAI.SnakyPrototype.Certificate21.envelope_383 line 309
  163. def OAI.SnakyPrototype.Certificate21.childrenC_383 line 310
  164. def OAI.SnakyPrototype.Certificate21.childrenD_383 line 311
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_383 line 312
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_383 line 313
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_383 line 314
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_383 line 315
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_383 line 316
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_383 line 321
  171. def OAI.SnakyPrototype.Certificate21.required_386_i1 line 326
  172. def OAI.SnakyPrototype.Certificate21.envelope_386_i1 line 327
  173. def OAI.SnakyPrototype.Certificate21.childrenC_386_i1 line 328
  174. def OAI.SnakyPrototype.Certificate21.childrenD_386_i1 line 329
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_386_i1 line 330
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_386_i1 line 331
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_386_i1 line 332
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_386_i1 line 333
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_386_i1 line 334
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_386_i1 line 339
  181. def OAI.SnakyPrototype.Certificate21.required_386_i0 line 344
  182. def OAI.SnakyPrototype.Certificate21.envelope_386_i0 line 345
  183. def OAI.SnakyPrototype.Certificate21.childrenC_386_i0 line 346
  184. def OAI.SnakyPrototype.Certificate21.childrenD_386_i0 line 347
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_386_i0 line 348
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_386_i0 line 349
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_386_i0 line 350
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_386_i0 line 351
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_386_i0 line 352
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_386_i0 line 357
  191. def OAI.SnakyPrototype.Certificate21.required_386 line 362
  192. def OAI.SnakyPrototype.Certificate21.envelope_386 line 363
  193. def OAI.SnakyPrototype.Certificate21.childrenC_386 line 364
  194. def OAI.SnakyPrototype.Certificate21.childrenD_386 line 365
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_386 line 366
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_386 line 367
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_386 line 368
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_386 line 369
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_386 line 370
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_386 line 375
  201. def OAI.SnakyPrototype.Certificate21.required_389_i0 line 380
  202. def OAI.SnakyPrototype.Certificate21.envelope_389_i0 line 381
  203. def OAI.SnakyPrototype.Certificate21.childrenC_389_i0 line 382
  204. def OAI.SnakyPrototype.Certificate21.childrenD_389_i0 line 383
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_389_i0 line 384
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_389_i0 line 385
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_389_i0 line 386
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_389_i0 line 387
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_389_i0 line 388
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_389_i0 line 393
  211. def OAI.SnakyPrototype.Certificate21.required_389 line 398
  212. def OAI.SnakyPrototype.Certificate21.envelope_389 line 399
  213. def OAI.SnakyPrototype.Certificate21.childrenC_389 line 400
  214. def OAI.SnakyPrototype.Certificate21.childrenD_389 line 401
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_389 line 402
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_389 line 403
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_389 line 404
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_389 line 405
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_389 line 406
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_389 line 413
  221. def OAI.SnakyPrototype.Certificate21.height_356_i0 line 418
  222. def OAI.SnakyPrototype.Certificate21.childrenH_356_i0 line 419
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_356_i0 line 420
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_356_i0 line 421
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_356_i0 line 423
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_356_i0 line 427
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_356_i0 line 429
  228. def OAI.SnakyPrototype.Certificate21.checked_356_i0 line 433
  229. def OAI.SnakyPrototype.Certificate21.height_356 line 441
  230. def OAI.SnakyPrototype.Certificate21.childrenH_356 line 442
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_356 line 443
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_356 line 444
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_356 line 446
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_356 line 450
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_356 line 452
  236. def OAI.SnakyPrototype.Certificate21.checked_356 line 456
  237. def OAI.SnakyPrototype.Certificate21.height_357_i2 line 464
  238. def OAI.SnakyPrototype.Certificate21.childrenH_357_i2 line 465
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_357_i2 line 466
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_357_i2 line 467
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_357_i2 line 469
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_357_i2 line 473
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_357_i2 line 475
  244. def OAI.SnakyPrototype.Certificate21.checked_357_i2 line 479
  245. def OAI.SnakyPrototype.Certificate21.height_357_i1 line 487
  246. def OAI.SnakyPrototype.Certificate21.childrenH_357_i1 line 488
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_357_i1 line 489
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_357_i1 line 490
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_357_i1 line 492
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_357_i1 line 496
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_357_i1 line 498
  252. def OAI.SnakyPrototype.Certificate21.checked_357_i1 line 502
  253. def OAI.SnakyPrototype.Certificate21.height_357_i0 line 510
  254. def OAI.SnakyPrototype.Certificate21.childrenH_357_i0 line 511
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_357_i0 line 512
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_357_i0 line 513
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_357_i0 line 515
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_357_i0 line 519
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_357_i0 line 521
  260. def OAI.SnakyPrototype.Certificate21.checked_357_i0 line 525
  261. def OAI.SnakyPrototype.Certificate21.height_357 line 533
  262. def OAI.SnakyPrototype.Certificate21.childrenH_357 line 534
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_357 line 535
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_357 line 536
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_357 line 538
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_357 line 542
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_357 line 544
  268. def OAI.SnakyPrototype.Certificate21.checked_357 line 548
  269. def OAI.SnakyPrototype.Certificate21.height_359_i0 line 556
  270. def OAI.SnakyPrototype.Certificate21.childrenH_359_i0 line 557
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_359_i0 line 558
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_359_i0 line 559
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_359_i0 line 561
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_359_i0 line 565
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_359_i0 line 567
  276. def OAI.SnakyPrototype.Certificate21.checked_359_i0 line 571
  277. def OAI.SnakyPrototype.Certificate21.height_359 line 579
  278. def OAI.SnakyPrototype.Certificate21.childrenH_359 line 580
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_359 line 581
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_359 line 582
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_359 line 584
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_359 line 588
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_359 line 590
  284. def OAI.SnakyPrototype.Certificate21.checked_359 line 594
  285. def OAI.SnakyPrototype.Certificate21.height_362_i0 line 602
  286. def OAI.SnakyPrototype.Certificate21.childrenH_362_i0 line 603
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_362_i0 line 604
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_362_i0 line 605
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_362_i0 line 607
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_362_i0 line 611
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_362_i0 line 613
  292. def OAI.SnakyPrototype.Certificate21.checked_362_i0 line 617
  293. def OAI.SnakyPrototype.Certificate21.height_362 line 625
  294. def OAI.SnakyPrototype.Certificate21.childrenH_362 line 626
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_362 line 627
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_362 line 628
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_362 line 630
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_362 line 634
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_362 line 636
  300. def OAI.SnakyPrototype.Certificate21.checked_362 line 640
  301. def OAI.SnakyPrototype.Certificate21.height_366 line 648
  302. def OAI.SnakyPrototype.Certificate21.childrenH_366 line 649
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_366 line 650
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_366 line 651
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_366 line 653
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_366 line 657
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_366 line 659
  308. def OAI.SnakyPrototype.Certificate21.checked_366 line 663
  309. def OAI.SnakyPrototype.Certificate21.height_370_i0 line 671
  310. def OAI.SnakyPrototype.Certificate21.childrenH_370_i0 line 672
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_370_i0 line 673
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_370_i0 line 674
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_370_i0 line 676
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_370_i0 line 680
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_370_i0 line 682
  316. def OAI.SnakyPrototype.Certificate21.checked_370_i0 line 686
  317. def OAI.SnakyPrototype.Certificate21.height_370 line 694
  318. def OAI.SnakyPrototype.Certificate21.childrenH_370 line 695
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_370 line 696
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_370 line 697
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_370 line 699
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_370 line 703
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_370 line 705
  324. def OAI.SnakyPrototype.Certificate21.checked_370 line 709
  325. def OAI.SnakyPrototype.Certificate21.height_377 line 717
  326. def OAI.SnakyPrototype.Certificate21.childrenH_377 line 718
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_377 line 719
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_377 line 720
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_377 line 722
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_377 line 726
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_377 line 728
  332. def OAI.SnakyPrototype.Certificate21.checked_377 line 732
  333. def OAI.SnakyPrototype.Certificate21.height_382 line 740
  334. def OAI.SnakyPrototype.Certificate21.childrenH_382 line 741
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_382 line 742
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_382 line 743
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_382 line 745
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_382 line 749
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_382 line 751
  340. def OAI.SnakyPrototype.Certificate21.checked_382 line 755
  341. def OAI.SnakyPrototype.Certificate21.height_383_i0 line 763
  342. def OAI.SnakyPrototype.Certificate21.childrenH_383_i0 line 764
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_383_i0 line 765
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_383_i0 line 766
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_383_i0 line 768
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_383_i0 line 772
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_383_i0 line 774
  348. def OAI.SnakyPrototype.Certificate21.checked_383_i0 line 778
  349. def OAI.SnakyPrototype.Certificate21.height_383 line 786
  350. def OAI.SnakyPrototype.Certificate21.childrenH_383 line 787
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_383 line 788
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_383 line 789
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_383 line 791
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_383 line 795
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_383 line 797
  356. def OAI.SnakyPrototype.Certificate21.checked_383 line 801
  357. def OAI.SnakyPrototype.Certificate21.height_386_i1 line 809
  358. def OAI.SnakyPrototype.Certificate21.childrenH_386_i1 line 810
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_386_i1 line 811
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_386_i1 line 812
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_386_i1 line 814
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_386_i1 line 818
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_386_i1 line 820
  364. def OAI.SnakyPrototype.Certificate21.checked_386_i1 line 824
  365. def OAI.SnakyPrototype.Certificate21.height_386_i0 line 832
  366. def OAI.SnakyPrototype.Certificate21.childrenH_386_i0 line 833
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_386_i0 line 834
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_386_i0 line 835
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_386_i0 line 837
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_386_i0 line 841
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_386_i0 line 843
  372. def OAI.SnakyPrototype.Certificate21.checked_386_i0 line 847
  373. def OAI.SnakyPrototype.Certificate21.height_386 line 855
  374. def OAI.SnakyPrototype.Certificate21.childrenH_386 line 856
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_386 line 857
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_386 line 858
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_386 line 860
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_386 line 864
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_386 line 866
  380. def OAI.SnakyPrototype.Certificate21.checked_386 line 870
  381. def OAI.SnakyPrototype.Certificate21.height_389_i0 line 878
  382. def OAI.SnakyPrototype.Certificate21.childrenH_389_i0 line 879
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_389_i0 line 880
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_389_i0 line 881
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_389_i0 line 883
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_389_i0 line 887
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_389_i0 line 889
  388. def OAI.SnakyPrototype.Certificate21.checked_389_i0 line 893
  389. def OAI.SnakyPrototype.Certificate21.height_389 line 901
  390. def OAI.SnakyPrototype.Certificate21.childrenH_389 line 902
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_389 line 903
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_389 line 904
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_389 line 906
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_389 line 910
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_389 line 912
  396. def OAI.SnakyPrototype.Certificate21.checked_389 line 916