OAI/GameTheory/SnakyTwentyOne/Cards/Height20Part01.lean

GitHub source file

198 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_708_i2 line 39
  2. def OAI.SnakyPrototype.Certificate21.envelope_708_i2 line 40
  3. def OAI.SnakyPrototype.Certificate21.childrenC_708_i2 line 41
  4. def OAI.SnakyPrototype.Certificate21.childrenD_708_i2 line 42
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i2 line 43
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i2 line 44
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i2 line 45
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i2 line 46
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i2 line 47
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i2 line 53
  11. def OAI.SnakyPrototype.Certificate21.required_708_i4 line 58
  12. def OAI.SnakyPrototype.Certificate21.envelope_708_i4 line 59
  13. def OAI.SnakyPrototype.Certificate21.childrenC_708_i4 line 60
  14. def OAI.SnakyPrototype.Certificate21.childrenD_708_i4 line 61
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i4 line 62
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i4 line 63
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i4 line 64
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i4 line 65
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i4 line 66
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i4 line 72
  21. def OAI.SnakyPrototype.Certificate21.required_708_i3 line 77
  22. def OAI.SnakyPrototype.Certificate21.envelope_708_i3 line 78
  23. def OAI.SnakyPrototype.Certificate21.childrenC_708_i3 line 79
  24. def OAI.SnakyPrototype.Certificate21.childrenD_708_i3 line 80
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i3 line 81
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i3 line 82
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i3 line 83
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i3 line 84
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i3 line 85
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i3 line 91
  31. def OAI.SnakyPrototype.Certificate21.required_708_i1 line 96
  32. def OAI.SnakyPrototype.Certificate21.envelope_708_i1 line 97
  33. def OAI.SnakyPrototype.Certificate21.childrenC_708_i1 line 98
  34. def OAI.SnakyPrototype.Certificate21.childrenD_708_i1 line 99
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i1 line 100
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i1 line 101
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i1 line 102
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i1 line 103
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i1 line 104
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i1 line 113
  41. def OAI.SnakyPrototype.Certificate21.required_708_i5 line 118
  42. def OAI.SnakyPrototype.Certificate21.envelope_708_i5 line 119
  43. def OAI.SnakyPrototype.Certificate21.childrenC_708_i5 line 120
  44. def OAI.SnakyPrototype.Certificate21.childrenD_708_i5 line 121
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i5 line 122
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i5 line 123
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i5 line 124
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i5 line 125
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i5 line 126
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i5 line 132
  51. def OAI.SnakyPrototype.Certificate21.required_708_i0 line 137
  52. def OAI.SnakyPrototype.Certificate21.envelope_708_i0 line 138
  53. def OAI.SnakyPrototype.Certificate21.childrenC_708_i0 line 139
  54. def OAI.SnakyPrototype.Certificate21.childrenD_708_i0 line 140
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i0 line 141
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i0 line 142
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i0 line 143
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i0 line 144
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i0 line 145
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i0 line 155
  61. def OAI.SnakyPrototype.Certificate21.required_708_i6 line 160
  62. def OAI.SnakyPrototype.Certificate21.envelope_708_i6 line 161
  63. def OAI.SnakyPrototype.Certificate21.childrenC_708_i6 line 162
  64. def OAI.SnakyPrototype.Certificate21.childrenD_708_i6 line 163
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i6 line 164
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i6 line 165
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i6 line 166
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i6 line 167
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i6 line 168
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i6 line 178
  71. def OAI.SnakyPrototype.Certificate21.required_708_i7 line 183
  72. def OAI.SnakyPrototype.Certificate21.envelope_708_i7 line 184
  73. def OAI.SnakyPrototype.Certificate21.childrenC_708_i7 line 185
  74. def OAI.SnakyPrototype.Certificate21.childrenD_708_i7 line 186
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_708_i7 line 187
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708_i7 line 188
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708_i7 line 189
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708_i7 line 190
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_708_i7 line 191
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_708_i7 line 200
  81. def OAI.SnakyPrototype.Certificate21.required_708 line 205
  82. def OAI.SnakyPrototype.Certificate21.envelope_708 line 206
  83. def OAI.SnakyPrototype.Certificate21.childrenC_708 line 207
  84. def OAI.SnakyPrototype.Certificate21.childrenD_708 line 208
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_708 line 209
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_708 line 210
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_708 line 211
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_708 line 212
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_708 line 213
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_708 line 232
  91. def OAI.SnakyPrototype.Certificate21.required_725 line 237
  92. def OAI.SnakyPrototype.Certificate21.envelope_725 line 238
  93. def OAI.SnakyPrototype.Certificate21.childrenC_725 line 239
  94. def OAI.SnakyPrototype.Certificate21.childrenD_725 line 240
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_725 line 241
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_725 line 242
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_725 line 243
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_725 line 244
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_725 line 245
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_725 line 264
  101. def OAI.SnakyPrototype.Certificate21.required_726 line 269
  102. def OAI.SnakyPrototype.Certificate21.envelope_726 line 270
  103. def OAI.SnakyPrototype.Certificate21.childrenC_726 line 271
  104. def OAI.SnakyPrototype.Certificate21.childrenD_726 line 272
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_726 line 273
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_726 line 274
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_726 line 275
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_726 line 276
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_726 line 277
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_726 line 296
  111. def OAI.SnakyPrototype.Certificate21.height_708_i2 line 301
  112. def OAI.SnakyPrototype.Certificate21.childrenH_708_i2 line 302
  113. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i2 line 303
  114. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i2 line 304
  115. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i2 line 306
  116. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i2 line 310
  117. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i2 line 312
  118. def OAI.SnakyPrototype.Certificate21.checked_708_i2 line 316
  119. def OAI.SnakyPrototype.Certificate21.height_708_i4 line 324
  120. def OAI.SnakyPrototype.Certificate21.childrenH_708_i4 line 325
  121. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i4 line 326
  122. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i4 line 327
  123. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i4 line 329
  124. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i4 line 333
  125. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i4 line 335
  126. def OAI.SnakyPrototype.Certificate21.checked_708_i4 line 339
  127. def OAI.SnakyPrototype.Certificate21.height_708_i3 line 347
  128. def OAI.SnakyPrototype.Certificate21.childrenH_708_i3 line 348
  129. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i3 line 349
  130. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i3 line 350
  131. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i3 line 352
  132. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i3 line 356
  133. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i3 line 358
  134. def OAI.SnakyPrototype.Certificate21.checked_708_i3 line 362
  135. def OAI.SnakyPrototype.Certificate21.height_708_i1 line 370
  136. def OAI.SnakyPrototype.Certificate21.childrenH_708_i1 line 371
  137. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i1 line 372
  138. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i1 line 373
  139. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i1 line 375
  140. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i1 line 379
  141. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i1 line 381
  142. def OAI.SnakyPrototype.Certificate21.checked_708_i1 line 385
  143. def OAI.SnakyPrototype.Certificate21.height_708_i5 line 393
  144. def OAI.SnakyPrototype.Certificate21.childrenH_708_i5 line 394
  145. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i5 line 395
  146. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i5 line 396
  147. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i5 line 398
  148. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i5 line 402
  149. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i5 line 404
  150. def OAI.SnakyPrototype.Certificate21.checked_708_i5 line 408
  151. def OAI.SnakyPrototype.Certificate21.height_708_i0 line 416
  152. def OAI.SnakyPrototype.Certificate21.childrenH_708_i0 line 417
  153. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i0 line 418
  154. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i0 line 419
  155. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i0 line 421
  156. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i0 line 425
  157. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i0 line 427
  158. def OAI.SnakyPrototype.Certificate21.checked_708_i0 line 431
  159. def OAI.SnakyPrototype.Certificate21.height_708_i6 line 439
  160. def OAI.SnakyPrototype.Certificate21.childrenH_708_i6 line 440
  161. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i6 line 441
  162. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i6 line 442
  163. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i6 line 444
  164. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i6 line 448
  165. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i6 line 450
  166. def OAI.SnakyPrototype.Certificate21.checked_708_i6 line 454
  167. def OAI.SnakyPrototype.Certificate21.height_708_i7 line 462
  168. def OAI.SnakyPrototype.Certificate21.childrenH_708_i7 line 463
  169. theorem OAI.SnakyPrototype.Certificate21.height_exact_708_i7 line 464
  170. theorem OAI.SnakyPrototype.Certificate21.required_origin_708_i7 line 465
  171. theorem OAI.SnakyPrototype.Certificate21.required_exact_708_i7 line 467
  172. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708_i7 line 471
  173. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708_i7 line 473
  174. def OAI.SnakyPrototype.Certificate21.checked_708_i7 line 477
  175. def OAI.SnakyPrototype.Certificate21.height_708 line 485
  176. def OAI.SnakyPrototype.Certificate21.childrenH_708 line 486
  177. theorem OAI.SnakyPrototype.Certificate21.height_exact_708 line 487
  178. theorem OAI.SnakyPrototype.Certificate21.required_origin_708 line 488
  179. theorem OAI.SnakyPrototype.Certificate21.required_exact_708 line 490
  180. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_708 line 494
  181. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_708 line 496
  182. def OAI.SnakyPrototype.Certificate21.checked_708 line 500
  183. def OAI.SnakyPrototype.Certificate21.height_725 line 508
  184. def OAI.SnakyPrototype.Certificate21.childrenH_725 line 509
  185. theorem OAI.SnakyPrototype.Certificate21.height_exact_725 line 510
  186. theorem OAI.SnakyPrototype.Certificate21.required_origin_725 line 511
  187. theorem OAI.SnakyPrototype.Certificate21.required_exact_725 line 513
  188. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_725 line 517
  189. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_725 line 519
  190. def OAI.SnakyPrototype.Certificate21.checked_725 line 523
  191. def OAI.SnakyPrototype.Certificate21.height_726 line 531
  192. def OAI.SnakyPrototype.Certificate21.childrenH_726 line 532
  193. theorem OAI.SnakyPrototype.Certificate21.height_exact_726 line 533
  194. theorem OAI.SnakyPrototype.Certificate21.required_origin_726 line 534
  195. theorem OAI.SnakyPrototype.Certificate21.required_exact_726 line 536
  196. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_726 line 540
  197. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_726 line 542
  198. def OAI.SnakyPrototype.Certificate21.checked_726 line 546