OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part06.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_652_i3 line 23
  2. def OAI.SnakyPrototype.Certificate21.envelope_652_i3 line 24
  3. def OAI.SnakyPrototype.Certificate21.childrenC_652_i3 line 25
  4. def OAI.SnakyPrototype.Certificate21.childrenD_652_i3 line 26
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_652_i3 line 27
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_652_i3 line 28
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_652_i3 line 29
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_652_i3 line 30
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_652_i3 line 31
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_652_i3 line 36
  11. def OAI.SnakyPrototype.Certificate21.required_652_i2 line 41
  12. def OAI.SnakyPrototype.Certificate21.envelope_652_i2 line 42
  13. def OAI.SnakyPrototype.Certificate21.childrenC_652_i2 line 43
  14. def OAI.SnakyPrototype.Certificate21.childrenD_652_i2 line 44
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_652_i2 line 45
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_652_i2 line 46
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_652_i2 line 47
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_652_i2 line 48
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_652_i2 line 49
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_652_i2 line 55
  21. def OAI.SnakyPrototype.Certificate21.required_652_i1 line 60
  22. def OAI.SnakyPrototype.Certificate21.envelope_652_i1 line 61
  23. def OAI.SnakyPrototype.Certificate21.childrenC_652_i1 line 62
  24. def OAI.SnakyPrototype.Certificate21.childrenD_652_i1 line 63
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_652_i1 line 64
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_652_i1 line 65
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_652_i1 line 66
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_652_i1 line 67
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_652_i1 line 68
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_652_i1 line 73
  31. def OAI.SnakyPrototype.Certificate21.required_652_i0 line 78
  32. def OAI.SnakyPrototype.Certificate21.envelope_652_i0 line 79
  33. def OAI.SnakyPrototype.Certificate21.childrenC_652_i0 line 80
  34. def OAI.SnakyPrototype.Certificate21.childrenD_652_i0 line 81
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_652_i0 line 82
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_652_i0 line 83
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_652_i0 line 84
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_652_i0 line 85
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_652_i0 line 86
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_652_i0 line 92
  41. def OAI.SnakyPrototype.Certificate21.required_652 line 97
  42. def OAI.SnakyPrototype.Certificate21.envelope_652 line 98
  43. def OAI.SnakyPrototype.Certificate21.childrenC_652 line 99
  44. def OAI.SnakyPrototype.Certificate21.childrenD_652 line 100
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_652 line 101
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_652 line 102
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_652 line 103
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_652 line 104
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_652 line 105
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_652 line 110
  51. def OAI.SnakyPrototype.Certificate21.required_674 line 115
  52. def OAI.SnakyPrototype.Certificate21.envelope_674 line 116
  53. def OAI.SnakyPrototype.Certificate21.childrenC_674 line 117
  54. def OAI.SnakyPrototype.Certificate21.childrenD_674 line 118
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_674 line 119
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_674 line 120
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_674 line 121
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_674 line 122
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_674 line 123
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_674 line 129
  61. def OAI.SnakyPrototype.Certificate21.required_702_i1 line 134
  62. def OAI.SnakyPrototype.Certificate21.envelope_702_i1 line 135
  63. def OAI.SnakyPrototype.Certificate21.childrenC_702_i1 line 136
  64. def OAI.SnakyPrototype.Certificate21.childrenD_702_i1 line 137
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_702_i1 line 138
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_702_i1 line 139
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_702_i1 line 140
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_702_i1 line 141
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_702_i1 line 142
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_702_i1 line 147
  71. def OAI.SnakyPrototype.Certificate21.required_702_i0 line 152
  72. def OAI.SnakyPrototype.Certificate21.envelope_702_i0 line 153
  73. def OAI.SnakyPrototype.Certificate21.childrenC_702_i0 line 154
  74. def OAI.SnakyPrototype.Certificate21.childrenD_702_i0 line 155
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_702_i0 line 156
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_702_i0 line 157
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_702_i0 line 158
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_702_i0 line 159
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_702_i0 line 160
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_702_i0 line 167
  81. def OAI.SnakyPrototype.Certificate21.required_702 line 172
  82. def OAI.SnakyPrototype.Certificate21.envelope_702 line 173
  83. def OAI.SnakyPrototype.Certificate21.childrenC_702 line 174
  84. def OAI.SnakyPrototype.Certificate21.childrenD_702 line 175
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_702 line 176
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_702 line 177
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_702 line 178
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_702 line 179
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_702 line 180
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_702 line 186
  91. def OAI.SnakyPrototype.Certificate21.required_704_i1 line 191
  92. def OAI.SnakyPrototype.Certificate21.envelope_704_i1 line 192
  93. def OAI.SnakyPrototype.Certificate21.childrenC_704_i1 line 193
  94. def OAI.SnakyPrototype.Certificate21.childrenD_704_i1 line 194
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_704_i1 line 195
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704_i1 line 196
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704_i1 line 197
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704_i1 line 198
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_704_i1 line 199
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_704_i1 line 205
  101. def OAI.SnakyPrototype.Certificate21.required_704_i3 line 210
  102. def OAI.SnakyPrototype.Certificate21.envelope_704_i3 line 211
  103. def OAI.SnakyPrototype.Certificate21.childrenC_704_i3 line 212
  104. def OAI.SnakyPrototype.Certificate21.childrenD_704_i3 line 213
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_704_i3 line 214
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704_i3 line 215
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704_i3 line 216
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704_i3 line 217
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_704_i3 line 218
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_704_i3 line 223
  111. def OAI.SnakyPrototype.Certificate21.required_704_i4 line 228
  112. def OAI.SnakyPrototype.Certificate21.envelope_704_i4 line 229
  113. def OAI.SnakyPrototype.Certificate21.childrenC_704_i4 line 230
  114. def OAI.SnakyPrototype.Certificate21.childrenD_704_i4 line 231
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_704_i4 line 232
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704_i4 line 233
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704_i4 line 234
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704_i4 line 235
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_704_i4 line 236
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_704_i4 line 241
  121. def OAI.SnakyPrototype.Certificate21.required_704_i5 line 246
  122. def OAI.SnakyPrototype.Certificate21.envelope_704_i5 line 247
  123. def OAI.SnakyPrototype.Certificate21.childrenC_704_i5 line 248
  124. def OAI.SnakyPrototype.Certificate21.childrenD_704_i5 line 249
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_704_i5 line 250
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704_i5 line 251
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704_i5 line 252
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704_i5 line 253
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_704_i5 line 254
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_704_i5 line 259
  131. def OAI.SnakyPrototype.Certificate21.required_704_i2 line 264
  132. def OAI.SnakyPrototype.Certificate21.envelope_704_i2 line 265
  133. def OAI.SnakyPrototype.Certificate21.childrenC_704_i2 line 266
  134. def OAI.SnakyPrototype.Certificate21.childrenD_704_i2 line 267
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_704_i2 line 268
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704_i2 line 269
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704_i2 line 270
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704_i2 line 271
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_704_i2 line 272
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_704_i2 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_704_i0 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_704_i0 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_704_i0 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_704_i0 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_704_i0 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704_i0 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704_i0 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704_i0 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_704_i0 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_704_i0 line 299
  151. def OAI.SnakyPrototype.Certificate21.required_704 line 304
  152. def OAI.SnakyPrototype.Certificate21.envelope_704 line 305
  153. def OAI.SnakyPrototype.Certificate21.childrenC_704 line 306
  154. def OAI.SnakyPrototype.Certificate21.childrenD_704 line 307
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_704 line 308
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_704 line 309
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_704 line 310
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_704 line 311
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_704 line 312
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_704 line 318
  161. def OAI.SnakyPrototype.Certificate21.required_721_i4 line 323
  162. def OAI.SnakyPrototype.Certificate21.envelope_721_i4 line 324
  163. def OAI.SnakyPrototype.Certificate21.childrenC_721_i4 line 325
  164. def OAI.SnakyPrototype.Certificate21.childrenD_721_i4 line 326
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_721_i4 line 327
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_721_i4 line 328
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_721_i4 line 329
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_721_i4 line 330
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_721_i4 line 331
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_721_i4 line 336
  171. def OAI.SnakyPrototype.Certificate21.required_721_i3 line 341
  172. def OAI.SnakyPrototype.Certificate21.envelope_721_i3 line 342
  173. def OAI.SnakyPrototype.Certificate21.childrenC_721_i3 line 343
  174. def OAI.SnakyPrototype.Certificate21.childrenD_721_i3 line 344
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_721_i3 line 345
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_721_i3 line 346
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_721_i3 line 347
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_721_i3 line 348
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_721_i3 line 349
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_721_i3 line 354
  181. def OAI.SnakyPrototype.Certificate21.required_721_i2 line 359
  182. def OAI.SnakyPrototype.Certificate21.envelope_721_i2 line 360
  183. def OAI.SnakyPrototype.Certificate21.childrenC_721_i2 line 361
  184. def OAI.SnakyPrototype.Certificate21.childrenD_721_i2 line 362
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_721_i2 line 363
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_721_i2 line 364
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_721_i2 line 365
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_721_i2 line 366
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_721_i2 line 367
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_721_i2 line 372
  191. def OAI.SnakyPrototype.Certificate21.required_721_i1 line 377
  192. def OAI.SnakyPrototype.Certificate21.envelope_721_i1 line 378
  193. def OAI.SnakyPrototype.Certificate21.childrenC_721_i1 line 379
  194. def OAI.SnakyPrototype.Certificate21.childrenD_721_i1 line 380
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_721_i1 line 381
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_721_i1 line 382
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_721_i1 line 383
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_721_i1 line 384
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_721_i1 line 385
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_721_i1 line 390
  201. def OAI.SnakyPrototype.Certificate21.required_721_i0 line 395
  202. def OAI.SnakyPrototype.Certificate21.envelope_721_i0 line 396
  203. def OAI.SnakyPrototype.Certificate21.childrenC_721_i0 line 397
  204. def OAI.SnakyPrototype.Certificate21.childrenD_721_i0 line 398
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_721_i0 line 399
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_721_i0 line 400
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_721_i0 line 401
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_721_i0 line 402
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_721_i0 line 403
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_721_i0 line 409
  211. def OAI.SnakyPrototype.Certificate21.required_721 line 414
  212. def OAI.SnakyPrototype.Certificate21.envelope_721 line 415
  213. def OAI.SnakyPrototype.Certificate21.childrenC_721 line 416
  214. def OAI.SnakyPrototype.Certificate21.childrenD_721 line 417
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_721 line 418
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_721 line 419
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_721 line 420
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_721 line 421
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_721 line 422
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_721 line 430
  221. def OAI.SnakyPrototype.Certificate21.height_652_i3 line 435
  222. def OAI.SnakyPrototype.Certificate21.childrenH_652_i3 line 436
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_652_i3 line 437
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_652_i3 line 438
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_652_i3 line 440
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_652_i3 line 444
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_652_i3 line 446
  228. def OAI.SnakyPrototype.Certificate21.checked_652_i3 line 450
  229. def OAI.SnakyPrototype.Certificate21.height_652_i2 line 458
  230. def OAI.SnakyPrototype.Certificate21.childrenH_652_i2 line 459
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_652_i2 line 460
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_652_i2 line 461
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_652_i2 line 463
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_652_i2 line 467
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_652_i2 line 469
  236. def OAI.SnakyPrototype.Certificate21.checked_652_i2 line 473
  237. def OAI.SnakyPrototype.Certificate21.height_652_i1 line 481
  238. def OAI.SnakyPrototype.Certificate21.childrenH_652_i1 line 482
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_652_i1 line 483
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_652_i1 line 484
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_652_i1 line 486
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_652_i1 line 490
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_652_i1 line 492
  244. def OAI.SnakyPrototype.Certificate21.checked_652_i1 line 496
  245. def OAI.SnakyPrototype.Certificate21.height_652_i0 line 504
  246. def OAI.SnakyPrototype.Certificate21.childrenH_652_i0 line 505
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_652_i0 line 506
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_652_i0 line 507
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_652_i0 line 509
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_652_i0 line 513
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_652_i0 line 515
  252. def OAI.SnakyPrototype.Certificate21.checked_652_i0 line 519
  253. def OAI.SnakyPrototype.Certificate21.height_652 line 527
  254. def OAI.SnakyPrototype.Certificate21.childrenH_652 line 528
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_652 line 529
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_652 line 530
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_652 line 532
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_652 line 536
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_652 line 538
  260. def OAI.SnakyPrototype.Certificate21.checked_652 line 542
  261. def OAI.SnakyPrototype.Certificate21.height_674 line 550
  262. def OAI.SnakyPrototype.Certificate21.childrenH_674 line 551
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_674 line 552
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_674 line 553
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_674 line 555
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_674 line 559
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_674 line 561
  268. def OAI.SnakyPrototype.Certificate21.checked_674 line 565
  269. def OAI.SnakyPrototype.Certificate21.height_702_i1 line 573
  270. def OAI.SnakyPrototype.Certificate21.childrenH_702_i1 line 574
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_702_i1 line 575
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_702_i1 line 576
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_702_i1 line 578
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_702_i1 line 582
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_702_i1 line 584
  276. def OAI.SnakyPrototype.Certificate21.checked_702_i1 line 588
  277. def OAI.SnakyPrototype.Certificate21.height_702_i0 line 596
  278. def OAI.SnakyPrototype.Certificate21.childrenH_702_i0 line 597
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_702_i0 line 598
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_702_i0 line 599
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_702_i0 line 601
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_702_i0 line 605
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_702_i0 line 607
  284. def OAI.SnakyPrototype.Certificate21.checked_702_i0 line 611
  285. def OAI.SnakyPrototype.Certificate21.height_702 line 619
  286. def OAI.SnakyPrototype.Certificate21.childrenH_702 line 620
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_702 line 621
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_702 line 622
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_702 line 624
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_702 line 628
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_702 line 630
  292. def OAI.SnakyPrototype.Certificate21.checked_702 line 634
  293. def OAI.SnakyPrototype.Certificate21.height_704_i1 line 642
  294. def OAI.SnakyPrototype.Certificate21.childrenH_704_i1 line 643
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_704_i1 line 644
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_704_i1 line 645
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_704_i1 line 647
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704_i1 line 651
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704_i1 line 653
  300. def OAI.SnakyPrototype.Certificate21.checked_704_i1 line 657
  301. def OAI.SnakyPrototype.Certificate21.height_704_i3 line 665
  302. def OAI.SnakyPrototype.Certificate21.childrenH_704_i3 line 666
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_704_i3 line 667
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_704_i3 line 668
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_704_i3 line 670
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704_i3 line 674
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704_i3 line 676
  308. def OAI.SnakyPrototype.Certificate21.checked_704_i3 line 680
  309. def OAI.SnakyPrototype.Certificate21.height_704_i4 line 688
  310. def OAI.SnakyPrototype.Certificate21.childrenH_704_i4 line 689
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_704_i4 line 690
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_704_i4 line 691
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_704_i4 line 693
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704_i4 line 697
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704_i4 line 699
  316. def OAI.SnakyPrototype.Certificate21.checked_704_i4 line 703
  317. def OAI.SnakyPrototype.Certificate21.height_704_i5 line 711
  318. def OAI.SnakyPrototype.Certificate21.childrenH_704_i5 line 712
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_704_i5 line 713
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_704_i5 line 714
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_704_i5 line 716
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704_i5 line 720
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704_i5 line 722
  324. def OAI.SnakyPrototype.Certificate21.checked_704_i5 line 726
  325. def OAI.SnakyPrototype.Certificate21.height_704_i2 line 734
  326. def OAI.SnakyPrototype.Certificate21.childrenH_704_i2 line 735
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_704_i2 line 736
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_704_i2 line 737
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_704_i2 line 739
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704_i2 line 743
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704_i2 line 745
  332. def OAI.SnakyPrototype.Certificate21.checked_704_i2 line 749
  333. def OAI.SnakyPrototype.Certificate21.height_704_i0 line 757
  334. def OAI.SnakyPrototype.Certificate21.childrenH_704_i0 line 758
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_704_i0 line 759
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_704_i0 line 760
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_704_i0 line 762
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704_i0 line 766
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704_i0 line 768
  340. def OAI.SnakyPrototype.Certificate21.checked_704_i0 line 772
  341. def OAI.SnakyPrototype.Certificate21.height_704 line 780
  342. def OAI.SnakyPrototype.Certificate21.childrenH_704 line 781
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_704 line 782
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_704 line 783
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_704 line 785
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_704 line 789
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_704 line 791
  348. def OAI.SnakyPrototype.Certificate21.checked_704 line 795
  349. def OAI.SnakyPrototype.Certificate21.height_721_i4 line 803
  350. def OAI.SnakyPrototype.Certificate21.childrenH_721_i4 line 804
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_721_i4 line 805
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_721_i4 line 806
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_721_i4 line 808
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_721_i4 line 812
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_721_i4 line 814
  356. def OAI.SnakyPrototype.Certificate21.checked_721_i4 line 818
  357. def OAI.SnakyPrototype.Certificate21.height_721_i3 line 826
  358. def OAI.SnakyPrototype.Certificate21.childrenH_721_i3 line 827
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_721_i3 line 828
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_721_i3 line 829
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_721_i3 line 831
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_721_i3 line 835
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_721_i3 line 837
  364. def OAI.SnakyPrototype.Certificate21.checked_721_i3 line 841
  365. def OAI.SnakyPrototype.Certificate21.height_721_i2 line 849
  366. def OAI.SnakyPrototype.Certificate21.childrenH_721_i2 line 850
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_721_i2 line 851
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_721_i2 line 852
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_721_i2 line 854
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_721_i2 line 858
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_721_i2 line 860
  372. def OAI.SnakyPrototype.Certificate21.checked_721_i2 line 864
  373. def OAI.SnakyPrototype.Certificate21.height_721_i1 line 872
  374. def OAI.SnakyPrototype.Certificate21.childrenH_721_i1 line 873
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_721_i1 line 874
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_721_i1 line 875
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_721_i1 line 877
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_721_i1 line 881
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_721_i1 line 883
  380. def OAI.SnakyPrototype.Certificate21.checked_721_i1 line 887
  381. def OAI.SnakyPrototype.Certificate21.height_721_i0 line 895
  382. def OAI.SnakyPrototype.Certificate21.childrenH_721_i0 line 896
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_721_i0 line 897
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_721_i0 line 898
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_721_i0 line 900
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_721_i0 line 904
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_721_i0 line 906
  388. def OAI.SnakyPrototype.Certificate21.checked_721_i0 line 910
  389. def OAI.SnakyPrototype.Certificate21.height_721 line 918
  390. def OAI.SnakyPrototype.Certificate21.childrenH_721 line 919
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_721 line 920
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_721 line 921
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_721 line 923
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_721 line 927
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_721 line 929
  396. def OAI.SnakyPrototype.Certificate21.checked_721 line 933