OAI/GameTheory/SnakyTwentyOne/Cards/Height08Part05.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_658_i0 line 23
  2. def OAI.SnakyPrototype.Certificate21.envelope_658_i0 line 24
  3. def OAI.SnakyPrototype.Certificate21.childrenC_658_i0 line 25
  4. def OAI.SnakyPrototype.Certificate21.childrenD_658_i0 line 26
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_658_i0 line 27
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_658_i0 line 28
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_658_i0 line 29
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_658_i0 line 30
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_658_i0 line 31
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_658_i0 line 36
  11. def OAI.SnakyPrototype.Certificate21.required_658 line 41
  12. def OAI.SnakyPrototype.Certificate21.envelope_658 line 42
  13. def OAI.SnakyPrototype.Certificate21.childrenC_658 line 43
  14. def OAI.SnakyPrototype.Certificate21.childrenD_658 line 44
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_658 line 45
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_658 line 46
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_658 line 47
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_658 line 48
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_658 line 49
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_658 line 56
  21. def OAI.SnakyPrototype.Certificate21.required_661_i0 line 61
  22. def OAI.SnakyPrototype.Certificate21.envelope_661_i0 line 62
  23. def OAI.SnakyPrototype.Certificate21.childrenC_661_i0 line 63
  24. def OAI.SnakyPrototype.Certificate21.childrenD_661_i0 line 64
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_661_i0 line 65
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_661_i0 line 66
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_661_i0 line 67
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_661_i0 line 68
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_661_i0 line 69
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_661_i0 line 76
  31. def OAI.SnakyPrototype.Certificate21.required_661 line 81
  32. def OAI.SnakyPrototype.Certificate21.envelope_661 line 82
  33. def OAI.SnakyPrototype.Certificate21.childrenC_661 line 83
  34. def OAI.SnakyPrototype.Certificate21.childrenD_661 line 84
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_661 line 85
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_661 line 86
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_661 line 87
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_661 line 88
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_661 line 89
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_661 line 97
  41. def OAI.SnakyPrototype.Certificate21.required_666_i1 line 102
  42. def OAI.SnakyPrototype.Certificate21.envelope_666_i1 line 103
  43. def OAI.SnakyPrototype.Certificate21.childrenC_666_i1 line 104
  44. def OAI.SnakyPrototype.Certificate21.childrenD_666_i1 line 105
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_666_i1 line 106
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_666_i1 line 107
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_666_i1 line 108
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_666_i1 line 109
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_666_i1 line 110
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_666_i1 line 115
  51. def OAI.SnakyPrototype.Certificate21.required_666_i0 line 120
  52. def OAI.SnakyPrototype.Certificate21.envelope_666_i0 line 121
  53. def OAI.SnakyPrototype.Certificate21.childrenC_666_i0 line 122
  54. def OAI.SnakyPrototype.Certificate21.childrenD_666_i0 line 123
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_666_i0 line 124
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_666_i0 line 125
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_666_i0 line 126
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_666_i0 line 127
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_666_i0 line 128
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_666_i0 line 133
  61. def OAI.SnakyPrototype.Certificate21.required_666 line 138
  62. def OAI.SnakyPrototype.Certificate21.envelope_666 line 139
  63. def OAI.SnakyPrototype.Certificate21.childrenC_666 line 140
  64. def OAI.SnakyPrototype.Certificate21.childrenD_666 line 141
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_666 line 142
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_666 line 143
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_666 line 144
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_666 line 145
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_666 line 146
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_666 line 151
  71. def OAI.SnakyPrototype.Certificate21.required_678_i1 line 156
  72. def OAI.SnakyPrototype.Certificate21.envelope_678_i1 line 157
  73. def OAI.SnakyPrototype.Certificate21.childrenC_678_i1 line 158
  74. def OAI.SnakyPrototype.Certificate21.childrenD_678_i1 line 159
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_678_i1 line 160
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_678_i1 line 161
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_678_i1 line 162
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_678_i1 line 163
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_678_i1 line 164
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_678_i1 line 169
  81. def OAI.SnakyPrototype.Certificate21.required_678_i0 line 174
  82. def OAI.SnakyPrototype.Certificate21.envelope_678_i0 line 175
  83. def OAI.SnakyPrototype.Certificate21.childrenC_678_i0 line 176
  84. def OAI.SnakyPrototype.Certificate21.childrenD_678_i0 line 177
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_678_i0 line 178
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_678_i0 line 179
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_678_i0 line 180
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_678_i0 line 181
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_678_i0 line 182
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_678_i0 line 187
  91. def OAI.SnakyPrototype.Certificate21.required_678 line 192
  92. def OAI.SnakyPrototype.Certificate21.envelope_678 line 193
  93. def OAI.SnakyPrototype.Certificate21.childrenC_678 line 194
  94. def OAI.SnakyPrototype.Certificate21.childrenD_678 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_678 line 196
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_678 line 197
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_678 line 198
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_678 line 199
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_678 line 200
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_678 line 206
  101. def OAI.SnakyPrototype.Certificate21.required_703_i1 line 211
  102. def OAI.SnakyPrototype.Certificate21.envelope_703_i1 line 212
  103. def OAI.SnakyPrototype.Certificate21.childrenC_703_i1 line 213
  104. def OAI.SnakyPrototype.Certificate21.childrenD_703_i1 line 214
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i1 line 215
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i1 line 216
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i1 line 217
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i1 line 218
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i1 line 219
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i1 line 224
  111. def OAI.SnakyPrototype.Certificate21.required_703_i2 line 229
  112. def OAI.SnakyPrototype.Certificate21.envelope_703_i2 line 230
  113. def OAI.SnakyPrototype.Certificate21.childrenC_703_i2 line 231
  114. def OAI.SnakyPrototype.Certificate21.childrenD_703_i2 line 232
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i2 line 233
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i2 line 234
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i2 line 235
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i2 line 236
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i2 line 237
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i2 line 242
  121. def OAI.SnakyPrototype.Certificate21.required_703_i3 line 247
  122. def OAI.SnakyPrototype.Certificate21.envelope_703_i3 line 248
  123. def OAI.SnakyPrototype.Certificate21.childrenC_703_i3 line 249
  124. def OAI.SnakyPrototype.Certificate21.childrenD_703_i3 line 250
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i3 line 251
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i3 line 252
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i3 line 253
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i3 line 254
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i3 line 255
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i3 line 260
  131. def OAI.SnakyPrototype.Certificate21.required_703_i0 line 265
  132. def OAI.SnakyPrototype.Certificate21.envelope_703_i0 line 266
  133. def OAI.SnakyPrototype.Certificate21.childrenC_703_i0 line 267
  134. def OAI.SnakyPrototype.Certificate21.childrenD_703_i0 line 268
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i0 line 269
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i0 line 270
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i0 line 271
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i0 line 272
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i0 line 273
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i0 line 280
  141. def OAI.SnakyPrototype.Certificate21.required_703_i7 line 285
  142. def OAI.SnakyPrototype.Certificate21.envelope_703_i7 line 286
  143. def OAI.SnakyPrototype.Certificate21.childrenC_703_i7 line 287
  144. def OAI.SnakyPrototype.Certificate21.childrenD_703_i7 line 288
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i7 line 289
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i7 line 290
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i7 line 291
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i7 line 292
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i7 line 293
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i7 line 299
  151. def OAI.SnakyPrototype.Certificate21.required_703_i6 line 304
  152. def OAI.SnakyPrototype.Certificate21.envelope_703_i6 line 305
  153. def OAI.SnakyPrototype.Certificate21.childrenC_703_i6 line 306
  154. def OAI.SnakyPrototype.Certificate21.childrenD_703_i6 line 307
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i6 line 308
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i6 line 309
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i6 line 310
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i6 line 311
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i6 line 312
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i6 line 317
  161. def OAI.SnakyPrototype.Certificate21.required_703_i5 line 322
  162. def OAI.SnakyPrototype.Certificate21.envelope_703_i5 line 323
  163. def OAI.SnakyPrototype.Certificate21.childrenC_703_i5 line 324
  164. def OAI.SnakyPrototype.Certificate21.childrenD_703_i5 line 325
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i5 line 326
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i5 line 327
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i5 line 328
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i5 line 329
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i5 line 330
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i5 line 335
  171. def OAI.SnakyPrototype.Certificate21.required_703_i4 line 340
  172. def OAI.SnakyPrototype.Certificate21.envelope_703_i4 line 341
  173. def OAI.SnakyPrototype.Certificate21.childrenC_703_i4 line 342
  174. def OAI.SnakyPrototype.Certificate21.childrenD_703_i4 line 343
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i4 line 344
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i4 line 345
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i4 line 346
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i4 line 347
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i4 line 348
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i4 line 354
  181. def OAI.SnakyPrototype.Certificate21.required_703_i9 line 359
  182. def OAI.SnakyPrototype.Certificate21.envelope_703_i9 line 360
  183. def OAI.SnakyPrototype.Certificate21.childrenC_703_i9 line 361
  184. def OAI.SnakyPrototype.Certificate21.childrenD_703_i9 line 362
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i9 line 363
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i9 line 364
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i9 line 365
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i9 line 366
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i9 line 367
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i9 line 372
  191. def OAI.SnakyPrototype.Certificate21.required_703_i8 line 377
  192. def OAI.SnakyPrototype.Certificate21.envelope_703_i8 line 378
  193. def OAI.SnakyPrototype.Certificate21.childrenC_703_i8 line 379
  194. def OAI.SnakyPrototype.Certificate21.childrenD_703_i8 line 380
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_703_i8 line 381
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703_i8 line 382
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703_i8 line 383
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703_i8 line 384
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_703_i8 line 385
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_703_i8 line 392
  201. def OAI.SnakyPrototype.Certificate21.required_703 line 397
  202. def OAI.SnakyPrototype.Certificate21.envelope_703 line 398
  203. def OAI.SnakyPrototype.Certificate21.childrenC_703 line 399
  204. def OAI.SnakyPrototype.Certificate21.childrenD_703 line 400
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_703 line 401
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_703 line 402
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_703 line 403
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_703 line 404
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_703 line 405
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_703 line 414
  211. def OAI.SnakyPrototype.Certificate21.height_658_i0 line 419
  212. def OAI.SnakyPrototype.Certificate21.childrenH_658_i0 line 420
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_658_i0 line 421
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_658_i0 line 422
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_658_i0 line 424
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_658_i0 line 428
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_658_i0 line 430
  218. def OAI.SnakyPrototype.Certificate21.checked_658_i0 line 434
  219. def OAI.SnakyPrototype.Certificate21.height_658 line 442
  220. def OAI.SnakyPrototype.Certificate21.childrenH_658 line 443
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_658 line 444
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_658 line 445
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_658 line 447
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_658 line 451
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_658 line 453
  226. def OAI.SnakyPrototype.Certificate21.checked_658 line 457
  227. def OAI.SnakyPrototype.Certificate21.height_661_i0 line 465
  228. def OAI.SnakyPrototype.Certificate21.childrenH_661_i0 line 466
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_661_i0 line 467
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_661_i0 line 468
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_661_i0 line 470
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_661_i0 line 474
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_661_i0 line 476
  234. def OAI.SnakyPrototype.Certificate21.checked_661_i0 line 480
  235. def OAI.SnakyPrototype.Certificate21.height_661 line 488
  236. def OAI.SnakyPrototype.Certificate21.childrenH_661 line 489
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_661 line 490
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_661 line 491
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_661 line 493
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_661 line 497
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_661 line 499
  242. def OAI.SnakyPrototype.Certificate21.checked_661 line 503
  243. def OAI.SnakyPrototype.Certificate21.height_666_i1 line 511
  244. def OAI.SnakyPrototype.Certificate21.childrenH_666_i1 line 512
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_666_i1 line 513
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_666_i1 line 514
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_666_i1 line 516
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_666_i1 line 520
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_666_i1 line 522
  250. def OAI.SnakyPrototype.Certificate21.checked_666_i1 line 526
  251. def OAI.SnakyPrototype.Certificate21.height_666_i0 line 534
  252. def OAI.SnakyPrototype.Certificate21.childrenH_666_i0 line 535
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_666_i0 line 536
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_666_i0 line 537
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_666_i0 line 539
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_666_i0 line 543
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_666_i0 line 545
  258. def OAI.SnakyPrototype.Certificate21.checked_666_i0 line 549
  259. def OAI.SnakyPrototype.Certificate21.height_666 line 557
  260. def OAI.SnakyPrototype.Certificate21.childrenH_666 line 558
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_666 line 559
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_666 line 560
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_666 line 562
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_666 line 566
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_666 line 568
  266. def OAI.SnakyPrototype.Certificate21.checked_666 line 572
  267. def OAI.SnakyPrototype.Certificate21.height_678_i1 line 580
  268. def OAI.SnakyPrototype.Certificate21.childrenH_678_i1 line 581
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_678_i1 line 582
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_678_i1 line 583
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_678_i1 line 585
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_678_i1 line 589
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_678_i1 line 591
  274. def OAI.SnakyPrototype.Certificate21.checked_678_i1 line 595
  275. def OAI.SnakyPrototype.Certificate21.height_678_i0 line 603
  276. def OAI.SnakyPrototype.Certificate21.childrenH_678_i0 line 604
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_678_i0 line 605
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_678_i0 line 606
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_678_i0 line 608
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_678_i0 line 612
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_678_i0 line 614
  282. def OAI.SnakyPrototype.Certificate21.checked_678_i0 line 618
  283. def OAI.SnakyPrototype.Certificate21.height_678 line 626
  284. def OAI.SnakyPrototype.Certificate21.childrenH_678 line 627
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_678 line 628
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_678 line 629
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_678 line 631
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_678 line 635
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_678 line 637
  290. def OAI.SnakyPrototype.Certificate21.checked_678 line 641
  291. def OAI.SnakyPrototype.Certificate21.height_703_i1 line 649
  292. def OAI.SnakyPrototype.Certificate21.childrenH_703_i1 line 650
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i1 line 651
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i1 line 652
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i1 line 654
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i1 line 658
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i1 line 660
  298. def OAI.SnakyPrototype.Certificate21.checked_703_i1 line 664
  299. def OAI.SnakyPrototype.Certificate21.height_703_i2 line 672
  300. def OAI.SnakyPrototype.Certificate21.childrenH_703_i2 line 673
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i2 line 674
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i2 line 675
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i2 line 677
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i2 line 681
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i2 line 683
  306. def OAI.SnakyPrototype.Certificate21.checked_703_i2 line 687
  307. def OAI.SnakyPrototype.Certificate21.height_703_i3 line 695
  308. def OAI.SnakyPrototype.Certificate21.childrenH_703_i3 line 696
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i3 line 697
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i3 line 698
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i3 line 700
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i3 line 704
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i3 line 706
  314. def OAI.SnakyPrototype.Certificate21.checked_703_i3 line 710
  315. def OAI.SnakyPrototype.Certificate21.height_703_i0 line 718
  316. def OAI.SnakyPrototype.Certificate21.childrenH_703_i0 line 719
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i0 line 720
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i0 line 721
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i0 line 723
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i0 line 727
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i0 line 729
  322. def OAI.SnakyPrototype.Certificate21.checked_703_i0 line 733
  323. def OAI.SnakyPrototype.Certificate21.height_703_i7 line 741
  324. def OAI.SnakyPrototype.Certificate21.childrenH_703_i7 line 742
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i7 line 743
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i7 line 744
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i7 line 746
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i7 line 750
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i7 line 752
  330. def OAI.SnakyPrototype.Certificate21.checked_703_i7 line 756
  331. def OAI.SnakyPrototype.Certificate21.height_703_i6 line 764
  332. def OAI.SnakyPrototype.Certificate21.childrenH_703_i6 line 765
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i6 line 766
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i6 line 767
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i6 line 769
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i6 line 773
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i6 line 775
  338. def OAI.SnakyPrototype.Certificate21.checked_703_i6 line 779
  339. def OAI.SnakyPrototype.Certificate21.height_703_i5 line 787
  340. def OAI.SnakyPrototype.Certificate21.childrenH_703_i5 line 788
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i5 line 789
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i5 line 790
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i5 line 792
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i5 line 796
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i5 line 798
  346. def OAI.SnakyPrototype.Certificate21.checked_703_i5 line 802
  347. def OAI.SnakyPrototype.Certificate21.height_703_i4 line 810
  348. def OAI.SnakyPrototype.Certificate21.childrenH_703_i4 line 811
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i4 line 812
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i4 line 813
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i4 line 815
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i4 line 819
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i4 line 821
  354. def OAI.SnakyPrototype.Certificate21.checked_703_i4 line 825
  355. def OAI.SnakyPrototype.Certificate21.height_703_i9 line 833
  356. def OAI.SnakyPrototype.Certificate21.childrenH_703_i9 line 834
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i9 line 835
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i9 line 836
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i9 line 838
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i9 line 842
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i9 line 844
  362. def OAI.SnakyPrototype.Certificate21.checked_703_i9 line 848
  363. def OAI.SnakyPrototype.Certificate21.height_703_i8 line 856
  364. def OAI.SnakyPrototype.Certificate21.childrenH_703_i8 line 857
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_703_i8 line 858
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_703_i8 line 859
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_703_i8 line 861
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703_i8 line 865
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703_i8 line 867
  370. def OAI.SnakyPrototype.Certificate21.checked_703_i8 line 871
  371. def OAI.SnakyPrototype.Certificate21.height_703 line 879
  372. def OAI.SnakyPrototype.Certificate21.childrenH_703 line 880
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_703 line 881
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_703 line 882
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_703 line 884
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_703 line 888
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_703 line 890
  378. def OAI.SnakyPrototype.Certificate21.checked_703 line 894