OAI/GameTheory/SnakyTwentyOne/Cards/Height05Part05.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_391_i1 line 14
  2. def OAI.SnakyPrototype.Certificate21.envelope_391_i1 line 15
  3. def OAI.SnakyPrototype.Certificate21.childrenC_391_i1 line 16
  4. def OAI.SnakyPrototype.Certificate21.childrenD_391_i1 line 17
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_391_i1 line 18
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_391_i1 line 19
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_391_i1 line 20
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_391_i1 line 21
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_391_i1 line 22
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_391_i1 line 27
  11. def OAI.SnakyPrototype.Certificate21.required_391_i0 line 32
  12. def OAI.SnakyPrototype.Certificate21.envelope_391_i0 line 33
  13. def OAI.SnakyPrototype.Certificate21.childrenC_391_i0 line 34
  14. def OAI.SnakyPrototype.Certificate21.childrenD_391_i0 line 35
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_391_i0 line 36
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_391_i0 line 37
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_391_i0 line 38
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_391_i0 line 39
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_391_i0 line 40
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_391_i0 line 45
  21. def OAI.SnakyPrototype.Certificate21.required_391 line 50
  22. def OAI.SnakyPrototype.Certificate21.envelope_391 line 51
  23. def OAI.SnakyPrototype.Certificate21.childrenC_391 line 52
  24. def OAI.SnakyPrototype.Certificate21.childrenD_391 line 53
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_391 line 54
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_391 line 55
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_391 line 56
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_391 line 57
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_391 line 58
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_391 line 63
  31. def OAI.SnakyPrototype.Certificate21.required_413_i0 line 68
  32. def OAI.SnakyPrototype.Certificate21.envelope_413_i0 line 69
  33. def OAI.SnakyPrototype.Certificate21.childrenC_413_i0 line 70
  34. def OAI.SnakyPrototype.Certificate21.childrenD_413_i0 line 71
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_413_i0 line 72
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_413_i0 line 73
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_413_i0 line 74
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_413_i0 line 75
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_413_i0 line 76
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_413_i0 line 81
  41. def OAI.SnakyPrototype.Certificate21.required_413 line 86
  42. def OAI.SnakyPrototype.Certificate21.envelope_413 line 87
  43. def OAI.SnakyPrototype.Certificate21.childrenC_413 line 88
  44. def OAI.SnakyPrototype.Certificate21.childrenD_413 line 89
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_413 line 90
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_413 line 91
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_413 line 92
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_413 line 93
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_413 line 94
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_413 line 99
  51. def OAI.SnakyPrototype.Certificate21.required_416_i0 line 104
  52. def OAI.SnakyPrototype.Certificate21.envelope_416_i0 line 105
  53. def OAI.SnakyPrototype.Certificate21.childrenC_416_i0 line 106
  54. def OAI.SnakyPrototype.Certificate21.childrenD_416_i0 line 107
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_416_i0 line 108
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_416_i0 line 109
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_416_i0 line 110
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_416_i0 line 111
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_416_i0 line 112
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_416_i0 line 117
  61. def OAI.SnakyPrototype.Certificate21.required_416 line 122
  62. def OAI.SnakyPrototype.Certificate21.envelope_416 line 123
  63. def OAI.SnakyPrototype.Certificate21.childrenC_416 line 124
  64. def OAI.SnakyPrototype.Certificate21.childrenD_416 line 125
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_416 line 126
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_416 line 127
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_416 line 128
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_416 line 129
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_416 line 130
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_416 line 135
  71. def OAI.SnakyPrototype.Certificate21.required_425_i0 line 140
  72. def OAI.SnakyPrototype.Certificate21.envelope_425_i0 line 141
  73. def OAI.SnakyPrototype.Certificate21.childrenC_425_i0 line 142
  74. def OAI.SnakyPrototype.Certificate21.childrenD_425_i0 line 143
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_425_i0 line 144
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_425_i0 line 145
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_425_i0 line 146
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_425_i0 line 147
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_425_i0 line 148
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_425_i0 line 153
  81. def OAI.SnakyPrototype.Certificate21.required_425 line 158
  82. def OAI.SnakyPrototype.Certificate21.envelope_425 line 159
  83. def OAI.SnakyPrototype.Certificate21.childrenC_425 line 160
  84. def OAI.SnakyPrototype.Certificate21.childrenD_425 line 161
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_425 line 162
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_425 line 163
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_425 line 164
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_425 line 165
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_425 line 166
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_425 line 171
  91. def OAI.SnakyPrototype.Certificate21.required_426_i0 line 176
  92. def OAI.SnakyPrototype.Certificate21.envelope_426_i0 line 177
  93. def OAI.SnakyPrototype.Certificate21.childrenC_426_i0 line 178
  94. def OAI.SnakyPrototype.Certificate21.childrenD_426_i0 line 179
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_426_i0 line 180
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_426_i0 line 181
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_426_i0 line 182
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_426_i0 line 183
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_426_i0 line 184
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_426_i0 line 189
  101. def OAI.SnakyPrototype.Certificate21.required_426 line 194
  102. def OAI.SnakyPrototype.Certificate21.envelope_426 line 195
  103. def OAI.SnakyPrototype.Certificate21.childrenC_426 line 196
  104. def OAI.SnakyPrototype.Certificate21.childrenD_426 line 197
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_426 line 198
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_426 line 199
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_426 line 200
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_426 line 201
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_426 line 202
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_426 line 207
  111. def OAI.SnakyPrototype.Certificate21.required_433 line 212
  112. def OAI.SnakyPrototype.Certificate21.envelope_433 line 213
  113. def OAI.SnakyPrototype.Certificate21.childrenC_433 line 214
  114. def OAI.SnakyPrototype.Certificate21.childrenD_433 line 215
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_433 line 216
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_433 line 217
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_433 line 218
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_433 line 219
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_433 line 220
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_433 line 225
  121. def OAI.SnakyPrototype.Certificate21.required_445_i0 line 230
  122. def OAI.SnakyPrototype.Certificate21.envelope_445_i0 line 231
  123. def OAI.SnakyPrototype.Certificate21.childrenC_445_i0 line 232
  124. def OAI.SnakyPrototype.Certificate21.childrenD_445_i0 line 233
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_445_i0 line 234
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_445_i0 line 235
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_445_i0 line 236
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_445_i0 line 237
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_445_i0 line 238
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_445_i0 line 244
  131. def OAI.SnakyPrototype.Certificate21.required_445 line 249
  132. def OAI.SnakyPrototype.Certificate21.envelope_445 line 250
  133. def OAI.SnakyPrototype.Certificate21.childrenC_445 line 251
  134. def OAI.SnakyPrototype.Certificate21.childrenD_445 line 252
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_445 line 253
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_445 line 254
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_445 line 255
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_445 line 256
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_445 line 257
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_445 line 262
  141. def OAI.SnakyPrototype.Certificate21.required_451_i0 line 267
  142. def OAI.SnakyPrototype.Certificate21.envelope_451_i0 line 268
  143. def OAI.SnakyPrototype.Certificate21.childrenC_451_i0 line 269
  144. def OAI.SnakyPrototype.Certificate21.childrenD_451_i0 line 270
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_451_i0 line 271
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_451_i0 line 272
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_451_i0 line 273
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_451_i0 line 274
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_451_i0 line 275
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_451_i0 line 280
  151. def OAI.SnakyPrototype.Certificate21.required_451 line 285
  152. def OAI.SnakyPrototype.Certificate21.envelope_451 line 286
  153. def OAI.SnakyPrototype.Certificate21.childrenC_451 line 287
  154. def OAI.SnakyPrototype.Certificate21.childrenD_451 line 288
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_451 line 289
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_451 line 290
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_451 line 291
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_451 line 292
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_451 line 293
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_451 line 298
  161. def OAI.SnakyPrototype.Certificate21.required_464_i1 line 303
  162. def OAI.SnakyPrototype.Certificate21.envelope_464_i1 line 304
  163. def OAI.SnakyPrototype.Certificate21.childrenC_464_i1 line 305
  164. def OAI.SnakyPrototype.Certificate21.childrenD_464_i1 line 306
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_464_i1 line 307
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_464_i1 line 308
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_464_i1 line 309
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_464_i1 line 310
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_464_i1 line 311
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_464_i1 line 316
  171. def OAI.SnakyPrototype.Certificate21.required_464_i0 line 321
  172. def OAI.SnakyPrototype.Certificate21.envelope_464_i0 line 322
  173. def OAI.SnakyPrototype.Certificate21.childrenC_464_i0 line 323
  174. def OAI.SnakyPrototype.Certificate21.childrenD_464_i0 line 324
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_464_i0 line 325
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_464_i0 line 326
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_464_i0 line 327
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_464_i0 line 328
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_464_i0 line 329
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_464_i0 line 334
  181. def OAI.SnakyPrototype.Certificate21.required_464_i2 line 339
  182. def OAI.SnakyPrototype.Certificate21.envelope_464_i2 line 340
  183. def OAI.SnakyPrototype.Certificate21.childrenC_464_i2 line 341
  184. def OAI.SnakyPrototype.Certificate21.childrenD_464_i2 line 342
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_464_i2 line 343
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_464_i2 line 344
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_464_i2 line 345
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_464_i2 line 346
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_464_i2 line 347
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_464_i2 line 352
  191. def OAI.SnakyPrototype.Certificate21.required_464 line 357
  192. def OAI.SnakyPrototype.Certificate21.envelope_464 line 358
  193. def OAI.SnakyPrototype.Certificate21.childrenC_464 line 359
  194. def OAI.SnakyPrototype.Certificate21.childrenD_464 line 360
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_464 line 361
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_464 line 362
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_464 line 363
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_464 line 364
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_464 line 365
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_464 line 371
  201. def OAI.SnakyPrototype.Certificate21.required_492_i1 line 376
  202. def OAI.SnakyPrototype.Certificate21.envelope_492_i1 line 377
  203. def OAI.SnakyPrototype.Certificate21.childrenC_492_i1 line 378
  204. def OAI.SnakyPrototype.Certificate21.childrenD_492_i1 line 379
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_492_i1 line 380
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_492_i1 line 381
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_492_i1 line 382
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_492_i1 line 383
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_492_i1 line 384
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_492_i1 line 389
  211. def OAI.SnakyPrototype.Certificate21.required_492_i0 line 394
  212. def OAI.SnakyPrototype.Certificate21.envelope_492_i0 line 395
  213. def OAI.SnakyPrototype.Certificate21.childrenC_492_i0 line 396
  214. def OAI.SnakyPrototype.Certificate21.childrenD_492_i0 line 397
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_492_i0 line 398
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_492_i0 line 399
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_492_i0 line 400
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_492_i0 line 401
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_492_i0 line 402
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_492_i0 line 407
  221. def OAI.SnakyPrototype.Certificate21.required_492 line 412
  222. def OAI.SnakyPrototype.Certificate21.envelope_492 line 413
  223. def OAI.SnakyPrototype.Certificate21.childrenC_492 line 414
  224. def OAI.SnakyPrototype.Certificate21.childrenD_492 line 415
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_492 line 416
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_492 line 417
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_492 line 418
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_492 line 419
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_492 line 420
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_492 line 425
  231. def OAI.SnakyPrototype.Certificate21.height_391_i1 line 430
  232. def OAI.SnakyPrototype.Certificate21.childrenH_391_i1 line 431
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_391_i1 line 432
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_391_i1 line 433
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_391_i1 line 435
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_391_i1 line 439
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_391_i1 line 441
  238. def OAI.SnakyPrototype.Certificate21.checked_391_i1 line 445
  239. def OAI.SnakyPrototype.Certificate21.height_391_i0 line 453
  240. def OAI.SnakyPrototype.Certificate21.childrenH_391_i0 line 454
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_391_i0 line 455
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_391_i0 line 456
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_391_i0 line 458
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_391_i0 line 462
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_391_i0 line 464
  246. def OAI.SnakyPrototype.Certificate21.checked_391_i0 line 468
  247. def OAI.SnakyPrototype.Certificate21.height_391 line 476
  248. def OAI.SnakyPrototype.Certificate21.childrenH_391 line 477
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_391 line 478
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_391 line 479
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_391 line 481
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_391 line 485
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_391 line 487
  254. def OAI.SnakyPrototype.Certificate21.checked_391 line 491
  255. def OAI.SnakyPrototype.Certificate21.height_413_i0 line 499
  256. def OAI.SnakyPrototype.Certificate21.childrenH_413_i0 line 500
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_413_i0 line 501
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_413_i0 line 502
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_413_i0 line 504
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_413_i0 line 508
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_413_i0 line 510
  262. def OAI.SnakyPrototype.Certificate21.checked_413_i0 line 514
  263. def OAI.SnakyPrototype.Certificate21.height_413 line 522
  264. def OAI.SnakyPrototype.Certificate21.childrenH_413 line 523
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_413 line 524
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_413 line 525
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_413 line 527
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_413 line 531
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_413 line 533
  270. def OAI.SnakyPrototype.Certificate21.checked_413 line 537
  271. def OAI.SnakyPrototype.Certificate21.height_416_i0 line 545
  272. def OAI.SnakyPrototype.Certificate21.childrenH_416_i0 line 546
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_416_i0 line 547
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_416_i0 line 548
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_416_i0 line 550
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_416_i0 line 554
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_416_i0 line 556
  278. def OAI.SnakyPrototype.Certificate21.checked_416_i0 line 560
  279. def OAI.SnakyPrototype.Certificate21.height_416 line 568
  280. def OAI.SnakyPrototype.Certificate21.childrenH_416 line 569
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_416 line 570
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_416 line 571
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_416 line 573
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_416 line 577
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_416 line 579
  286. def OAI.SnakyPrototype.Certificate21.checked_416 line 583
  287. def OAI.SnakyPrototype.Certificate21.height_425_i0 line 591
  288. def OAI.SnakyPrototype.Certificate21.childrenH_425_i0 line 592
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_425_i0 line 593
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_425_i0 line 594
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_425_i0 line 596
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_425_i0 line 600
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_425_i0 line 602
  294. def OAI.SnakyPrototype.Certificate21.checked_425_i0 line 606
  295. def OAI.SnakyPrototype.Certificate21.height_425 line 614
  296. def OAI.SnakyPrototype.Certificate21.childrenH_425 line 615
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_425 line 616
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_425 line 617
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_425 line 619
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_425 line 623
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_425 line 625
  302. def OAI.SnakyPrototype.Certificate21.checked_425 line 629
  303. def OAI.SnakyPrototype.Certificate21.height_426_i0 line 637
  304. def OAI.SnakyPrototype.Certificate21.childrenH_426_i0 line 638
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_426_i0 line 639
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_426_i0 line 640
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_426_i0 line 642
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_426_i0 line 646
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_426_i0 line 648
  310. def OAI.SnakyPrototype.Certificate21.checked_426_i0 line 652
  311. def OAI.SnakyPrototype.Certificate21.height_426 line 660
  312. def OAI.SnakyPrototype.Certificate21.childrenH_426 line 661
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_426 line 662
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_426 line 663
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_426 line 665
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_426 line 669
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_426 line 671
  318. def OAI.SnakyPrototype.Certificate21.checked_426 line 675
  319. def OAI.SnakyPrototype.Certificate21.height_433 line 683
  320. def OAI.SnakyPrototype.Certificate21.childrenH_433 line 684
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_433 line 685
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_433 line 686
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_433 line 688
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_433 line 692
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_433 line 694
  326. def OAI.SnakyPrototype.Certificate21.checked_433 line 698
  327. def OAI.SnakyPrototype.Certificate21.height_445_i0 line 706
  328. def OAI.SnakyPrototype.Certificate21.childrenH_445_i0 line 707
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_445_i0 line 708
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_445_i0 line 709
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_445_i0 line 711
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_445_i0 line 715
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_445_i0 line 717
  334. def OAI.SnakyPrototype.Certificate21.checked_445_i0 line 721
  335. def OAI.SnakyPrototype.Certificate21.height_445 line 729
  336. def OAI.SnakyPrototype.Certificate21.childrenH_445 line 730
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_445 line 731
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_445 line 732
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_445 line 734
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_445 line 738
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_445 line 740
  342. def OAI.SnakyPrototype.Certificate21.checked_445 line 744
  343. def OAI.SnakyPrototype.Certificate21.height_451_i0 line 752
  344. def OAI.SnakyPrototype.Certificate21.childrenH_451_i0 line 753
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_451_i0 line 754
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_451_i0 line 755
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_451_i0 line 757
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_451_i0 line 761
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_451_i0 line 763
  350. def OAI.SnakyPrototype.Certificate21.checked_451_i0 line 767
  351. def OAI.SnakyPrototype.Certificate21.height_451 line 775
  352. def OAI.SnakyPrototype.Certificate21.childrenH_451 line 776
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_451 line 777
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_451 line 778
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_451 line 780
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_451 line 784
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_451 line 786
  358. def OAI.SnakyPrototype.Certificate21.checked_451 line 790
  359. def OAI.SnakyPrototype.Certificate21.height_464_i1 line 798
  360. def OAI.SnakyPrototype.Certificate21.childrenH_464_i1 line 799
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_464_i1 line 800
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_464_i1 line 801
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_464_i1 line 803
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_464_i1 line 807
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_464_i1 line 809
  366. def OAI.SnakyPrototype.Certificate21.checked_464_i1 line 813
  367. def OAI.SnakyPrototype.Certificate21.height_464_i0 line 821
  368. def OAI.SnakyPrototype.Certificate21.childrenH_464_i0 line 822
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_464_i0 line 823
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_464_i0 line 824
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_464_i0 line 826
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_464_i0 line 830
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_464_i0 line 832
  374. def OAI.SnakyPrototype.Certificate21.checked_464_i0 line 836
  375. def OAI.SnakyPrototype.Certificate21.height_464_i2 line 844
  376. def OAI.SnakyPrototype.Certificate21.childrenH_464_i2 line 845
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_464_i2 line 846
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_464_i2 line 847
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_464_i2 line 849
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_464_i2 line 853
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_464_i2 line 855
  382. def OAI.SnakyPrototype.Certificate21.checked_464_i2 line 859
  383. def OAI.SnakyPrototype.Certificate21.height_464 line 867
  384. def OAI.SnakyPrototype.Certificate21.childrenH_464 line 868
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_464 line 869
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_464 line 870
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_464 line 872
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_464 line 876
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_464 line 878
  390. def OAI.SnakyPrototype.Certificate21.checked_464 line 882
  391. def OAI.SnakyPrototype.Certificate21.height_492_i1 line 890
  392. def OAI.SnakyPrototype.Certificate21.childrenH_492_i1 line 891
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_492_i1 line 892
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_492_i1 line 893
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_492_i1 line 895
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_492_i1 line 899
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_492_i1 line 901
  398. def OAI.SnakyPrototype.Certificate21.checked_492_i1 line 905
  399. def OAI.SnakyPrototype.Certificate21.height_492_i0 line 913
  400. def OAI.SnakyPrototype.Certificate21.childrenH_492_i0 line 914
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_492_i0 line 915
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_492_i0 line 916
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_492_i0 line 918
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_492_i0 line 922
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_492_i0 line 924
  406. def OAI.SnakyPrototype.Certificate21.checked_492_i0 line 928
  407. def OAI.SnakyPrototype.Certificate21.height_492 line 936
  408. def OAI.SnakyPrototype.Certificate21.childrenH_492 line 937
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_492 line 938
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_492 line 939
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_492 line 941
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_492 line 945
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_492 line 947
  414. def OAI.SnakyPrototype.Certificate21.checked_492 line 951