OAI/GameTheory/SnakyTwentyOne/Cards/Height04Part02.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_67 line 12
  2. def OAI.SnakyPrototype.Certificate21.envelope_67 line 13
  3. def OAI.SnakyPrototype.Certificate21.childrenC_67 line 14
  4. def OAI.SnakyPrototype.Certificate21.childrenD_67 line 15
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_67 line 16
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_67 line 17
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_67 line 18
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_67 line 19
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_67 line 20
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_67 line 25
  11. def OAI.SnakyPrototype.Certificate21.required_73 line 30
  12. def OAI.SnakyPrototype.Certificate21.envelope_73 line 31
  13. def OAI.SnakyPrototype.Certificate21.childrenC_73 line 32
  14. def OAI.SnakyPrototype.Certificate21.childrenD_73 line 33
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_73 line 34
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_73 line 35
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_73 line 36
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_73 line 37
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_73 line 38
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_73 line 43
  21. def OAI.SnakyPrototype.Certificate21.required_75 line 48
  22. def OAI.SnakyPrototype.Certificate21.envelope_75 line 49
  23. def OAI.SnakyPrototype.Certificate21.childrenC_75 line 50
  24. def OAI.SnakyPrototype.Certificate21.childrenD_75 line 51
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_75 line 52
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_75 line 53
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_75 line 54
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_75 line 55
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_75 line 56
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_75 line 61
  31. def OAI.SnakyPrototype.Certificate21.required_79 line 66
  32. def OAI.SnakyPrototype.Certificate21.envelope_79 line 67
  33. def OAI.SnakyPrototype.Certificate21.childrenC_79 line 68
  34. def OAI.SnakyPrototype.Certificate21.childrenD_79 line 69
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_79 line 70
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_79 line 71
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_79 line 72
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_79 line 73
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_79 line 74
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_79 line 79
  41. def OAI.SnakyPrototype.Certificate21.required_82 line 84
  42. def OAI.SnakyPrototype.Certificate21.envelope_82 line 85
  43. def OAI.SnakyPrototype.Certificate21.childrenC_82 line 86
  44. def OAI.SnakyPrototype.Certificate21.childrenD_82 line 87
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_82 line 88
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_82 line 89
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_82 line 90
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_82 line 91
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_82 line 92
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_82 line 97
  51. def OAI.SnakyPrototype.Certificate21.required_86 line 102
  52. def OAI.SnakyPrototype.Certificate21.envelope_86 line 103
  53. def OAI.SnakyPrototype.Certificate21.childrenC_86 line 104
  54. def OAI.SnakyPrototype.Certificate21.childrenD_86 line 105
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_86 line 106
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_86 line 107
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_86 line 108
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_86 line 109
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_86 line 110
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_86 line 115
  61. def OAI.SnakyPrototype.Certificate21.required_88 line 120
  62. def OAI.SnakyPrototype.Certificate21.envelope_88 line 121
  63. def OAI.SnakyPrototype.Certificate21.childrenC_88 line 122
  64. def OAI.SnakyPrototype.Certificate21.childrenD_88 line 123
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_88 line 124
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_88 line 125
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_88 line 126
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_88 line 127
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_88 line 128
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_88 line 133
  71. def OAI.SnakyPrototype.Certificate21.required_89 line 138
  72. def OAI.SnakyPrototype.Certificate21.envelope_89 line 139
  73. def OAI.SnakyPrototype.Certificate21.childrenC_89 line 140
  74. def OAI.SnakyPrototype.Certificate21.childrenD_89 line 141
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_89 line 142
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_89 line 143
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_89 line 144
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_89 line 145
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_89 line 146
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_89 line 151
  81. def OAI.SnakyPrototype.Certificate21.required_90 line 156
  82. def OAI.SnakyPrototype.Certificate21.envelope_90 line 157
  83. def OAI.SnakyPrototype.Certificate21.childrenC_90 line 158
  84. def OAI.SnakyPrototype.Certificate21.childrenD_90 line 159
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_90 line 160
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_90 line 161
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_90 line 162
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_90 line 163
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_90 line 164
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_90 line 169
  91. def OAI.SnakyPrototype.Certificate21.required_91 line 174
  92. def OAI.SnakyPrototype.Certificate21.envelope_91 line 175
  93. def OAI.SnakyPrototype.Certificate21.childrenC_91 line 176
  94. def OAI.SnakyPrototype.Certificate21.childrenD_91 line 177
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_91 line 178
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_91 line 179
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_91 line 180
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_91 line 181
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_91 line 182
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_91 line 187
  101. def OAI.SnakyPrototype.Certificate21.required_92 line 192
  102. def OAI.SnakyPrototype.Certificate21.envelope_92 line 193
  103. def OAI.SnakyPrototype.Certificate21.childrenC_92 line 194
  104. def OAI.SnakyPrototype.Certificate21.childrenD_92 line 195
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_92 line 196
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_92 line 197
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_92 line 198
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_92 line 199
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_92 line 200
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_92 line 205
  111. def OAI.SnakyPrototype.Certificate21.required_93 line 210
  112. def OAI.SnakyPrototype.Certificate21.envelope_93 line 211
  113. def OAI.SnakyPrototype.Certificate21.childrenC_93 line 212
  114. def OAI.SnakyPrototype.Certificate21.childrenD_93 line 213
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_93 line 214
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_93 line 215
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_93 line 216
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_93 line 217
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_93 line 218
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_93 line 223
  121. def OAI.SnakyPrototype.Certificate21.required_97 line 228
  122. def OAI.SnakyPrototype.Certificate21.envelope_97 line 229
  123. def OAI.SnakyPrototype.Certificate21.childrenC_97 line 230
  124. def OAI.SnakyPrototype.Certificate21.childrenD_97 line 231
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_97 line 232
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_97 line 233
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_97 line 234
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_97 line 235
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_97 line 236
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_97 line 241
  131. def OAI.SnakyPrototype.Certificate21.required_98 line 246
  132. def OAI.SnakyPrototype.Certificate21.envelope_98 line 247
  133. def OAI.SnakyPrototype.Certificate21.childrenC_98 line 248
  134. def OAI.SnakyPrototype.Certificate21.childrenD_98 line 249
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_98 line 250
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_98 line 251
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_98 line 252
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_98 line 253
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_98 line 254
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_98 line 259
  141. def OAI.SnakyPrototype.Certificate21.required_99 line 264
  142. def OAI.SnakyPrototype.Certificate21.envelope_99 line 265
  143. def OAI.SnakyPrototype.Certificate21.childrenC_99 line 266
  144. def OAI.SnakyPrototype.Certificate21.childrenD_99 line 267
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_99 line 268
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_99 line 269
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_99 line 270
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_99 line 271
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_99 line 272
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_99 line 277
  151. def OAI.SnakyPrototype.Certificate21.required_106 line 282
  152. def OAI.SnakyPrototype.Certificate21.envelope_106 line 283
  153. def OAI.SnakyPrototype.Certificate21.childrenC_106 line 284
  154. def OAI.SnakyPrototype.Certificate21.childrenD_106 line 285
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_106 line 286
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_106 line 287
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_106 line 288
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_106 line 289
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_106 line 290
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_106 line 295
  161. def OAI.SnakyPrototype.Certificate21.required_109 line 300
  162. def OAI.SnakyPrototype.Certificate21.envelope_109 line 301
  163. def OAI.SnakyPrototype.Certificate21.childrenC_109 line 302
  164. def OAI.SnakyPrototype.Certificate21.childrenD_109 line 303
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_109 line 304
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_109 line 305
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_109 line 306
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_109 line 307
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_109 line 308
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_109 line 313
  171. def OAI.SnakyPrototype.Certificate21.required_112 line 318
  172. def OAI.SnakyPrototype.Certificate21.envelope_112 line 319
  173. def OAI.SnakyPrototype.Certificate21.childrenC_112 line 320
  174. def OAI.SnakyPrototype.Certificate21.childrenD_112 line 321
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_112 line 322
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_112 line 323
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_112 line 324
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_112 line 325
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_112 line 326
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_112 line 331
  181. def OAI.SnakyPrototype.Certificate21.required_125 line 336
  182. def OAI.SnakyPrototype.Certificate21.envelope_125 line 337
  183. def OAI.SnakyPrototype.Certificate21.childrenC_125 line 338
  184. def OAI.SnakyPrototype.Certificate21.childrenD_125 line 339
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_125 line 340
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_125 line 341
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_125 line 342
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_125 line 343
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_125 line 344
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_125 line 349
  191. def OAI.SnakyPrototype.Certificate21.required_127 line 354
  192. def OAI.SnakyPrototype.Certificate21.envelope_127 line 355
  193. def OAI.SnakyPrototype.Certificate21.childrenC_127 line 356
  194. def OAI.SnakyPrototype.Certificate21.childrenD_127 line 357
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_127 line 358
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_127 line 359
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_127 line 360
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_127 line 361
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_127 line 362
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_127 line 368
  201. def OAI.SnakyPrototype.Certificate21.required_128 line 373
  202. def OAI.SnakyPrototype.Certificate21.envelope_128 line 374
  203. def OAI.SnakyPrototype.Certificate21.childrenC_128 line 375
  204. def OAI.SnakyPrototype.Certificate21.childrenD_128 line 376
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_128 line 377
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_128 line 378
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_128 line 379
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_128 line 380
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_128 line 381
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_128 line 387
  211. def OAI.SnakyPrototype.Certificate21.required_132 line 392
  212. def OAI.SnakyPrototype.Certificate21.envelope_132 line 393
  213. def OAI.SnakyPrototype.Certificate21.childrenC_132 line 394
  214. def OAI.SnakyPrototype.Certificate21.childrenD_132 line 395
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_132 line 396
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_132 line 397
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_132 line 398
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_132 line 399
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_132 line 400
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_132 line 405
  221. def OAI.SnakyPrototype.Certificate21.required_141 line 410
  222. def OAI.SnakyPrototype.Certificate21.envelope_141 line 411
  223. def OAI.SnakyPrototype.Certificate21.childrenC_141 line 412
  224. def OAI.SnakyPrototype.Certificate21.childrenD_141 line 413
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_141 line 414
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_141 line 415
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_141 line 416
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_141 line 417
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_141 line 418
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_141 line 424
  231. def OAI.SnakyPrototype.Certificate21.required_148 line 429
  232. def OAI.SnakyPrototype.Certificate21.envelope_148 line 430
  233. def OAI.SnakyPrototype.Certificate21.childrenC_148 line 431
  234. def OAI.SnakyPrototype.Certificate21.childrenD_148 line 432
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_148 line 433
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_148 line 434
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_148 line 435
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_148 line 436
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_148 line 437
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_148 line 442
  241. def OAI.SnakyPrototype.Certificate21.height_67 line 447
  242. def OAI.SnakyPrototype.Certificate21.childrenH_67 line 448
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_67 line 449
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_67 line 450
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_67 line 452
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_67 line 456
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_67 line 458
  248. def OAI.SnakyPrototype.Certificate21.checked_67 line 462
  249. def OAI.SnakyPrototype.Certificate21.height_73 line 470
  250. def OAI.SnakyPrototype.Certificate21.childrenH_73 line 471
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_73 line 472
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_73 line 473
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_73 line 475
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_73 line 479
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_73 line 481
  256. def OAI.SnakyPrototype.Certificate21.checked_73 line 485
  257. def OAI.SnakyPrototype.Certificate21.height_75 line 493
  258. def OAI.SnakyPrototype.Certificate21.childrenH_75 line 494
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_75 line 495
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_75 line 496
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_75 line 498
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_75 line 502
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_75 line 504
  264. def OAI.SnakyPrototype.Certificate21.checked_75 line 508
  265. def OAI.SnakyPrototype.Certificate21.height_79 line 516
  266. def OAI.SnakyPrototype.Certificate21.childrenH_79 line 517
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_79 line 518
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_79 line 519
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_79 line 521
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_79 line 525
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_79 line 527
  272. def OAI.SnakyPrototype.Certificate21.checked_79 line 531
  273. def OAI.SnakyPrototype.Certificate21.height_82 line 539
  274. def OAI.SnakyPrototype.Certificate21.childrenH_82 line 540
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_82 line 541
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_82 line 542
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_82 line 544
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_82 line 548
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_82 line 550
  280. def OAI.SnakyPrototype.Certificate21.checked_82 line 554
  281. def OAI.SnakyPrototype.Certificate21.height_86 line 562
  282. def OAI.SnakyPrototype.Certificate21.childrenH_86 line 563
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_86 line 564
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_86 line 565
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_86 line 567
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_86 line 571
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_86 line 573
  288. def OAI.SnakyPrototype.Certificate21.checked_86 line 577
  289. def OAI.SnakyPrototype.Certificate21.height_88 line 585
  290. def OAI.SnakyPrototype.Certificate21.childrenH_88 line 586
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_88 line 587
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_88 line 588
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_88 line 590
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_88 line 594
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_88 line 596
  296. def OAI.SnakyPrototype.Certificate21.checked_88 line 600
  297. def OAI.SnakyPrototype.Certificate21.height_89 line 608
  298. def OAI.SnakyPrototype.Certificate21.childrenH_89 line 609
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_89 line 610
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_89 line 611
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_89 line 613
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_89 line 617
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_89 line 619
  304. def OAI.SnakyPrototype.Certificate21.checked_89 line 623
  305. def OAI.SnakyPrototype.Certificate21.height_90 line 631
  306. def OAI.SnakyPrototype.Certificate21.childrenH_90 line 632
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_90 line 633
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_90 line 634
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_90 line 636
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_90 line 640
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_90 line 642
  312. def OAI.SnakyPrototype.Certificate21.checked_90 line 646
  313. def OAI.SnakyPrototype.Certificate21.height_91 line 654
  314. def OAI.SnakyPrototype.Certificate21.childrenH_91 line 655
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_91 line 656
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_91 line 657
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_91 line 659
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_91 line 663
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_91 line 665
  320. def OAI.SnakyPrototype.Certificate21.checked_91 line 669
  321. def OAI.SnakyPrototype.Certificate21.height_92 line 677
  322. def OAI.SnakyPrototype.Certificate21.childrenH_92 line 678
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_92 line 679
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_92 line 680
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_92 line 682
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_92 line 686
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_92 line 688
  328. def OAI.SnakyPrototype.Certificate21.checked_92 line 692
  329. def OAI.SnakyPrototype.Certificate21.height_93 line 700
  330. def OAI.SnakyPrototype.Certificate21.childrenH_93 line 701
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_93 line 702
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_93 line 703
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_93 line 705
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_93 line 709
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_93 line 711
  336. def OAI.SnakyPrototype.Certificate21.checked_93 line 715
  337. def OAI.SnakyPrototype.Certificate21.height_97 line 723
  338. def OAI.SnakyPrototype.Certificate21.childrenH_97 line 724
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_97 line 725
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_97 line 726
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_97 line 728
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_97 line 732
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_97 line 734
  344. def OAI.SnakyPrototype.Certificate21.checked_97 line 738
  345. def OAI.SnakyPrototype.Certificate21.height_98 line 746
  346. def OAI.SnakyPrototype.Certificate21.childrenH_98 line 747
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_98 line 748
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_98 line 749
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_98 line 751
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_98 line 755
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_98 line 757
  352. def OAI.SnakyPrototype.Certificate21.checked_98 line 761
  353. def OAI.SnakyPrototype.Certificate21.height_99 line 769
  354. def OAI.SnakyPrototype.Certificate21.childrenH_99 line 770
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_99 line 771
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_99 line 772
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_99 line 774
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_99 line 778
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_99 line 780
  360. def OAI.SnakyPrototype.Certificate21.checked_99 line 784
  361. def OAI.SnakyPrototype.Certificate21.height_106 line 792
  362. def OAI.SnakyPrototype.Certificate21.childrenH_106 line 793
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_106 line 794
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_106 line 795
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_106 line 797
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_106 line 801
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_106 line 803
  368. def OAI.SnakyPrototype.Certificate21.checked_106 line 807
  369. def OAI.SnakyPrototype.Certificate21.height_109 line 815
  370. def OAI.SnakyPrototype.Certificate21.childrenH_109 line 816
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_109 line 817
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_109 line 818
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_109 line 820
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_109 line 824
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_109 line 826
  376. def OAI.SnakyPrototype.Certificate21.checked_109 line 830
  377. def OAI.SnakyPrototype.Certificate21.height_112 line 838
  378. def OAI.SnakyPrototype.Certificate21.childrenH_112 line 839
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_112 line 840
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_112 line 841
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_112 line 843
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_112 line 847
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_112 line 849
  384. def OAI.SnakyPrototype.Certificate21.checked_112 line 853
  385. def OAI.SnakyPrototype.Certificate21.height_125 line 861
  386. def OAI.SnakyPrototype.Certificate21.childrenH_125 line 862
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_125 line 863
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_125 line 864
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_125 line 866
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_125 line 870
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_125 line 872
  392. def OAI.SnakyPrototype.Certificate21.checked_125 line 876
  393. def OAI.SnakyPrototype.Certificate21.height_127 line 884
  394. def OAI.SnakyPrototype.Certificate21.childrenH_127 line 885
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_127 line 886
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_127 line 887
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_127 line 889
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_127 line 893
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_127 line 895
  400. def OAI.SnakyPrototype.Certificate21.checked_127 line 899
  401. def OAI.SnakyPrototype.Certificate21.height_128 line 907
  402. def OAI.SnakyPrototype.Certificate21.childrenH_128 line 908
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_128 line 909
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_128 line 910
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_128 line 912
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_128 line 916
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_128 line 918
  408. def OAI.SnakyPrototype.Certificate21.checked_128 line 922
  409. def OAI.SnakyPrototype.Certificate21.height_132 line 930
  410. def OAI.SnakyPrototype.Certificate21.childrenH_132 line 931
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_132 line 932
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_132 line 933
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_132 line 935
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_132 line 939
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_132 line 941
  416. def OAI.SnakyPrototype.Certificate21.checked_132 line 945
  417. def OAI.SnakyPrototype.Certificate21.height_141 line 953
  418. def OAI.SnakyPrototype.Certificate21.childrenH_141 line 954
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_141 line 955
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_141 line 956
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_141 line 958
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_141 line 962
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_141 line 964
  424. def OAI.SnakyPrototype.Certificate21.checked_141 line 968
  425. def OAI.SnakyPrototype.Certificate21.height_148 line 976
  426. def OAI.SnakyPrototype.Certificate21.childrenH_148 line 977
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_148 line 978
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_148 line 979
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_148 line 981
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_148 line 985
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_148 line 987
  432. def OAI.SnakyPrototype.Certificate21.checked_148 line 991