OAI/GameTheory/SnakyTwentyOne/Cards/Height16Part02.lean

GitHub source file

252 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_683_i0 line 33
  2. def OAI.SnakyPrototype.Certificate21.envelope_683_i0 line 34
  3. def OAI.SnakyPrototype.Certificate21.childrenC_683_i0 line 35
  4. def OAI.SnakyPrototype.Certificate21.childrenD_683_i0 line 36
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_683_i0 line 37
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_683_i0 line 38
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_683_i0 line 39
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_683_i0 line 40
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_683_i0 line 41
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_683_i0 line 46
  11. def OAI.SnakyPrototype.Certificate21.required_683_i1 line 51
  12. def OAI.SnakyPrototype.Certificate21.envelope_683_i1 line 52
  13. def OAI.SnakyPrototype.Certificate21.childrenC_683_i1 line 53
  14. def OAI.SnakyPrototype.Certificate21.childrenD_683_i1 line 54
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_683_i1 line 55
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_683_i1 line 56
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_683_i1 line 57
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_683_i1 line 58
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_683_i1 line 59
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_683_i1 line 64
  21. def OAI.SnakyPrototype.Certificate21.required_683 line 69
  22. def OAI.SnakyPrototype.Certificate21.envelope_683 line 70
  23. def OAI.SnakyPrototype.Certificate21.childrenC_683 line 71
  24. def OAI.SnakyPrototype.Certificate21.childrenD_683 line 72
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_683 line 73
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_683 line 74
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_683 line 75
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_683 line 76
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_683 line 77
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_683 line 85
  31. def OAI.SnakyPrototype.Certificate21.required_706_i2 line 90
  32. def OAI.SnakyPrototype.Certificate21.envelope_706_i2 line 91
  33. def OAI.SnakyPrototype.Certificate21.childrenC_706_i2 line 92
  34. def OAI.SnakyPrototype.Certificate21.childrenD_706_i2 line 93
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i2 line 94
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i2 line 95
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i2 line 96
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i2 line 97
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i2 line 98
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i2 line 103
  41. def OAI.SnakyPrototype.Certificate21.required_706_i3 line 108
  42. def OAI.SnakyPrototype.Certificate21.envelope_706_i3 line 109
  43. def OAI.SnakyPrototype.Certificate21.childrenC_706_i3 line 110
  44. def OAI.SnakyPrototype.Certificate21.childrenD_706_i3 line 111
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i3 line 112
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i3 line 113
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i3 line 114
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i3 line 115
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i3 line 116
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i3 line 121
  51. def OAI.SnakyPrototype.Certificate21.required_706_i4 line 126
  52. def OAI.SnakyPrototype.Certificate21.envelope_706_i4 line 127
  53. def OAI.SnakyPrototype.Certificate21.childrenC_706_i4 line 128
  54. def OAI.SnakyPrototype.Certificate21.childrenD_706_i4 line 129
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i4 line 130
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i4 line 131
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i4 line 132
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i4 line 133
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i4 line 134
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i4 line 140
  61. def OAI.SnakyPrototype.Certificate21.required_706_i1 line 145
  62. def OAI.SnakyPrototype.Certificate21.envelope_706_i1 line 146
  63. def OAI.SnakyPrototype.Certificate21.childrenC_706_i1 line 147
  64. def OAI.SnakyPrototype.Certificate21.childrenD_706_i1 line 148
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i1 line 149
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i1 line 150
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i1 line 151
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i1 line 152
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i1 line 153
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i1 line 160
  71. def OAI.SnakyPrototype.Certificate21.required_706_i0 line 165
  72. def OAI.SnakyPrototype.Certificate21.envelope_706_i0 line 166
  73. def OAI.SnakyPrototype.Certificate21.childrenC_706_i0 line 167
  74. def OAI.SnakyPrototype.Certificate21.childrenD_706_i0 line 168
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i0 line 169
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i0 line 170
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i0 line 171
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i0 line 172
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i0 line 173
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i0 line 179
  81. def OAI.SnakyPrototype.Certificate21.required_706_i6 line 184
  82. def OAI.SnakyPrototype.Certificate21.envelope_706_i6 line 185
  83. def OAI.SnakyPrototype.Certificate21.childrenC_706_i6 line 186
  84. def OAI.SnakyPrototype.Certificate21.childrenD_706_i6 line 187
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i6 line 188
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i6 line 189
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i6 line 190
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i6 line 191
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i6 line 192
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i6 line 198
  91. def OAI.SnakyPrototype.Certificate21.required_706_i7 line 203
  92. def OAI.SnakyPrototype.Certificate21.envelope_706_i7 line 204
  93. def OAI.SnakyPrototype.Certificate21.childrenC_706_i7 line 205
  94. def OAI.SnakyPrototype.Certificate21.childrenD_706_i7 line 206
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i7 line 207
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i7 line 208
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i7 line 209
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i7 line 210
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i7 line 211
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i7 line 217
  101. def OAI.SnakyPrototype.Certificate21.required_706_i5 line 222
  102. def OAI.SnakyPrototype.Certificate21.envelope_706_i5 line 223
  103. def OAI.SnakyPrototype.Certificate21.childrenC_706_i5 line 224
  104. def OAI.SnakyPrototype.Certificate21.childrenD_706_i5 line 225
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i5 line 226
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i5 line 227
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i5 line 228
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i5 line 229
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i5 line 230
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i5 line 239
  111. def OAI.SnakyPrototype.Certificate21.required_706_i9 line 244
  112. def OAI.SnakyPrototype.Certificate21.envelope_706_i9 line 245
  113. def OAI.SnakyPrototype.Certificate21.childrenC_706_i9 line 246
  114. def OAI.SnakyPrototype.Certificate21.childrenD_706_i9 line 247
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i9 line 248
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i9 line 249
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i9 line 250
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i9 line 251
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i9 line 252
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i9 line 259
  121. def OAI.SnakyPrototype.Certificate21.required_706_i8 line 264
  122. def OAI.SnakyPrototype.Certificate21.envelope_706_i8 line 265
  123. def OAI.SnakyPrototype.Certificate21.childrenC_706_i8 line 266
  124. def OAI.SnakyPrototype.Certificate21.childrenD_706_i8 line 267
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_706_i8 line 268
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706_i8 line 269
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706_i8 line 270
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706_i8 line 271
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_706_i8 line 272
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_706_i8 line 279
  131. def OAI.SnakyPrototype.Certificate21.required_706 line 284
  132. def OAI.SnakyPrototype.Certificate21.envelope_706 line 285
  133. def OAI.SnakyPrototype.Certificate21.childrenC_706 line 286
  134. def OAI.SnakyPrototype.Certificate21.childrenD_706 line 287
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_706 line 288
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_706 line 289
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_706 line 290
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_706 line 291
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_706 line 292
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_706 line 302
  141. def OAI.SnakyPrototype.Certificate21.height_683_i0 line 307
  142. def OAI.SnakyPrototype.Certificate21.childrenH_683_i0 line 308
  143. theorem OAI.SnakyPrototype.Certificate21.height_exact_683_i0 line 309
  144. theorem OAI.SnakyPrototype.Certificate21.required_origin_683_i0 line 310
  145. theorem OAI.SnakyPrototype.Certificate21.required_exact_683_i0 line 312
  146. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_683_i0 line 316
  147. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_683_i0 line 318
  148. def OAI.SnakyPrototype.Certificate21.checked_683_i0 line 322
  149. def OAI.SnakyPrototype.Certificate21.height_683_i1 line 330
  150. def OAI.SnakyPrototype.Certificate21.childrenH_683_i1 line 331
  151. theorem OAI.SnakyPrototype.Certificate21.height_exact_683_i1 line 332
  152. theorem OAI.SnakyPrototype.Certificate21.required_origin_683_i1 line 333
  153. theorem OAI.SnakyPrototype.Certificate21.required_exact_683_i1 line 335
  154. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_683_i1 line 339
  155. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_683_i1 line 341
  156. def OAI.SnakyPrototype.Certificate21.checked_683_i1 line 345
  157. def OAI.SnakyPrototype.Certificate21.height_683 line 353
  158. def OAI.SnakyPrototype.Certificate21.childrenH_683 line 354
  159. theorem OAI.SnakyPrototype.Certificate21.height_exact_683 line 355
  160. theorem OAI.SnakyPrototype.Certificate21.required_origin_683 line 356
  161. theorem OAI.SnakyPrototype.Certificate21.required_exact_683 line 358
  162. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_683 line 362
  163. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_683 line 364
  164. def OAI.SnakyPrototype.Certificate21.checked_683 line 368
  165. def OAI.SnakyPrototype.Certificate21.height_706_i2 line 376
  166. def OAI.SnakyPrototype.Certificate21.childrenH_706_i2 line 377
  167. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i2 line 378
  168. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i2 line 379
  169. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i2 line 381
  170. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i2 line 385
  171. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i2 line 387
  172. def OAI.SnakyPrototype.Certificate21.checked_706_i2 line 391
  173. def OAI.SnakyPrototype.Certificate21.height_706_i3 line 399
  174. def OAI.SnakyPrototype.Certificate21.childrenH_706_i3 line 400
  175. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i3 line 401
  176. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i3 line 402
  177. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i3 line 404
  178. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i3 line 408
  179. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i3 line 410
  180. def OAI.SnakyPrototype.Certificate21.checked_706_i3 line 414
  181. def OAI.SnakyPrototype.Certificate21.height_706_i4 line 422
  182. def OAI.SnakyPrototype.Certificate21.childrenH_706_i4 line 423
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i4 line 424
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i4 line 425
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i4 line 427
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i4 line 431
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i4 line 433
  188. def OAI.SnakyPrototype.Certificate21.checked_706_i4 line 437
  189. def OAI.SnakyPrototype.Certificate21.height_706_i1 line 445
  190. def OAI.SnakyPrototype.Certificate21.childrenH_706_i1 line 446
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i1 line 447
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i1 line 448
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i1 line 450
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i1 line 454
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i1 line 456
  196. def OAI.SnakyPrototype.Certificate21.checked_706_i1 line 460
  197. def OAI.SnakyPrototype.Certificate21.height_706_i0 line 468
  198. def OAI.SnakyPrototype.Certificate21.childrenH_706_i0 line 469
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i0 line 470
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i0 line 471
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i0 line 473
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i0 line 477
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i0 line 479
  204. def OAI.SnakyPrototype.Certificate21.checked_706_i0 line 483
  205. def OAI.SnakyPrototype.Certificate21.height_706_i6 line 491
  206. def OAI.SnakyPrototype.Certificate21.childrenH_706_i6 line 492
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i6 line 493
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i6 line 494
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i6 line 496
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i6 line 500
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i6 line 502
  212. def OAI.SnakyPrototype.Certificate21.checked_706_i6 line 506
  213. def OAI.SnakyPrototype.Certificate21.height_706_i7 line 514
  214. def OAI.SnakyPrototype.Certificate21.childrenH_706_i7 line 515
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i7 line 516
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i7 line 517
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i7 line 519
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i7 line 523
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i7 line 525
  220. def OAI.SnakyPrototype.Certificate21.checked_706_i7 line 529
  221. def OAI.SnakyPrototype.Certificate21.height_706_i5 line 537
  222. def OAI.SnakyPrototype.Certificate21.childrenH_706_i5 line 538
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i5 line 539
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i5 line 540
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i5 line 542
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i5 line 546
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i5 line 548
  228. def OAI.SnakyPrototype.Certificate21.checked_706_i5 line 552
  229. def OAI.SnakyPrototype.Certificate21.height_706_i9 line 560
  230. def OAI.SnakyPrototype.Certificate21.childrenH_706_i9 line 561
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i9 line 562
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i9 line 563
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i9 line 565
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i9 line 569
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i9 line 571
  236. def OAI.SnakyPrototype.Certificate21.checked_706_i9 line 575
  237. def OAI.SnakyPrototype.Certificate21.height_706_i8 line 583
  238. def OAI.SnakyPrototype.Certificate21.childrenH_706_i8 line 584
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_706_i8 line 585
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_706_i8 line 586
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_706_i8 line 588
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706_i8 line 592
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706_i8 line 594
  244. def OAI.SnakyPrototype.Certificate21.checked_706_i8 line 598
  245. def OAI.SnakyPrototype.Certificate21.height_706 line 606
  246. def OAI.SnakyPrototype.Certificate21.childrenH_706 line 607
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_706 line 608
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_706 line 609
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_706 line 611
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_706 line 615
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_706 line 617
  252. def OAI.SnakyPrototype.Certificate21.checked_706 line 621