OAI/GameTheory/SnakyTwentyOne/Cards/Height14Part04.lean

GitHub source file

252 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_697_i4 line 33
  2. def OAI.SnakyPrototype.Certificate21.envelope_697_i4 line 34
  3. def OAI.SnakyPrototype.Certificate21.childrenC_697_i4 line 35
  4. def OAI.SnakyPrototype.Certificate21.childrenD_697_i4 line 36
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_697_i4 line 37
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_697_i4 line 38
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_697_i4 line 39
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_697_i4 line 40
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_697_i4 line 41
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_697_i4 line 46
  11. def OAI.SnakyPrototype.Certificate21.required_697_i3 line 51
  12. def OAI.SnakyPrototype.Certificate21.envelope_697_i3 line 52
  13. def OAI.SnakyPrototype.Certificate21.childrenC_697_i3 line 53
  14. def OAI.SnakyPrototype.Certificate21.childrenD_697_i3 line 54
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_697_i3 line 55
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_697_i3 line 56
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_697_i3 line 57
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_697_i3 line 58
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_697_i3 line 59
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_697_i3 line 64
  21. def OAI.SnakyPrototype.Certificate21.required_697_i2 line 69
  22. def OAI.SnakyPrototype.Certificate21.envelope_697_i2 line 70
  23. def OAI.SnakyPrototype.Certificate21.childrenC_697_i2 line 71
  24. def OAI.SnakyPrototype.Certificate21.childrenD_697_i2 line 72
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_697_i2 line 73
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_697_i2 line 74
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_697_i2 line 75
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_697_i2 line 76
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_697_i2 line 77
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_697_i2 line 83
  31. def OAI.SnakyPrototype.Certificate21.required_697_i1 line 88
  32. def OAI.SnakyPrototype.Certificate21.envelope_697_i1 line 89
  33. def OAI.SnakyPrototype.Certificate21.childrenC_697_i1 line 90
  34. def OAI.SnakyPrototype.Certificate21.childrenD_697_i1 line 91
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_697_i1 line 92
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_697_i1 line 93
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_697_i1 line 94
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_697_i1 line 95
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_697_i1 line 96
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_697_i1 line 102
  41. def OAI.SnakyPrototype.Certificate21.required_697_i0 line 107
  42. def OAI.SnakyPrototype.Certificate21.envelope_697_i0 line 108
  43. def OAI.SnakyPrototype.Certificate21.childrenC_697_i0 line 109
  44. def OAI.SnakyPrototype.Certificate21.childrenD_697_i0 line 110
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_697_i0 line 111
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_697_i0 line 112
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_697_i0 line 113
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_697_i0 line 114
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_697_i0 line 115
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_697_i0 line 121
  51. def OAI.SnakyPrototype.Certificate21.required_697 line 126
  52. def OAI.SnakyPrototype.Certificate21.envelope_697 line 127
  53. def OAI.SnakyPrototype.Certificate21.childrenC_697 line 128
  54. def OAI.SnakyPrototype.Certificate21.childrenD_697 line 129
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_697 line 130
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_697 line 131
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_697 line 132
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_697 line 133
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_697 line 134
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_697 line 141
  61. def OAI.SnakyPrototype.Certificate21.required_705_i1 line 146
  62. def OAI.SnakyPrototype.Certificate21.envelope_705_i1 line 147
  63. def OAI.SnakyPrototype.Certificate21.childrenC_705_i1 line 148
  64. def OAI.SnakyPrototype.Certificate21.childrenD_705_i1 line 149
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_705_i1 line 150
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_705_i1 line 151
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_705_i1 line 152
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_705_i1 line 153
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_705_i1 line 154
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_705_i1 line 163
  71. def OAI.SnakyPrototype.Certificate21.required_705_i0 line 168
  72. def OAI.SnakyPrototype.Certificate21.envelope_705_i0 line 169
  73. def OAI.SnakyPrototype.Certificate21.childrenC_705_i0 line 170
  74. def OAI.SnakyPrototype.Certificate21.childrenD_705_i0 line 171
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_705_i0 line 172
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_705_i0 line 173
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_705_i0 line 174
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_705_i0 line 175
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_705_i0 line 176
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_705_i0 line 183
  81. def OAI.SnakyPrototype.Certificate21.required_705_i4 line 188
  82. def OAI.SnakyPrototype.Certificate21.envelope_705_i4 line 189
  83. def OAI.SnakyPrototype.Certificate21.childrenC_705_i4 line 190
  84. def OAI.SnakyPrototype.Certificate21.childrenD_705_i4 line 191
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_705_i4 line 192
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_705_i4 line 193
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_705_i4 line 194
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_705_i4 line 195
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_705_i4 line 196
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_705_i4 line 201
  91. def OAI.SnakyPrototype.Certificate21.required_705_i3 line 206
  92. def OAI.SnakyPrototype.Certificate21.envelope_705_i3 line 207
  93. def OAI.SnakyPrototype.Certificate21.childrenC_705_i3 line 208
  94. def OAI.SnakyPrototype.Certificate21.childrenD_705_i3 line 209
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_705_i3 line 210
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_705_i3 line 211
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_705_i3 line 212
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_705_i3 line 213
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_705_i3 line 214
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_705_i3 line 221
  101. def OAI.SnakyPrototype.Certificate21.required_705_i2 line 226
  102. def OAI.SnakyPrototype.Certificate21.envelope_705_i2 line 227
  103. def OAI.SnakyPrototype.Certificate21.childrenC_705_i2 line 228
  104. def OAI.SnakyPrototype.Certificate21.childrenD_705_i2 line 229
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_705_i2 line 230
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_705_i2 line 231
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_705_i2 line 232
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_705_i2 line 233
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_705_i2 line 234
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_705_i2 line 243
  111. def OAI.SnakyPrototype.Certificate21.required_705 line 248
  112. def OAI.SnakyPrototype.Certificate21.envelope_705 line 249
  113. def OAI.SnakyPrototype.Certificate21.childrenC_705 line 250
  114. def OAI.SnakyPrototype.Certificate21.childrenD_705 line 251
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_705 line 252
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_705 line 253
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_705 line 254
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_705 line 255
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_705 line 256
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_705 line 266
  121. def OAI.SnakyPrototype.Certificate21.required_711_i0 line 271
  122. def OAI.SnakyPrototype.Certificate21.envelope_711_i0 line 272
  123. def OAI.SnakyPrototype.Certificate21.childrenC_711_i0 line 273
  124. def OAI.SnakyPrototype.Certificate21.childrenD_711_i0 line 274
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_711_i0 line 275
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_711_i0 line 276
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_711_i0 line 277
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_711_i0 line 278
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_711_i0 line 279
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_711_i0 line 288
  131. def OAI.SnakyPrototype.Certificate21.required_711 line 293
  132. def OAI.SnakyPrototype.Certificate21.envelope_711 line 294
  133. def OAI.SnakyPrototype.Certificate21.childrenC_711 line 295
  134. def OAI.SnakyPrototype.Certificate21.childrenD_711 line 296
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_711 line 297
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_711 line 298
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_711 line 299
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_711 line 300
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_711 line 301
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_711 line 313
  141. def OAI.SnakyPrototype.Certificate21.height_697_i4 line 318
  142. def OAI.SnakyPrototype.Certificate21.childrenH_697_i4 line 319
  143. theorem OAI.SnakyPrototype.Certificate21.height_exact_697_i4 line 320
  144. theorem OAI.SnakyPrototype.Certificate21.required_origin_697_i4 line 321
  145. theorem OAI.SnakyPrototype.Certificate21.required_exact_697_i4 line 323
  146. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_697_i4 line 327
  147. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_697_i4 line 329
  148. def OAI.SnakyPrototype.Certificate21.checked_697_i4 line 333
  149. def OAI.SnakyPrototype.Certificate21.height_697_i3 line 341
  150. def OAI.SnakyPrototype.Certificate21.childrenH_697_i3 line 342
  151. theorem OAI.SnakyPrototype.Certificate21.height_exact_697_i3 line 343
  152. theorem OAI.SnakyPrototype.Certificate21.required_origin_697_i3 line 344
  153. theorem OAI.SnakyPrototype.Certificate21.required_exact_697_i3 line 346
  154. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_697_i3 line 350
  155. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_697_i3 line 352
  156. def OAI.SnakyPrototype.Certificate21.checked_697_i3 line 356
  157. def OAI.SnakyPrototype.Certificate21.height_697_i2 line 364
  158. def OAI.SnakyPrototype.Certificate21.childrenH_697_i2 line 365
  159. theorem OAI.SnakyPrototype.Certificate21.height_exact_697_i2 line 366
  160. theorem OAI.SnakyPrototype.Certificate21.required_origin_697_i2 line 367
  161. theorem OAI.SnakyPrototype.Certificate21.required_exact_697_i2 line 369
  162. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_697_i2 line 373
  163. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_697_i2 line 375
  164. def OAI.SnakyPrototype.Certificate21.checked_697_i2 line 379
  165. def OAI.SnakyPrototype.Certificate21.height_697_i1 line 387
  166. def OAI.SnakyPrototype.Certificate21.childrenH_697_i1 line 388
  167. theorem OAI.SnakyPrototype.Certificate21.height_exact_697_i1 line 389
  168. theorem OAI.SnakyPrototype.Certificate21.required_origin_697_i1 line 390
  169. theorem OAI.SnakyPrototype.Certificate21.required_exact_697_i1 line 392
  170. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_697_i1 line 396
  171. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_697_i1 line 398
  172. def OAI.SnakyPrototype.Certificate21.checked_697_i1 line 402
  173. def OAI.SnakyPrototype.Certificate21.height_697_i0 line 410
  174. def OAI.SnakyPrototype.Certificate21.childrenH_697_i0 line 411
  175. theorem OAI.SnakyPrototype.Certificate21.height_exact_697_i0 line 412
  176. theorem OAI.SnakyPrototype.Certificate21.required_origin_697_i0 line 413
  177. theorem OAI.SnakyPrototype.Certificate21.required_exact_697_i0 line 415
  178. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_697_i0 line 419
  179. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_697_i0 line 421
  180. def OAI.SnakyPrototype.Certificate21.checked_697_i0 line 425
  181. def OAI.SnakyPrototype.Certificate21.height_697 line 433
  182. def OAI.SnakyPrototype.Certificate21.childrenH_697 line 434
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_697 line 435
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_697 line 436
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_697 line 438
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_697 line 442
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_697 line 444
  188. def OAI.SnakyPrototype.Certificate21.checked_697 line 448
  189. def OAI.SnakyPrototype.Certificate21.height_705_i1 line 456
  190. def OAI.SnakyPrototype.Certificate21.childrenH_705_i1 line 457
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_705_i1 line 458
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_705_i1 line 459
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_705_i1 line 461
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_705_i1 line 465
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_705_i1 line 467
  196. def OAI.SnakyPrototype.Certificate21.checked_705_i1 line 471
  197. def OAI.SnakyPrototype.Certificate21.height_705_i0 line 479
  198. def OAI.SnakyPrototype.Certificate21.childrenH_705_i0 line 480
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_705_i0 line 481
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_705_i0 line 482
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_705_i0 line 484
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_705_i0 line 488
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_705_i0 line 490
  204. def OAI.SnakyPrototype.Certificate21.checked_705_i0 line 494
  205. def OAI.SnakyPrototype.Certificate21.height_705_i4 line 502
  206. def OAI.SnakyPrototype.Certificate21.childrenH_705_i4 line 503
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_705_i4 line 504
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_705_i4 line 505
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_705_i4 line 507
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_705_i4 line 511
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_705_i4 line 513
  212. def OAI.SnakyPrototype.Certificate21.checked_705_i4 line 517
  213. def OAI.SnakyPrototype.Certificate21.height_705_i3 line 525
  214. def OAI.SnakyPrototype.Certificate21.childrenH_705_i3 line 526
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_705_i3 line 527
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_705_i3 line 528
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_705_i3 line 530
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_705_i3 line 534
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_705_i3 line 536
  220. def OAI.SnakyPrototype.Certificate21.checked_705_i3 line 540
  221. def OAI.SnakyPrototype.Certificate21.height_705_i2 line 548
  222. def OAI.SnakyPrototype.Certificate21.childrenH_705_i2 line 549
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_705_i2 line 550
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_705_i2 line 551
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_705_i2 line 553
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_705_i2 line 557
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_705_i2 line 559
  228. def OAI.SnakyPrototype.Certificate21.checked_705_i2 line 563
  229. def OAI.SnakyPrototype.Certificate21.height_705 line 571
  230. def OAI.SnakyPrototype.Certificate21.childrenH_705 line 572
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_705 line 573
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_705 line 574
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_705 line 576
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_705 line 580
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_705 line 582
  236. def OAI.SnakyPrototype.Certificate21.checked_705 line 586
  237. def OAI.SnakyPrototype.Certificate21.height_711_i0 line 594
  238. def OAI.SnakyPrototype.Certificate21.childrenH_711_i0 line 595
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_711_i0 line 596
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_711_i0 line 597
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_711_i0 line 599
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_711_i0 line 603
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_711_i0 line 605
  244. def OAI.SnakyPrototype.Certificate21.checked_711_i0 line 609
  245. def OAI.SnakyPrototype.Certificate21.height_711 line 617
  246. def OAI.SnakyPrototype.Certificate21.childrenH_711 line 618
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_711 line 619
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_711 line 620
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_711 line 622
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_711 line 626
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_711 line 628
  252. def OAI.SnakyPrototype.Certificate21.checked_711 line 632