OAI/GameTheory/SnakyTwentyOne/Cards/Height09Part05.lean

GitHub source file

252 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_574_i1 line 21
  2. def OAI.SnakyPrototype.Certificate21.envelope_574_i1 line 22
  3. def OAI.SnakyPrototype.Certificate21.childrenC_574_i1 line 23
  4. def OAI.SnakyPrototype.Certificate21.childrenD_574_i1 line 24
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_574_i1 line 25
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574_i1 line 26
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574_i1 line 27
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574_i1 line 28
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_574_i1 line 29
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_574_i1 line 34
  11. def OAI.SnakyPrototype.Certificate21.required_574_i3 line 39
  12. def OAI.SnakyPrototype.Certificate21.envelope_574_i3 line 40
  13. def OAI.SnakyPrototype.Certificate21.childrenC_574_i3 line 41
  14. def OAI.SnakyPrototype.Certificate21.childrenD_574_i3 line 42
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_574_i3 line 43
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574_i3 line 44
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574_i3 line 45
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574_i3 line 46
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_574_i3 line 47
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_574_i3 line 52
  21. def OAI.SnakyPrototype.Certificate21.required_574_i2 line 57
  22. def OAI.SnakyPrototype.Certificate21.envelope_574_i2 line 58
  23. def OAI.SnakyPrototype.Certificate21.childrenC_574_i2 line 59
  24. def OAI.SnakyPrototype.Certificate21.childrenD_574_i2 line 60
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_574_i2 line 61
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574_i2 line 62
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574_i2 line 63
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574_i2 line 64
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_574_i2 line 65
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_574_i2 line 70
  31. def OAI.SnakyPrototype.Certificate21.required_574_i5 line 75
  32. def OAI.SnakyPrototype.Certificate21.envelope_574_i5 line 76
  33. def OAI.SnakyPrototype.Certificate21.childrenC_574_i5 line 77
  34. def OAI.SnakyPrototype.Certificate21.childrenD_574_i5 line 78
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_574_i5 line 79
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574_i5 line 80
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574_i5 line 81
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574_i5 line 82
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_574_i5 line 83
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_574_i5 line 88
  41. def OAI.SnakyPrototype.Certificate21.required_574_i4 line 93
  42. def OAI.SnakyPrototype.Certificate21.envelope_574_i4 line 94
  43. def OAI.SnakyPrototype.Certificate21.childrenC_574_i4 line 95
  44. def OAI.SnakyPrototype.Certificate21.childrenD_574_i4 line 96
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_574_i4 line 97
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574_i4 line 98
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574_i4 line 99
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574_i4 line 100
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_574_i4 line 101
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_574_i4 line 107
  51. def OAI.SnakyPrototype.Certificate21.required_574_i0 line 112
  52. def OAI.SnakyPrototype.Certificate21.envelope_574_i0 line 113
  53. def OAI.SnakyPrototype.Certificate21.childrenC_574_i0 line 114
  54. def OAI.SnakyPrototype.Certificate21.childrenD_574_i0 line 115
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_574_i0 line 116
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574_i0 line 117
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574_i0 line 118
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574_i0 line 119
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_574_i0 line 120
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_574_i0 line 127
  61. def OAI.SnakyPrototype.Certificate21.required_574 line 132
  62. def OAI.SnakyPrototype.Certificate21.envelope_574 line 133
  63. def OAI.SnakyPrototype.Certificate21.childrenC_574 line 134
  64. def OAI.SnakyPrototype.Certificate21.childrenD_574 line 135
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_574 line 136
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_574 line 137
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_574 line 138
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_574 line 139
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_574 line 140
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_574 line 149
  71. def OAI.SnakyPrototype.Certificate21.required_577_i1 line 154
  72. def OAI.SnakyPrototype.Certificate21.envelope_577_i1 line 155
  73. def OAI.SnakyPrototype.Certificate21.childrenC_577_i1 line 156
  74. def OAI.SnakyPrototype.Certificate21.childrenD_577_i1 line 157
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_577_i1 line 158
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_577_i1 line 159
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_577_i1 line 160
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_577_i1 line 161
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_577_i1 line 162
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_577_i1 line 167
  81. def OAI.SnakyPrototype.Certificate21.required_577_i0 line 172
  82. def OAI.SnakyPrototype.Certificate21.envelope_577_i0 line 173
  83. def OAI.SnakyPrototype.Certificate21.childrenC_577_i0 line 174
  84. def OAI.SnakyPrototype.Certificate21.childrenD_577_i0 line 175
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_577_i0 line 176
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_577_i0 line 177
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_577_i0 line 178
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_577_i0 line 179
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_577_i0 line 180
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_577_i0 line 185
  91. def OAI.SnakyPrototype.Certificate21.required_577 line 190
  92. def OAI.SnakyPrototype.Certificate21.envelope_577 line 191
  93. def OAI.SnakyPrototype.Certificate21.childrenC_577 line 192
  94. def OAI.SnakyPrototype.Certificate21.childrenD_577 line 193
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_577 line 194
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_577 line 195
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_577 line 196
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_577 line 197
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_577 line 198
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_577 line 203
  101. def OAI.SnakyPrototype.Certificate21.required_584_i1 line 208
  102. def OAI.SnakyPrototype.Certificate21.envelope_584_i1 line 209
  103. def OAI.SnakyPrototype.Certificate21.childrenC_584_i1 line 210
  104. def OAI.SnakyPrototype.Certificate21.childrenD_584_i1 line 211
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_584_i1 line 212
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_584_i1 line 213
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_584_i1 line 214
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_584_i1 line 215
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_584_i1 line 216
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_584_i1 line 221
  111. def OAI.SnakyPrototype.Certificate21.required_584_i2 line 226
  112. def OAI.SnakyPrototype.Certificate21.envelope_584_i2 line 227
  113. def OAI.SnakyPrototype.Certificate21.childrenC_584_i2 line 228
  114. def OAI.SnakyPrototype.Certificate21.childrenD_584_i2 line 229
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_584_i2 line 230
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_584_i2 line 231
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_584_i2 line 232
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_584_i2 line 233
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_584_i2 line 234
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_584_i2 line 239
  121. def OAI.SnakyPrototype.Certificate21.required_584_i0 line 244
  122. def OAI.SnakyPrototype.Certificate21.envelope_584_i0 line 245
  123. def OAI.SnakyPrototype.Certificate21.childrenC_584_i0 line 246
  124. def OAI.SnakyPrototype.Certificate21.childrenD_584_i0 line 247
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_584_i0 line 248
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_584_i0 line 249
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_584_i0 line 250
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_584_i0 line 251
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_584_i0 line 252
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_584_i0 line 258
  131. def OAI.SnakyPrototype.Certificate21.required_584 line 263
  132. def OAI.SnakyPrototype.Certificate21.envelope_584 line 264
  133. def OAI.SnakyPrototype.Certificate21.childrenC_584 line 265
  134. def OAI.SnakyPrototype.Certificate21.childrenD_584 line 266
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_584 line 267
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_584 line 268
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_584 line 269
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_584 line 270
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_584 line 271
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_584 line 276
  141. def OAI.SnakyPrototype.Certificate21.height_574_i1 line 281
  142. def OAI.SnakyPrototype.Certificate21.childrenH_574_i1 line 282
  143. theorem OAI.SnakyPrototype.Certificate21.height_exact_574_i1 line 283
  144. theorem OAI.SnakyPrototype.Certificate21.required_origin_574_i1 line 284
  145. theorem OAI.SnakyPrototype.Certificate21.required_exact_574_i1 line 286
  146. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574_i1 line 290
  147. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574_i1 line 292
  148. def OAI.SnakyPrototype.Certificate21.checked_574_i1 line 296
  149. def OAI.SnakyPrototype.Certificate21.height_574_i3 line 304
  150. def OAI.SnakyPrototype.Certificate21.childrenH_574_i3 line 305
  151. theorem OAI.SnakyPrototype.Certificate21.height_exact_574_i3 line 306
  152. theorem OAI.SnakyPrototype.Certificate21.required_origin_574_i3 line 307
  153. theorem OAI.SnakyPrototype.Certificate21.required_exact_574_i3 line 309
  154. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574_i3 line 313
  155. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574_i3 line 315
  156. def OAI.SnakyPrototype.Certificate21.checked_574_i3 line 319
  157. def OAI.SnakyPrototype.Certificate21.height_574_i2 line 327
  158. def OAI.SnakyPrototype.Certificate21.childrenH_574_i2 line 328
  159. theorem OAI.SnakyPrototype.Certificate21.height_exact_574_i2 line 329
  160. theorem OAI.SnakyPrototype.Certificate21.required_origin_574_i2 line 330
  161. theorem OAI.SnakyPrototype.Certificate21.required_exact_574_i2 line 332
  162. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574_i2 line 336
  163. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574_i2 line 338
  164. def OAI.SnakyPrototype.Certificate21.checked_574_i2 line 342
  165. def OAI.SnakyPrototype.Certificate21.height_574_i5 line 350
  166. def OAI.SnakyPrototype.Certificate21.childrenH_574_i5 line 351
  167. theorem OAI.SnakyPrototype.Certificate21.height_exact_574_i5 line 352
  168. theorem OAI.SnakyPrototype.Certificate21.required_origin_574_i5 line 353
  169. theorem OAI.SnakyPrototype.Certificate21.required_exact_574_i5 line 355
  170. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574_i5 line 359
  171. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574_i5 line 361
  172. def OAI.SnakyPrototype.Certificate21.checked_574_i5 line 365
  173. def OAI.SnakyPrototype.Certificate21.height_574_i4 line 373
  174. def OAI.SnakyPrototype.Certificate21.childrenH_574_i4 line 374
  175. theorem OAI.SnakyPrototype.Certificate21.height_exact_574_i4 line 375
  176. theorem OAI.SnakyPrototype.Certificate21.required_origin_574_i4 line 376
  177. theorem OAI.SnakyPrototype.Certificate21.required_exact_574_i4 line 378
  178. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574_i4 line 382
  179. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574_i4 line 384
  180. def OAI.SnakyPrototype.Certificate21.checked_574_i4 line 388
  181. def OAI.SnakyPrototype.Certificate21.height_574_i0 line 396
  182. def OAI.SnakyPrototype.Certificate21.childrenH_574_i0 line 397
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_574_i0 line 398
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_574_i0 line 399
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_574_i0 line 401
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574_i0 line 405
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574_i0 line 407
  188. def OAI.SnakyPrototype.Certificate21.checked_574_i0 line 411
  189. def OAI.SnakyPrototype.Certificate21.height_574 line 419
  190. def OAI.SnakyPrototype.Certificate21.childrenH_574 line 420
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_574 line 421
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_574 line 422
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_574 line 424
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_574 line 428
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_574 line 430
  196. def OAI.SnakyPrototype.Certificate21.checked_574 line 434
  197. def OAI.SnakyPrototype.Certificate21.height_577_i1 line 442
  198. def OAI.SnakyPrototype.Certificate21.childrenH_577_i1 line 443
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_577_i1 line 444
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_577_i1 line 445
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_577_i1 line 447
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_577_i1 line 451
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_577_i1 line 453
  204. def OAI.SnakyPrototype.Certificate21.checked_577_i1 line 457
  205. def OAI.SnakyPrototype.Certificate21.height_577_i0 line 465
  206. def OAI.SnakyPrototype.Certificate21.childrenH_577_i0 line 466
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_577_i0 line 467
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_577_i0 line 468
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_577_i0 line 470
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_577_i0 line 474
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_577_i0 line 476
  212. def OAI.SnakyPrototype.Certificate21.checked_577_i0 line 480
  213. def OAI.SnakyPrototype.Certificate21.height_577 line 488
  214. def OAI.SnakyPrototype.Certificate21.childrenH_577 line 489
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_577 line 490
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_577 line 491
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_577 line 493
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_577 line 497
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_577 line 499
  220. def OAI.SnakyPrototype.Certificate21.checked_577 line 503
  221. def OAI.SnakyPrototype.Certificate21.height_584_i1 line 511
  222. def OAI.SnakyPrototype.Certificate21.childrenH_584_i1 line 512
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_584_i1 line 513
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_584_i1 line 514
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_584_i1 line 516
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_584_i1 line 520
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_584_i1 line 522
  228. def OAI.SnakyPrototype.Certificate21.checked_584_i1 line 526
  229. def OAI.SnakyPrototype.Certificate21.height_584_i2 line 534
  230. def OAI.SnakyPrototype.Certificate21.childrenH_584_i2 line 535
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_584_i2 line 536
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_584_i2 line 537
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_584_i2 line 539
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_584_i2 line 543
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_584_i2 line 545
  236. def OAI.SnakyPrototype.Certificate21.checked_584_i2 line 549
  237. def OAI.SnakyPrototype.Certificate21.height_584_i0 line 557
  238. def OAI.SnakyPrototype.Certificate21.childrenH_584_i0 line 558
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_584_i0 line 559
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_584_i0 line 560
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_584_i0 line 562
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_584_i0 line 566
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_584_i0 line 568
  244. def OAI.SnakyPrototype.Certificate21.checked_584_i0 line 572
  245. def OAI.SnakyPrototype.Certificate21.height_584 line 580
  246. def OAI.SnakyPrototype.Certificate21.childrenH_584 line 581
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_584 line 582
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_584 line 583
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_584 line 585
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_584 line 589
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_584 line 591
  252. def OAI.SnakyPrototype.Certificate21.checked_584 line 595