OAI/GameTheory/SnakyTwentyOne/Cards/Height11Part06.lean

GitHub source file

270 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_689_i0 line 26
  2. def OAI.SnakyPrototype.Certificate21.envelope_689_i0 line 27
  3. def OAI.SnakyPrototype.Certificate21.childrenC_689_i0 line 28
  4. def OAI.SnakyPrototype.Certificate21.childrenD_689_i0 line 29
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_689_i0 line 30
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_689_i0 line 31
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_689_i0 line 32
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_689_i0 line 33
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_689_i0 line 34
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_689_i0 line 43
  11. def OAI.SnakyPrototype.Certificate21.required_689 line 48
  12. def OAI.SnakyPrototype.Certificate21.envelope_689 line 49
  13. def OAI.SnakyPrototype.Certificate21.childrenC_689 line 50
  14. def OAI.SnakyPrototype.Certificate21.childrenD_689 line 51
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_689 line 52
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_689 line 53
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_689 line 54
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_689 line 55
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_689 line 56
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_689 line 63
  21. def OAI.SnakyPrototype.Certificate21.required_700_i0 line 68
  22. def OAI.SnakyPrototype.Certificate21.envelope_700_i0 line 69
  23. def OAI.SnakyPrototype.Certificate21.childrenC_700_i0 line 70
  24. def OAI.SnakyPrototype.Certificate21.childrenD_700_i0 line 71
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i0 line 72
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i0 line 73
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i0 line 74
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i0 line 75
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i0 line 76
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i0 line 81
  31. def OAI.SnakyPrototype.Certificate21.required_700_i3 line 86
  32. def OAI.SnakyPrototype.Certificate21.envelope_700_i3 line 87
  33. def OAI.SnakyPrototype.Certificate21.childrenC_700_i3 line 88
  34. def OAI.SnakyPrototype.Certificate21.childrenD_700_i3 line 89
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i3 line 90
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i3 line 91
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i3 line 92
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i3 line 93
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i3 line 94
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i3 line 99
  41. def OAI.SnakyPrototype.Certificate21.required_700_i2 line 104
  42. def OAI.SnakyPrototype.Certificate21.envelope_700_i2 line 105
  43. def OAI.SnakyPrototype.Certificate21.childrenC_700_i2 line 106
  44. def OAI.SnakyPrototype.Certificate21.childrenD_700_i2 line 107
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i2 line 108
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i2 line 109
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i2 line 110
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i2 line 111
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i2 line 112
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i2 line 117
  51. def OAI.SnakyPrototype.Certificate21.required_700_i1 line 122
  52. def OAI.SnakyPrototype.Certificate21.envelope_700_i1 line 123
  53. def OAI.SnakyPrototype.Certificate21.childrenC_700_i1 line 124
  54. def OAI.SnakyPrototype.Certificate21.childrenD_700_i1 line 125
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i1 line 126
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i1 line 127
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i1 line 128
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i1 line 129
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i1 line 130
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i1 line 136
  61. def OAI.SnakyPrototype.Certificate21.required_700_i5 line 141
  62. def OAI.SnakyPrototype.Certificate21.envelope_700_i5 line 142
  63. def OAI.SnakyPrototype.Certificate21.childrenC_700_i5 line 143
  64. def OAI.SnakyPrototype.Certificate21.childrenD_700_i5 line 144
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i5 line 145
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i5 line 146
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i5 line 147
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i5 line 148
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i5 line 149
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i5 line 155
  71. def OAI.SnakyPrototype.Certificate21.required_700_i6 line 160
  72. def OAI.SnakyPrototype.Certificate21.envelope_700_i6 line 161
  73. def OAI.SnakyPrototype.Certificate21.childrenC_700_i6 line 162
  74. def OAI.SnakyPrototype.Certificate21.childrenD_700_i6 line 163
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i6 line 164
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i6 line 165
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i6 line 166
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i6 line 167
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i6 line 168
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i6 line 173
  81. def OAI.SnakyPrototype.Certificate21.required_700_i4 line 178
  82. def OAI.SnakyPrototype.Certificate21.envelope_700_i4 line 179
  83. def OAI.SnakyPrototype.Certificate21.childrenC_700_i4 line 180
  84. def OAI.SnakyPrototype.Certificate21.childrenD_700_i4 line 181
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_700_i4 line 182
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700_i4 line 183
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700_i4 line 184
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700_i4 line 185
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_700_i4 line 186
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_700_i4 line 192
  91. def OAI.SnakyPrototype.Certificate21.required_700 line 197
  92. def OAI.SnakyPrototype.Certificate21.envelope_700 line 198
  93. def OAI.SnakyPrototype.Certificate21.childrenC_700 line 199
  94. def OAI.SnakyPrototype.Certificate21.childrenD_700 line 200
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_700 line 201
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_700 line 202
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_700 line 203
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_700 line 204
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_700 line 205
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_700 line 213
  101. def OAI.SnakyPrototype.Certificate21.required_710_i1 line 218
  102. def OAI.SnakyPrototype.Certificate21.envelope_710_i1 line 219
  103. def OAI.SnakyPrototype.Certificate21.childrenC_710_i1 line 220
  104. def OAI.SnakyPrototype.Certificate21.childrenD_710_i1 line 221
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_710_i1 line 222
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_710_i1 line 223
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_710_i1 line 224
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_710_i1 line 225
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_710_i1 line 226
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_710_i1 line 231
  111. def OAI.SnakyPrototype.Certificate21.required_710_i0 line 236
  112. def OAI.SnakyPrototype.Certificate21.envelope_710_i0 line 237
  113. def OAI.SnakyPrototype.Certificate21.childrenC_710_i0 line 238
  114. def OAI.SnakyPrototype.Certificate21.childrenD_710_i0 line 239
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_710_i0 line 240
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_710_i0 line 241
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_710_i0 line 242
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_710_i0 line 243
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_710_i0 line 244
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_710_i0 line 251
  121. def OAI.SnakyPrototype.Certificate21.required_710 line 256
  122. def OAI.SnakyPrototype.Certificate21.envelope_710 line 257
  123. def OAI.SnakyPrototype.Certificate21.childrenC_710 line 258
  124. def OAI.SnakyPrototype.Certificate21.childrenD_710 line 259
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_710 line 260
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_710 line 261
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_710 line 262
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_710 line 263
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_710 line 264
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_710 line 271
  131. def OAI.SnakyPrototype.Certificate21.required_716_i0 line 276
  132. def OAI.SnakyPrototype.Certificate21.envelope_716_i0 line 277
  133. def OAI.SnakyPrototype.Certificate21.childrenC_716_i0 line 278
  134. def OAI.SnakyPrototype.Certificate21.childrenD_716_i0 line 279
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_716_i0 line 280
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_716_i0 line 281
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_716_i0 line 282
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_716_i0 line 283
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_716_i0 line 284
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_716_i0 line 289
  141. def OAI.SnakyPrototype.Certificate21.required_716 line 294
  142. def OAI.SnakyPrototype.Certificate21.envelope_716 line 295
  143. def OAI.SnakyPrototype.Certificate21.childrenC_716 line 296
  144. def OAI.SnakyPrototype.Certificate21.childrenD_716 line 297
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_716 line 298
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_716 line 299
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_716 line 300
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_716 line 301
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_716 line 302
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_716 line 309
  151. def OAI.SnakyPrototype.Certificate21.height_689_i0 line 314
  152. def OAI.SnakyPrototype.Certificate21.childrenH_689_i0 line 315
  153. theorem OAI.SnakyPrototype.Certificate21.height_exact_689_i0 line 316
  154. theorem OAI.SnakyPrototype.Certificate21.required_origin_689_i0 line 317
  155. theorem OAI.SnakyPrototype.Certificate21.required_exact_689_i0 line 319
  156. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_689_i0 line 323
  157. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_689_i0 line 325
  158. def OAI.SnakyPrototype.Certificate21.checked_689_i0 line 329
  159. def OAI.SnakyPrototype.Certificate21.height_689 line 337
  160. def OAI.SnakyPrototype.Certificate21.childrenH_689 line 338
  161. theorem OAI.SnakyPrototype.Certificate21.height_exact_689 line 339
  162. theorem OAI.SnakyPrototype.Certificate21.required_origin_689 line 340
  163. theorem OAI.SnakyPrototype.Certificate21.required_exact_689 line 342
  164. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_689 line 346
  165. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_689 line 348
  166. def OAI.SnakyPrototype.Certificate21.checked_689 line 352
  167. def OAI.SnakyPrototype.Certificate21.height_700_i0 line 360
  168. def OAI.SnakyPrototype.Certificate21.childrenH_700_i0 line 361
  169. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i0 line 362
  170. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i0 line 363
  171. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i0 line 365
  172. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i0 line 369
  173. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i0 line 371
  174. def OAI.SnakyPrototype.Certificate21.checked_700_i0 line 375
  175. def OAI.SnakyPrototype.Certificate21.height_700_i3 line 383
  176. def OAI.SnakyPrototype.Certificate21.childrenH_700_i3 line 384
  177. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i3 line 385
  178. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i3 line 386
  179. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i3 line 388
  180. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i3 line 392
  181. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i3 line 394
  182. def OAI.SnakyPrototype.Certificate21.checked_700_i3 line 398
  183. def OAI.SnakyPrototype.Certificate21.height_700_i2 line 406
  184. def OAI.SnakyPrototype.Certificate21.childrenH_700_i2 line 407
  185. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i2 line 408
  186. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i2 line 409
  187. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i2 line 411
  188. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i2 line 415
  189. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i2 line 417
  190. def OAI.SnakyPrototype.Certificate21.checked_700_i2 line 421
  191. def OAI.SnakyPrototype.Certificate21.height_700_i1 line 429
  192. def OAI.SnakyPrototype.Certificate21.childrenH_700_i1 line 430
  193. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i1 line 431
  194. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i1 line 432
  195. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i1 line 434
  196. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i1 line 438
  197. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i1 line 440
  198. def OAI.SnakyPrototype.Certificate21.checked_700_i1 line 444
  199. def OAI.SnakyPrototype.Certificate21.height_700_i5 line 452
  200. def OAI.SnakyPrototype.Certificate21.childrenH_700_i5 line 453
  201. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i5 line 454
  202. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i5 line 455
  203. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i5 line 457
  204. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i5 line 461
  205. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i5 line 463
  206. def OAI.SnakyPrototype.Certificate21.checked_700_i5 line 467
  207. def OAI.SnakyPrototype.Certificate21.height_700_i6 line 475
  208. def OAI.SnakyPrototype.Certificate21.childrenH_700_i6 line 476
  209. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i6 line 477
  210. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i6 line 478
  211. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i6 line 480
  212. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i6 line 484
  213. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i6 line 486
  214. def OAI.SnakyPrototype.Certificate21.checked_700_i6 line 490
  215. def OAI.SnakyPrototype.Certificate21.height_700_i4 line 498
  216. def OAI.SnakyPrototype.Certificate21.childrenH_700_i4 line 499
  217. theorem OAI.SnakyPrototype.Certificate21.height_exact_700_i4 line 500
  218. theorem OAI.SnakyPrototype.Certificate21.required_origin_700_i4 line 501
  219. theorem OAI.SnakyPrototype.Certificate21.required_exact_700_i4 line 503
  220. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700_i4 line 507
  221. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700_i4 line 509
  222. def OAI.SnakyPrototype.Certificate21.checked_700_i4 line 513
  223. def OAI.SnakyPrototype.Certificate21.height_700 line 521
  224. def OAI.SnakyPrototype.Certificate21.childrenH_700 line 522
  225. theorem OAI.SnakyPrototype.Certificate21.height_exact_700 line 523
  226. theorem OAI.SnakyPrototype.Certificate21.required_origin_700 line 524
  227. theorem OAI.SnakyPrototype.Certificate21.required_exact_700 line 526
  228. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_700 line 530
  229. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_700 line 532
  230. def OAI.SnakyPrototype.Certificate21.checked_700 line 536
  231. def OAI.SnakyPrototype.Certificate21.height_710_i1 line 544
  232. def OAI.SnakyPrototype.Certificate21.childrenH_710_i1 line 545
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_710_i1 line 546
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_710_i1 line 547
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_710_i1 line 549
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_710_i1 line 553
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_710_i1 line 555
  238. def OAI.SnakyPrototype.Certificate21.checked_710_i1 line 559
  239. def OAI.SnakyPrototype.Certificate21.height_710_i0 line 567
  240. def OAI.SnakyPrototype.Certificate21.childrenH_710_i0 line 568
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_710_i0 line 569
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_710_i0 line 570
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_710_i0 line 572
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_710_i0 line 576
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_710_i0 line 578
  246. def OAI.SnakyPrototype.Certificate21.checked_710_i0 line 582
  247. def OAI.SnakyPrototype.Certificate21.height_710 line 590
  248. def OAI.SnakyPrototype.Certificate21.childrenH_710 line 591
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_710 line 592
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_710 line 593
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_710 line 595
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_710 line 599
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_710 line 601
  254. def OAI.SnakyPrototype.Certificate21.checked_710 line 605
  255. def OAI.SnakyPrototype.Certificate21.height_716_i0 line 613
  256. def OAI.SnakyPrototype.Certificate21.childrenH_716_i0 line 614
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_716_i0 line 615
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_716_i0 line 616
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_716_i0 line 618
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_716_i0 line 622
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_716_i0 line 624
  262. def OAI.SnakyPrototype.Certificate21.checked_716_i0 line 628
  263. def OAI.SnakyPrototype.Certificate21.height_716 line 636
  264. def OAI.SnakyPrototype.Certificate21.childrenH_716 line 637
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_716 line 638
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_716 line 639
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_716 line 641
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_716 line 645
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_716 line 647
  270. def OAI.SnakyPrototype.Certificate21.checked_716 line 651