OAI/GameTheory/SnakyTwentyOne/Cards/Height05Part06.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_495_i0 line 18
  2. def OAI.SnakyPrototype.Certificate21.envelope_495_i0 line 19
  3. def OAI.SnakyPrototype.Certificate21.childrenC_495_i0 line 20
  4. def OAI.SnakyPrototype.Certificate21.childrenD_495_i0 line 21
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_495_i0 line 22
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_495_i0 line 23
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_495_i0 line 24
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_495_i0 line 25
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_495_i0 line 26
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_495_i0 line 31
  11. def OAI.SnakyPrototype.Certificate21.required_495 line 36
  12. def OAI.SnakyPrototype.Certificate21.envelope_495 line 37
  13. def OAI.SnakyPrototype.Certificate21.childrenC_495 line 38
  14. def OAI.SnakyPrototype.Certificate21.childrenD_495 line 39
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_495 line 40
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_495 line 41
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_495 line 42
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_495 line 43
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_495 line 44
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_495 line 51
  21. def OAI.SnakyPrototype.Certificate21.required_497 line 56
  22. def OAI.SnakyPrototype.Certificate21.envelope_497 line 57
  23. def OAI.SnakyPrototype.Certificate21.childrenC_497 line 58
  24. def OAI.SnakyPrototype.Certificate21.childrenD_497 line 59
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_497 line 60
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_497 line 61
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_497 line 62
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_497 line 63
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_497 line 64
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_497 line 69
  31. def OAI.SnakyPrototype.Certificate21.required_501 line 74
  32. def OAI.SnakyPrototype.Certificate21.envelope_501 line 75
  33. def OAI.SnakyPrototype.Certificate21.childrenC_501 line 76
  34. def OAI.SnakyPrototype.Certificate21.childrenD_501 line 77
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_501 line 78
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_501 line 79
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_501 line 80
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_501 line 81
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_501 line 82
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_501 line 87
  41. def OAI.SnakyPrototype.Certificate21.required_502_i0 line 92
  42. def OAI.SnakyPrototype.Certificate21.envelope_502_i0 line 93
  43. def OAI.SnakyPrototype.Certificate21.childrenC_502_i0 line 94
  44. def OAI.SnakyPrototype.Certificate21.childrenD_502_i0 line 95
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_502_i0 line 96
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_502_i0 line 97
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_502_i0 line 98
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_502_i0 line 99
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_502_i0 line 100
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_502_i0 line 105
  51. def OAI.SnakyPrototype.Certificate21.required_502 line 110
  52. def OAI.SnakyPrototype.Certificate21.envelope_502 line 111
  53. def OAI.SnakyPrototype.Certificate21.childrenC_502 line 112
  54. def OAI.SnakyPrototype.Certificate21.childrenD_502 line 113
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_502 line 114
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_502 line 115
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_502 line 116
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_502 line 117
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_502 line 118
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_502 line 124
  61. def OAI.SnakyPrototype.Certificate21.required_505_i0 line 129
  62. def OAI.SnakyPrototype.Certificate21.envelope_505_i0 line 130
  63. def OAI.SnakyPrototype.Certificate21.childrenC_505_i0 line 131
  64. def OAI.SnakyPrototype.Certificate21.childrenD_505_i0 line 132
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_505_i0 line 133
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_505_i0 line 134
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_505_i0 line 135
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_505_i0 line 136
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_505_i0 line 137
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_505_i0 line 142
  71. def OAI.SnakyPrototype.Certificate21.required_505_i2 line 147
  72. def OAI.SnakyPrototype.Certificate21.envelope_505_i2 line 148
  73. def OAI.SnakyPrototype.Certificate21.childrenC_505_i2 line 149
  74. def OAI.SnakyPrototype.Certificate21.childrenD_505_i2 line 150
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_505_i2 line 151
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_505_i2 line 152
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_505_i2 line 153
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_505_i2 line 154
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_505_i2 line 155
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_505_i2 line 160
  81. def OAI.SnakyPrototype.Certificate21.required_505_i1 line 165
  82. def OAI.SnakyPrototype.Certificate21.envelope_505_i1 line 166
  83. def OAI.SnakyPrototype.Certificate21.childrenC_505_i1 line 167
  84. def OAI.SnakyPrototype.Certificate21.childrenD_505_i1 line 168
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_505_i1 line 169
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_505_i1 line 170
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_505_i1 line 171
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_505_i1 line 172
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_505_i1 line 173
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_505_i1 line 178
  91. def OAI.SnakyPrototype.Certificate21.required_505 line 183
  92. def OAI.SnakyPrototype.Certificate21.envelope_505 line 184
  93. def OAI.SnakyPrototype.Certificate21.childrenC_505 line 185
  94. def OAI.SnakyPrototype.Certificate21.childrenD_505 line 186
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_505 line 187
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_505 line 188
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_505 line 189
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_505 line 190
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_505 line 191
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_505 line 197
  101. def OAI.SnakyPrototype.Certificate21.required_506_i0 line 202
  102. def OAI.SnakyPrototype.Certificate21.envelope_506_i0 line 203
  103. def OAI.SnakyPrototype.Certificate21.childrenC_506_i0 line 204
  104. def OAI.SnakyPrototype.Certificate21.childrenD_506_i0 line 205
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_506_i0 line 206
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_506_i0 line 207
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_506_i0 line 208
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_506_i0 line 209
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_506_i0 line 210
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_506_i0 line 215
  111. def OAI.SnakyPrototype.Certificate21.required_506 line 220
  112. def OAI.SnakyPrototype.Certificate21.envelope_506 line 221
  113. def OAI.SnakyPrototype.Certificate21.childrenC_506 line 222
  114. def OAI.SnakyPrototype.Certificate21.childrenD_506 line 223
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_506 line 224
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_506 line 225
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_506 line 226
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_506 line 227
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_506 line 228
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_506 line 234
  121. def OAI.SnakyPrototype.Certificate21.required_515_i0 line 239
  122. def OAI.SnakyPrototype.Certificate21.envelope_515_i0 line 240
  123. def OAI.SnakyPrototype.Certificate21.childrenC_515_i0 line 241
  124. def OAI.SnakyPrototype.Certificate21.childrenD_515_i0 line 242
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_515_i0 line 243
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_515_i0 line 244
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_515_i0 line 245
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_515_i0 line 246
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_515_i0 line 247
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_515_i0 line 252
  131. def OAI.SnakyPrototype.Certificate21.required_515 line 257
  132. def OAI.SnakyPrototype.Certificate21.envelope_515 line 258
  133. def OAI.SnakyPrototype.Certificate21.childrenC_515 line 259
  134. def OAI.SnakyPrototype.Certificate21.childrenD_515 line 260
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_515 line 261
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_515 line 262
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_515 line 263
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_515 line 264
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_515 line 265
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_515 line 270
  141. def OAI.SnakyPrototype.Certificate21.required_592_i0 line 275
  142. def OAI.SnakyPrototype.Certificate21.envelope_592_i0 line 276
  143. def OAI.SnakyPrototype.Certificate21.childrenC_592_i0 line 277
  144. def OAI.SnakyPrototype.Certificate21.childrenD_592_i0 line 278
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_592_i0 line 279
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_592_i0 line 280
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_592_i0 line 281
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_592_i0 line 282
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_592_i0 line 283
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_592_i0 line 288
  151. def OAI.SnakyPrototype.Certificate21.required_592 line 293
  152. def OAI.SnakyPrototype.Certificate21.envelope_592 line 294
  153. def OAI.SnakyPrototype.Certificate21.childrenC_592 line 295
  154. def OAI.SnakyPrototype.Certificate21.childrenD_592 line 296
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_592 line 297
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_592 line 298
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_592 line 299
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_592 line 300
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_592 line 301
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_592 line 308
  161. def OAI.SnakyPrototype.Certificate21.required_612_i1 line 313
  162. def OAI.SnakyPrototype.Certificate21.envelope_612_i1 line 314
  163. def OAI.SnakyPrototype.Certificate21.childrenC_612_i1 line 315
  164. def OAI.SnakyPrototype.Certificate21.childrenD_612_i1 line 316
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_612_i1 line 317
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_612_i1 line 318
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_612_i1 line 319
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_612_i1 line 320
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_612_i1 line 321
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_612_i1 line 326
  171. def OAI.SnakyPrototype.Certificate21.required_612_i2 line 331
  172. def OAI.SnakyPrototype.Certificate21.envelope_612_i2 line 332
  173. def OAI.SnakyPrototype.Certificate21.childrenC_612_i2 line 333
  174. def OAI.SnakyPrototype.Certificate21.childrenD_612_i2 line 334
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_612_i2 line 335
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_612_i2 line 336
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_612_i2 line 337
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_612_i2 line 338
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_612_i2 line 339
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_612_i2 line 344
  181. def OAI.SnakyPrototype.Certificate21.required_612_i3 line 349
  182. def OAI.SnakyPrototype.Certificate21.envelope_612_i3 line 350
  183. def OAI.SnakyPrototype.Certificate21.childrenC_612_i3 line 351
  184. def OAI.SnakyPrototype.Certificate21.childrenD_612_i3 line 352
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_612_i3 line 353
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_612_i3 line 354
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_612_i3 line 355
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_612_i3 line 356
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_612_i3 line 357
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_612_i3 line 362
  191. def OAI.SnakyPrototype.Certificate21.required_612_i0 line 367
  192. def OAI.SnakyPrototype.Certificate21.envelope_612_i0 line 368
  193. def OAI.SnakyPrototype.Certificate21.childrenC_612_i0 line 369
  194. def OAI.SnakyPrototype.Certificate21.childrenD_612_i0 line 370
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_612_i0 line 371
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_612_i0 line 372
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_612_i0 line 373
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_612_i0 line 374
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_612_i0 line 375
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_612_i0 line 381
  201. def OAI.SnakyPrototype.Certificate21.required_612 line 386
  202. def OAI.SnakyPrototype.Certificate21.envelope_612 line 387
  203. def OAI.SnakyPrototype.Certificate21.childrenC_612 line 388
  204. def OAI.SnakyPrototype.Certificate21.childrenD_612 line 389
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_612 line 390
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_612 line 391
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_612 line 392
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_612 line 393
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_612 line 394
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_612 line 401
  211. def OAI.SnakyPrototype.Certificate21.required_672_i0 line 406
  212. def OAI.SnakyPrototype.Certificate21.envelope_672_i0 line 407
  213. def OAI.SnakyPrototype.Certificate21.childrenC_672_i0 line 408
  214. def OAI.SnakyPrototype.Certificate21.childrenD_672_i0 line 409
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_672_i0 line 410
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_672_i0 line 411
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_672_i0 line 412
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_672_i0 line 413
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_672_i0 line 414
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_672_i0 line 419
  221. def OAI.SnakyPrototype.Certificate21.required_672 line 424
  222. def OAI.SnakyPrototype.Certificate21.envelope_672 line 425
  223. def OAI.SnakyPrototype.Certificate21.childrenC_672 line 426
  224. def OAI.SnakyPrototype.Certificate21.childrenD_672 line 427
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_672 line 428
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_672 line 429
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_672 line 430
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_672 line 431
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_672 line 432
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_672 line 438
  231. def OAI.SnakyPrototype.Certificate21.height_495_i0 line 443
  232. def OAI.SnakyPrototype.Certificate21.childrenH_495_i0 line 444
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_495_i0 line 445
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_495_i0 line 446
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_495_i0 line 448
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_495_i0 line 452
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_495_i0 line 454
  238. def OAI.SnakyPrototype.Certificate21.checked_495_i0 line 458
  239. def OAI.SnakyPrototype.Certificate21.height_495 line 466
  240. def OAI.SnakyPrototype.Certificate21.childrenH_495 line 467
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_495 line 468
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_495 line 469
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_495 line 471
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_495 line 475
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_495 line 477
  246. def OAI.SnakyPrototype.Certificate21.checked_495 line 481
  247. def OAI.SnakyPrototype.Certificate21.height_497 line 489
  248. def OAI.SnakyPrototype.Certificate21.childrenH_497 line 490
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_497 line 491
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_497 line 492
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_497 line 494
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_497 line 498
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_497 line 500
  254. def OAI.SnakyPrototype.Certificate21.checked_497 line 504
  255. def OAI.SnakyPrototype.Certificate21.height_501 line 512
  256. def OAI.SnakyPrototype.Certificate21.childrenH_501 line 513
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_501 line 514
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_501 line 515
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_501 line 517
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_501 line 521
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_501 line 523
  262. def OAI.SnakyPrototype.Certificate21.checked_501 line 527
  263. def OAI.SnakyPrototype.Certificate21.height_502_i0 line 535
  264. def OAI.SnakyPrototype.Certificate21.childrenH_502_i0 line 536
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_502_i0 line 537
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_502_i0 line 538
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_502_i0 line 540
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_502_i0 line 544
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_502_i0 line 546
  270. def OAI.SnakyPrototype.Certificate21.checked_502_i0 line 550
  271. def OAI.SnakyPrototype.Certificate21.height_502 line 558
  272. def OAI.SnakyPrototype.Certificate21.childrenH_502 line 559
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_502 line 560
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_502 line 561
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_502 line 563
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_502 line 567
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_502 line 569
  278. def OAI.SnakyPrototype.Certificate21.checked_502 line 573
  279. def OAI.SnakyPrototype.Certificate21.height_505_i0 line 581
  280. def OAI.SnakyPrototype.Certificate21.childrenH_505_i0 line 582
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_505_i0 line 583
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_505_i0 line 584
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_505_i0 line 586
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_505_i0 line 590
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_505_i0 line 592
  286. def OAI.SnakyPrototype.Certificate21.checked_505_i0 line 596
  287. def OAI.SnakyPrototype.Certificate21.height_505_i2 line 604
  288. def OAI.SnakyPrototype.Certificate21.childrenH_505_i2 line 605
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_505_i2 line 606
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_505_i2 line 607
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_505_i2 line 609
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_505_i2 line 613
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_505_i2 line 615
  294. def OAI.SnakyPrototype.Certificate21.checked_505_i2 line 619
  295. def OAI.SnakyPrototype.Certificate21.height_505_i1 line 627
  296. def OAI.SnakyPrototype.Certificate21.childrenH_505_i1 line 628
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_505_i1 line 629
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_505_i1 line 630
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_505_i1 line 632
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_505_i1 line 636
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_505_i1 line 638
  302. def OAI.SnakyPrototype.Certificate21.checked_505_i1 line 642
  303. def OAI.SnakyPrototype.Certificate21.height_505 line 650
  304. def OAI.SnakyPrototype.Certificate21.childrenH_505 line 651
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_505 line 652
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_505 line 653
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_505 line 655
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_505 line 659
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_505 line 661
  310. def OAI.SnakyPrototype.Certificate21.checked_505 line 665
  311. def OAI.SnakyPrototype.Certificate21.height_506_i0 line 673
  312. def OAI.SnakyPrototype.Certificate21.childrenH_506_i0 line 674
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_506_i0 line 675
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_506_i0 line 676
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_506_i0 line 678
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_506_i0 line 682
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_506_i0 line 684
  318. def OAI.SnakyPrototype.Certificate21.checked_506_i0 line 688
  319. def OAI.SnakyPrototype.Certificate21.height_506 line 696
  320. def OAI.SnakyPrototype.Certificate21.childrenH_506 line 697
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_506 line 698
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_506 line 699
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_506 line 701
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_506 line 705
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_506 line 707
  326. def OAI.SnakyPrototype.Certificate21.checked_506 line 711
  327. def OAI.SnakyPrototype.Certificate21.height_515_i0 line 719
  328. def OAI.SnakyPrototype.Certificate21.childrenH_515_i0 line 720
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_515_i0 line 721
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_515_i0 line 722
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_515_i0 line 724
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_515_i0 line 728
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_515_i0 line 730
  334. def OAI.SnakyPrototype.Certificate21.checked_515_i0 line 734
  335. def OAI.SnakyPrototype.Certificate21.height_515 line 742
  336. def OAI.SnakyPrototype.Certificate21.childrenH_515 line 743
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_515 line 744
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_515 line 745
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_515 line 747
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_515 line 751
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_515 line 753
  342. def OAI.SnakyPrototype.Certificate21.checked_515 line 757
  343. def OAI.SnakyPrototype.Certificate21.height_592_i0 line 765
  344. def OAI.SnakyPrototype.Certificate21.childrenH_592_i0 line 766
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_592_i0 line 767
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_592_i0 line 768
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_592_i0 line 770
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_592_i0 line 774
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_592_i0 line 776
  350. def OAI.SnakyPrototype.Certificate21.checked_592_i0 line 780
  351. def OAI.SnakyPrototype.Certificate21.height_592 line 788
  352. def OAI.SnakyPrototype.Certificate21.childrenH_592 line 789
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_592 line 790
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_592 line 791
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_592 line 793
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_592 line 797
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_592 line 799
  358. def OAI.SnakyPrototype.Certificate21.checked_592 line 803
  359. def OAI.SnakyPrototype.Certificate21.height_612_i1 line 811
  360. def OAI.SnakyPrototype.Certificate21.childrenH_612_i1 line 812
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_612_i1 line 813
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_612_i1 line 814
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_612_i1 line 816
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_612_i1 line 820
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_612_i1 line 822
  366. def OAI.SnakyPrototype.Certificate21.checked_612_i1 line 826
  367. def OAI.SnakyPrototype.Certificate21.height_612_i2 line 834
  368. def OAI.SnakyPrototype.Certificate21.childrenH_612_i2 line 835
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_612_i2 line 836
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_612_i2 line 837
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_612_i2 line 839
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_612_i2 line 843
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_612_i2 line 845
  374. def OAI.SnakyPrototype.Certificate21.checked_612_i2 line 849
  375. def OAI.SnakyPrototype.Certificate21.height_612_i3 line 857
  376. def OAI.SnakyPrototype.Certificate21.childrenH_612_i3 line 858
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_612_i3 line 859
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_612_i3 line 860
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_612_i3 line 862
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_612_i3 line 866
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_612_i3 line 868
  382. def OAI.SnakyPrototype.Certificate21.checked_612_i3 line 872
  383. def OAI.SnakyPrototype.Certificate21.height_612_i0 line 880
  384. def OAI.SnakyPrototype.Certificate21.childrenH_612_i0 line 881
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_612_i0 line 882
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_612_i0 line 883
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_612_i0 line 885
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_612_i0 line 889
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_612_i0 line 891
  390. def OAI.SnakyPrototype.Certificate21.checked_612_i0 line 895
  391. def OAI.SnakyPrototype.Certificate21.height_612 line 903
  392. def OAI.SnakyPrototype.Certificate21.childrenH_612 line 904
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_612 line 905
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_612 line 906
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_612 line 908
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_612 line 912
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_612 line 914
  398. def OAI.SnakyPrototype.Certificate21.checked_612 line 918
  399. def OAI.SnakyPrototype.Certificate21.height_672_i0 line 926
  400. def OAI.SnakyPrototype.Certificate21.childrenH_672_i0 line 927
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_672_i0 line 928
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_672_i0 line 929
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_672_i0 line 931
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_672_i0 line 935
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_672_i0 line 937
  406. def OAI.SnakyPrototype.Certificate21.checked_672_i0 line 941
  407. def OAI.SnakyPrototype.Certificate21.height_672 line 949
  408. def OAI.SnakyPrototype.Certificate21.childrenH_672 line 950
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_672 line 951
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_672 line 952
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_672 line 954
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_672 line 958
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_672 line 960
  414. def OAI.SnakyPrototype.Certificate21.checked_672 line 964