OAI/GameTheory/SnakyTwentyOne/Cards/Height12Part02.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_551_i7 line 24
  2. def OAI.SnakyPrototype.Certificate21.envelope_551_i7 line 25
  3. def OAI.SnakyPrototype.Certificate21.childrenC_551_i7 line 26
  4. def OAI.SnakyPrototype.Certificate21.childrenD_551_i7 line 27
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i7 line 28
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i7 line 29
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i7 line 30
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i7 line 31
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i7 line 32
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i7 line 37
  11. def OAI.SnakyPrototype.Certificate21.required_551_i8 line 42
  12. def OAI.SnakyPrototype.Certificate21.envelope_551_i8 line 43
  13. def OAI.SnakyPrototype.Certificate21.childrenC_551_i8 line 44
  14. def OAI.SnakyPrototype.Certificate21.childrenD_551_i8 line 45
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i8 line 46
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i8 line 47
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i8 line 48
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i8 line 49
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i8 line 50
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i8 line 55
  21. def OAI.SnakyPrototype.Certificate21.required_551_i6 line 60
  22. def OAI.SnakyPrototype.Certificate21.envelope_551_i6 line 61
  23. def OAI.SnakyPrototype.Certificate21.childrenC_551_i6 line 62
  24. def OAI.SnakyPrototype.Certificate21.childrenD_551_i6 line 63
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i6 line 64
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i6 line 65
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i6 line 66
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i6 line 67
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i6 line 68
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i6 line 74
  31. def OAI.SnakyPrototype.Certificate21.required_551_i5 line 79
  32. def OAI.SnakyPrototype.Certificate21.envelope_551_i5 line 80
  33. def OAI.SnakyPrototype.Certificate21.childrenC_551_i5 line 81
  34. def OAI.SnakyPrototype.Certificate21.childrenD_551_i5 line 82
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i5 line 83
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i5 line 84
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i5 line 85
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i5 line 86
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i5 line 87
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i5 line 92
  41. def OAI.SnakyPrototype.Certificate21.required_551_i4 line 97
  42. def OAI.SnakyPrototype.Certificate21.envelope_551_i4 line 98
  43. def OAI.SnakyPrototype.Certificate21.childrenC_551_i4 line 99
  44. def OAI.SnakyPrototype.Certificate21.childrenD_551_i4 line 100
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i4 line 101
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i4 line 102
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i4 line 103
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i4 line 104
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i4 line 105
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i4 line 110
  51. def OAI.SnakyPrototype.Certificate21.required_551_i3 line 115
  52. def OAI.SnakyPrototype.Certificate21.envelope_551_i3 line 116
  53. def OAI.SnakyPrototype.Certificate21.childrenC_551_i3 line 117
  54. def OAI.SnakyPrototype.Certificate21.childrenD_551_i3 line 118
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i3 line 119
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i3 line 120
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i3 line 121
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i3 line 122
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i3 line 123
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i3 line 128
  61. def OAI.SnakyPrototype.Certificate21.required_551_i2 line 133
  62. def OAI.SnakyPrototype.Certificate21.envelope_551_i2 line 134
  63. def OAI.SnakyPrototype.Certificate21.childrenC_551_i2 line 135
  64. def OAI.SnakyPrototype.Certificate21.childrenD_551_i2 line 136
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i2 line 137
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i2 line 138
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i2 line 139
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i2 line 140
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i2 line 141
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i2 line 146
  71. def OAI.SnakyPrototype.Certificate21.required_551_i1 line 151
  72. def OAI.SnakyPrototype.Certificate21.envelope_551_i1 line 152
  73. def OAI.SnakyPrototype.Certificate21.childrenC_551_i1 line 153
  74. def OAI.SnakyPrototype.Certificate21.childrenD_551_i1 line 154
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i1 line 155
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i1 line 156
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i1 line 157
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i1 line 158
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i1 line 159
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i1 line 166
  81. def OAI.SnakyPrototype.Certificate21.required_551_i0 line 171
  82. def OAI.SnakyPrototype.Certificate21.envelope_551_i0 line 172
  83. def OAI.SnakyPrototype.Certificate21.childrenC_551_i0 line 173
  84. def OAI.SnakyPrototype.Certificate21.childrenD_551_i0 line 174
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_551_i0 line 175
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551_i0 line 176
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551_i0 line 177
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551_i0 line 178
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_551_i0 line 179
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_551_i0 line 186
  91. def OAI.SnakyPrototype.Certificate21.required_551 line 191
  92. def OAI.SnakyPrototype.Certificate21.envelope_551 line 192
  93. def OAI.SnakyPrototype.Certificate21.childrenC_551 line 193
  94. def OAI.SnakyPrototype.Certificate21.childrenD_551 line 194
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_551 line 195
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_551 line 196
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_551 line 197
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_551 line 198
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_551 line 199
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_551 line 205
  101. def OAI.SnakyPrototype.Certificate21.required_571_i1 line 210
  102. def OAI.SnakyPrototype.Certificate21.envelope_571_i1 line 211
  103. def OAI.SnakyPrototype.Certificate21.childrenC_571_i1 line 212
  104. def OAI.SnakyPrototype.Certificate21.childrenD_571_i1 line 213
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i1 line 214
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i1 line 215
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i1 line 216
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i1 line 217
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i1 line 218
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i1 line 225
  111. def OAI.SnakyPrototype.Certificate21.required_571_i0 line 230
  112. def OAI.SnakyPrototype.Certificate21.envelope_571_i0 line 231
  113. def OAI.SnakyPrototype.Certificate21.childrenC_571_i0 line 232
  114. def OAI.SnakyPrototype.Certificate21.childrenD_571_i0 line 233
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i0 line 234
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i0 line 235
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i0 line 236
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i0 line 237
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i0 line 238
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i0 line 243
  121. def OAI.SnakyPrototype.Certificate21.required_571_i3 line 248
  122. def OAI.SnakyPrototype.Certificate21.envelope_571_i3 line 249
  123. def OAI.SnakyPrototype.Certificate21.childrenC_571_i3 line 250
  124. def OAI.SnakyPrototype.Certificate21.childrenD_571_i3 line 251
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i3 line 252
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i3 line 253
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i3 line 254
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i3 line 255
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i3 line 256
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i3 line 261
  131. def OAI.SnakyPrototype.Certificate21.required_571_i2 line 266
  132. def OAI.SnakyPrototype.Certificate21.envelope_571_i2 line 267
  133. def OAI.SnakyPrototype.Certificate21.childrenC_571_i2 line 268
  134. def OAI.SnakyPrototype.Certificate21.childrenD_571_i2 line 269
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i2 line 270
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i2 line 271
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i2 line 272
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i2 line 273
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i2 line 274
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i2 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_571_i5 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_571_i5 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_571_i5 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_571_i5 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i5 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i5 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i5 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i5 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i5 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i5 line 297
  151. def OAI.SnakyPrototype.Certificate21.required_571_i4 line 302
  152. def OAI.SnakyPrototype.Certificate21.envelope_571_i4 line 303
  153. def OAI.SnakyPrototype.Certificate21.childrenC_571_i4 line 304
  154. def OAI.SnakyPrototype.Certificate21.childrenD_571_i4 line 305
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i4 line 306
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i4 line 307
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i4 line 308
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i4 line 309
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i4 line 310
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i4 line 315
  161. def OAI.SnakyPrototype.Certificate21.required_571_i9 line 320
  162. def OAI.SnakyPrototype.Certificate21.envelope_571_i9 line 321
  163. def OAI.SnakyPrototype.Certificate21.childrenC_571_i9 line 322
  164. def OAI.SnakyPrototype.Certificate21.childrenD_571_i9 line 323
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i9 line 324
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i9 line 325
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i9 line 326
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i9 line 327
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i9 line 328
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i9 line 333
  171. def OAI.SnakyPrototype.Certificate21.required_571_i8 line 338
  172. def OAI.SnakyPrototype.Certificate21.envelope_571_i8 line 339
  173. def OAI.SnakyPrototype.Certificate21.childrenC_571_i8 line 340
  174. def OAI.SnakyPrototype.Certificate21.childrenD_571_i8 line 341
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i8 line 342
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i8 line 343
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i8 line 344
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i8 line 345
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i8 line 346
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i8 line 352
  181. def OAI.SnakyPrototype.Certificate21.required_571_i7 line 357
  182. def OAI.SnakyPrototype.Certificate21.envelope_571_i7 line 358
  183. def OAI.SnakyPrototype.Certificate21.childrenC_571_i7 line 359
  184. def OAI.SnakyPrototype.Certificate21.childrenD_571_i7 line 360
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i7 line 361
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i7 line 362
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i7 line 363
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i7 line 364
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i7 line 365
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i7 line 370
  191. def OAI.SnakyPrototype.Certificate21.required_571_i6 line 375
  192. def OAI.SnakyPrototype.Certificate21.envelope_571_i6 line 376
  193. def OAI.SnakyPrototype.Certificate21.childrenC_571_i6 line 377
  194. def OAI.SnakyPrototype.Certificate21.childrenD_571_i6 line 378
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_571_i6 line 379
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571_i6 line 380
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571_i6 line 381
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571_i6 line 382
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_571_i6 line 383
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_571_i6 line 388
  201. def OAI.SnakyPrototype.Certificate21.required_571 line 393
  202. def OAI.SnakyPrototype.Certificate21.envelope_571 line 394
  203. def OAI.SnakyPrototype.Certificate21.childrenC_571 line 395
  204. def OAI.SnakyPrototype.Certificate21.childrenD_571 line 396
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_571 line 397
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_571 line 398
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_571 line 399
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_571 line 400
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_571 line 401
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_571 line 411
  211. def OAI.SnakyPrototype.Certificate21.required_587 line 416
  212. def OAI.SnakyPrototype.Certificate21.envelope_587 line 417
  213. def OAI.SnakyPrototype.Certificate21.childrenC_587 line 418
  214. def OAI.SnakyPrototype.Certificate21.childrenD_587 line 419
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_587 line 420
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_587 line 421
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_587 line 422
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_587 line 423
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_587 line 424
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_587 line 433
  221. def OAI.SnakyPrototype.Certificate21.required_588 line 438
  222. def OAI.SnakyPrototype.Certificate21.envelope_588 line 439
  223. def OAI.SnakyPrototype.Certificate21.childrenC_588 line 440
  224. def OAI.SnakyPrototype.Certificate21.childrenD_588 line 441
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_588 line 442
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_588 line 443
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_588 line 444
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_588 line 445
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_588 line 446
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_588 line 453
  231. def OAI.SnakyPrototype.Certificate21.height_551_i7 line 458
  232. def OAI.SnakyPrototype.Certificate21.childrenH_551_i7 line 459
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i7 line 460
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i7 line 461
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i7 line 463
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i7 line 467
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i7 line 469
  238. def OAI.SnakyPrototype.Certificate21.checked_551_i7 line 473
  239. def OAI.SnakyPrototype.Certificate21.height_551_i8 line 481
  240. def OAI.SnakyPrototype.Certificate21.childrenH_551_i8 line 482
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i8 line 483
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i8 line 484
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i8 line 486
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i8 line 490
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i8 line 492
  246. def OAI.SnakyPrototype.Certificate21.checked_551_i8 line 496
  247. def OAI.SnakyPrototype.Certificate21.height_551_i6 line 504
  248. def OAI.SnakyPrototype.Certificate21.childrenH_551_i6 line 505
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i6 line 506
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i6 line 507
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i6 line 509
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i6 line 513
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i6 line 515
  254. def OAI.SnakyPrototype.Certificate21.checked_551_i6 line 519
  255. def OAI.SnakyPrototype.Certificate21.height_551_i5 line 527
  256. def OAI.SnakyPrototype.Certificate21.childrenH_551_i5 line 528
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i5 line 529
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i5 line 530
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i5 line 532
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i5 line 536
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i5 line 538
  262. def OAI.SnakyPrototype.Certificate21.checked_551_i5 line 542
  263. def OAI.SnakyPrototype.Certificate21.height_551_i4 line 550
  264. def OAI.SnakyPrototype.Certificate21.childrenH_551_i4 line 551
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i4 line 552
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i4 line 553
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i4 line 555
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i4 line 559
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i4 line 561
  270. def OAI.SnakyPrototype.Certificate21.checked_551_i4 line 565
  271. def OAI.SnakyPrototype.Certificate21.height_551_i3 line 573
  272. def OAI.SnakyPrototype.Certificate21.childrenH_551_i3 line 574
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i3 line 575
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i3 line 576
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i3 line 578
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i3 line 582
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i3 line 584
  278. def OAI.SnakyPrototype.Certificate21.checked_551_i3 line 588
  279. def OAI.SnakyPrototype.Certificate21.height_551_i2 line 596
  280. def OAI.SnakyPrototype.Certificate21.childrenH_551_i2 line 597
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i2 line 598
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i2 line 599
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i2 line 601
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i2 line 605
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i2 line 607
  286. def OAI.SnakyPrototype.Certificate21.checked_551_i2 line 611
  287. def OAI.SnakyPrototype.Certificate21.height_551_i1 line 619
  288. def OAI.SnakyPrototype.Certificate21.childrenH_551_i1 line 620
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i1 line 621
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i1 line 622
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i1 line 624
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i1 line 628
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i1 line 630
  294. def OAI.SnakyPrototype.Certificate21.checked_551_i1 line 634
  295. def OAI.SnakyPrototype.Certificate21.height_551_i0 line 642
  296. def OAI.SnakyPrototype.Certificate21.childrenH_551_i0 line 643
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_551_i0 line 644
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_551_i0 line 645
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_551_i0 line 647
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551_i0 line 651
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551_i0 line 653
  302. def OAI.SnakyPrototype.Certificate21.checked_551_i0 line 657
  303. def OAI.SnakyPrototype.Certificate21.height_551 line 665
  304. def OAI.SnakyPrototype.Certificate21.childrenH_551 line 666
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_551 line 667
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_551 line 668
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_551 line 670
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_551 line 674
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_551 line 676
  310. def OAI.SnakyPrototype.Certificate21.checked_551 line 680
  311. def OAI.SnakyPrototype.Certificate21.height_571_i1 line 688
  312. def OAI.SnakyPrototype.Certificate21.childrenH_571_i1 line 689
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i1 line 690
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i1 line 691
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i1 line 693
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i1 line 697
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i1 line 699
  318. def OAI.SnakyPrototype.Certificate21.checked_571_i1 line 703
  319. def OAI.SnakyPrototype.Certificate21.height_571_i0 line 711
  320. def OAI.SnakyPrototype.Certificate21.childrenH_571_i0 line 712
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i0 line 713
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i0 line 714
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i0 line 716
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i0 line 720
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i0 line 722
  326. def OAI.SnakyPrototype.Certificate21.checked_571_i0 line 726
  327. def OAI.SnakyPrototype.Certificate21.height_571_i3 line 734
  328. def OAI.SnakyPrototype.Certificate21.childrenH_571_i3 line 735
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i3 line 736
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i3 line 737
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i3 line 739
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i3 line 743
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i3 line 745
  334. def OAI.SnakyPrototype.Certificate21.checked_571_i3 line 749
  335. def OAI.SnakyPrototype.Certificate21.height_571_i2 line 757
  336. def OAI.SnakyPrototype.Certificate21.childrenH_571_i2 line 758
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i2 line 759
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i2 line 760
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i2 line 762
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i2 line 766
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i2 line 768
  342. def OAI.SnakyPrototype.Certificate21.checked_571_i2 line 772
  343. def OAI.SnakyPrototype.Certificate21.height_571_i5 line 780
  344. def OAI.SnakyPrototype.Certificate21.childrenH_571_i5 line 781
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i5 line 782
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i5 line 783
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i5 line 785
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i5 line 789
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i5 line 791
  350. def OAI.SnakyPrototype.Certificate21.checked_571_i5 line 795
  351. def OAI.SnakyPrototype.Certificate21.height_571_i4 line 803
  352. def OAI.SnakyPrototype.Certificate21.childrenH_571_i4 line 804
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i4 line 805
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i4 line 806
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i4 line 808
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i4 line 812
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i4 line 814
  358. def OAI.SnakyPrototype.Certificate21.checked_571_i4 line 818
  359. def OAI.SnakyPrototype.Certificate21.height_571_i9 line 826
  360. def OAI.SnakyPrototype.Certificate21.childrenH_571_i9 line 827
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i9 line 828
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i9 line 829
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i9 line 831
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i9 line 835
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i9 line 837
  366. def OAI.SnakyPrototype.Certificate21.checked_571_i9 line 841
  367. def OAI.SnakyPrototype.Certificate21.height_571_i8 line 849
  368. def OAI.SnakyPrototype.Certificate21.childrenH_571_i8 line 850
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i8 line 851
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i8 line 852
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i8 line 854
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i8 line 858
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i8 line 860
  374. def OAI.SnakyPrototype.Certificate21.checked_571_i8 line 864
  375. def OAI.SnakyPrototype.Certificate21.height_571_i7 line 872
  376. def OAI.SnakyPrototype.Certificate21.childrenH_571_i7 line 873
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i7 line 874
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i7 line 875
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i7 line 877
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i7 line 881
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i7 line 883
  382. def OAI.SnakyPrototype.Certificate21.checked_571_i7 line 887
  383. def OAI.SnakyPrototype.Certificate21.height_571_i6 line 895
  384. def OAI.SnakyPrototype.Certificate21.childrenH_571_i6 line 896
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_571_i6 line 897
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_571_i6 line 898
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_571_i6 line 900
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571_i6 line 904
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571_i6 line 906
  390. def OAI.SnakyPrototype.Certificate21.checked_571_i6 line 910
  391. def OAI.SnakyPrototype.Certificate21.height_571 line 918
  392. def OAI.SnakyPrototype.Certificate21.childrenH_571 line 919
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_571 line 920
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_571 line 921
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_571 line 923
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_571 line 927
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_571 line 929
  398. def OAI.SnakyPrototype.Certificate21.checked_571 line 933
  399. def OAI.SnakyPrototype.Certificate21.height_587 line 941
  400. def OAI.SnakyPrototype.Certificate21.childrenH_587 line 942
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_587 line 943
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_587 line 944
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_587 line 946
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_587 line 950
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_587 line 952
  406. def OAI.SnakyPrototype.Certificate21.checked_587 line 956
  407. def OAI.SnakyPrototype.Certificate21.height_588 line 964
  408. def OAI.SnakyPrototype.Certificate21.childrenH_588 line 965
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_588 line 966
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_588 line 967
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_588 line 969
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_588 line 973
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_588 line 975
  414. def OAI.SnakyPrototype.Certificate21.checked_588 line 979