OAI/GameTheory/SnakyTwentyOne/Cards/Height17Part02.lean

GitHub source file

180 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_707_i0 line 28
  2. def OAI.SnakyPrototype.Certificate21.envelope_707_i0 line 29
  3. def OAI.SnakyPrototype.Certificate21.childrenC_707_i0 line 30
  4. def OAI.SnakyPrototype.Certificate21.childrenD_707_i0 line 31
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i0 line 32
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i0 line 33
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i0 line 34
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i0 line 35
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i0 line 36
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i0 line 46
  11. def OAI.SnakyPrototype.Certificate21.required_707_i2 line 51
  12. def OAI.SnakyPrototype.Certificate21.envelope_707_i2 line 52
  13. def OAI.SnakyPrototype.Certificate21.childrenC_707_i2 line 53
  14. def OAI.SnakyPrototype.Certificate21.childrenD_707_i2 line 54
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i2 line 55
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i2 line 56
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i2 line 57
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i2 line 58
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i2 line 59
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i2 line 65
  21. def OAI.SnakyPrototype.Certificate21.required_707_i1 line 70
  22. def OAI.SnakyPrototype.Certificate21.envelope_707_i1 line 71
  23. def OAI.SnakyPrototype.Certificate21.childrenC_707_i1 line 72
  24. def OAI.SnakyPrototype.Certificate21.childrenD_707_i1 line 73
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i1 line 74
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i1 line 75
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i1 line 76
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i1 line 77
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i1 line 78
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i1 line 85
  31. def OAI.SnakyPrototype.Certificate21.required_707_i4 line 90
  32. def OAI.SnakyPrototype.Certificate21.envelope_707_i4 line 91
  33. def OAI.SnakyPrototype.Certificate21.childrenC_707_i4 line 92
  34. def OAI.SnakyPrototype.Certificate21.childrenD_707_i4 line 93
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i4 line 94
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i4 line 95
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i4 line 96
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i4 line 97
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i4 line 98
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i4 line 105
  41. def OAI.SnakyPrototype.Certificate21.required_707_i3 line 110
  42. def OAI.SnakyPrototype.Certificate21.envelope_707_i3 line 111
  43. def OAI.SnakyPrototype.Certificate21.childrenC_707_i3 line 112
  44. def OAI.SnakyPrototype.Certificate21.childrenD_707_i3 line 113
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i3 line 114
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i3 line 115
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i3 line 116
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i3 line 117
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i3 line 118
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i3 line 126
  51. def OAI.SnakyPrototype.Certificate21.required_707_i6 line 131
  52. def OAI.SnakyPrototype.Certificate21.envelope_707_i6 line 132
  53. def OAI.SnakyPrototype.Certificate21.childrenC_707_i6 line 133
  54. def OAI.SnakyPrototype.Certificate21.childrenD_707_i6 line 134
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i6 line 135
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i6 line 136
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i6 line 137
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i6 line 138
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i6 line 139
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i6 line 146
  61. def OAI.SnakyPrototype.Certificate21.required_707_i5 line 151
  62. def OAI.SnakyPrototype.Certificate21.envelope_707_i5 line 152
  63. def OAI.SnakyPrototype.Certificate21.childrenC_707_i5 line 153
  64. def OAI.SnakyPrototype.Certificate21.childrenD_707_i5 line 154
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i5 line 155
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i5 line 156
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i5 line 157
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i5 line 158
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i5 line 159
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i5 line 166
  71. def OAI.SnakyPrototype.Certificate21.required_707_i7 line 171
  72. def OAI.SnakyPrototype.Certificate21.envelope_707_i7 line 172
  73. def OAI.SnakyPrototype.Certificate21.childrenC_707_i7 line 173
  74. def OAI.SnakyPrototype.Certificate21.childrenD_707_i7 line 174
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i7 line 175
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i7 line 176
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i7 line 177
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i7 line 178
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i7 line 179
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i7 line 189
  81. def OAI.SnakyPrototype.Certificate21.required_707_i8 line 194
  82. def OAI.SnakyPrototype.Certificate21.envelope_707_i8 line 195
  83. def OAI.SnakyPrototype.Certificate21.childrenC_707_i8 line 196
  84. def OAI.SnakyPrototype.Certificate21.childrenD_707_i8 line 197
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_707_i8 line 198
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707_i8 line 199
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707_i8 line 200
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707_i8 line 201
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_707_i8 line 202
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_707_i8 line 211
  91. def OAI.SnakyPrototype.Certificate21.required_707 line 216
  92. def OAI.SnakyPrototype.Certificate21.envelope_707 line 217
  93. def OAI.SnakyPrototype.Certificate21.childrenC_707 line 218
  94. def OAI.SnakyPrototype.Certificate21.childrenD_707 line 219
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_707 line 220
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_707 line 221
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_707 line 222
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_707 line 223
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_707 line 224
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_707 line 240
  101. def OAI.SnakyPrototype.Certificate21.height_707_i0 line 245
  102. def OAI.SnakyPrototype.Certificate21.childrenH_707_i0 line 246
  103. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i0 line 247
  104. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i0 line 248
  105. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i0 line 250
  106. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i0 line 254
  107. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i0 line 256
  108. def OAI.SnakyPrototype.Certificate21.checked_707_i0 line 260
  109. def OAI.SnakyPrototype.Certificate21.height_707_i2 line 268
  110. def OAI.SnakyPrototype.Certificate21.childrenH_707_i2 line 269
  111. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i2 line 270
  112. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i2 line 271
  113. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i2 line 273
  114. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i2 line 277
  115. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i2 line 279
  116. def OAI.SnakyPrototype.Certificate21.checked_707_i2 line 283
  117. def OAI.SnakyPrototype.Certificate21.height_707_i1 line 291
  118. def OAI.SnakyPrototype.Certificate21.childrenH_707_i1 line 292
  119. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i1 line 293
  120. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i1 line 294
  121. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i1 line 296
  122. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i1 line 300
  123. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i1 line 302
  124. def OAI.SnakyPrototype.Certificate21.checked_707_i1 line 306
  125. def OAI.SnakyPrototype.Certificate21.height_707_i4 line 314
  126. def OAI.SnakyPrototype.Certificate21.childrenH_707_i4 line 315
  127. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i4 line 316
  128. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i4 line 317
  129. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i4 line 319
  130. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i4 line 323
  131. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i4 line 325
  132. def OAI.SnakyPrototype.Certificate21.checked_707_i4 line 329
  133. def OAI.SnakyPrototype.Certificate21.height_707_i3 line 337
  134. def OAI.SnakyPrototype.Certificate21.childrenH_707_i3 line 338
  135. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i3 line 339
  136. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i3 line 340
  137. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i3 line 342
  138. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i3 line 346
  139. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i3 line 348
  140. def OAI.SnakyPrototype.Certificate21.checked_707_i3 line 352
  141. def OAI.SnakyPrototype.Certificate21.height_707_i6 line 360
  142. def OAI.SnakyPrototype.Certificate21.childrenH_707_i6 line 361
  143. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i6 line 362
  144. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i6 line 363
  145. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i6 line 365
  146. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i6 line 369
  147. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i6 line 371
  148. def OAI.SnakyPrototype.Certificate21.checked_707_i6 line 375
  149. def OAI.SnakyPrototype.Certificate21.height_707_i5 line 383
  150. def OAI.SnakyPrototype.Certificate21.childrenH_707_i5 line 384
  151. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i5 line 385
  152. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i5 line 386
  153. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i5 line 388
  154. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i5 line 392
  155. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i5 line 394
  156. def OAI.SnakyPrototype.Certificate21.checked_707_i5 line 398
  157. def OAI.SnakyPrototype.Certificate21.height_707_i7 line 406
  158. def OAI.SnakyPrototype.Certificate21.childrenH_707_i7 line 407
  159. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i7 line 408
  160. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i7 line 409
  161. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i7 line 411
  162. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i7 line 415
  163. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i7 line 417
  164. def OAI.SnakyPrototype.Certificate21.checked_707_i7 line 421
  165. def OAI.SnakyPrototype.Certificate21.height_707_i8 line 429
  166. def OAI.SnakyPrototype.Certificate21.childrenH_707_i8 line 430
  167. theorem OAI.SnakyPrototype.Certificate21.height_exact_707_i8 line 431
  168. theorem OAI.SnakyPrototype.Certificate21.required_origin_707_i8 line 432
  169. theorem OAI.SnakyPrototype.Certificate21.required_exact_707_i8 line 434
  170. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707_i8 line 438
  171. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707_i8 line 440
  172. def OAI.SnakyPrototype.Certificate21.checked_707_i8 line 444
  173. def OAI.SnakyPrototype.Certificate21.height_707 line 452
  174. def OAI.SnakyPrototype.Certificate21.childrenH_707 line 453
  175. theorem OAI.SnakyPrototype.Certificate21.height_exact_707 line 454
  176. theorem OAI.SnakyPrototype.Certificate21.required_origin_707 line 455
  177. theorem OAI.SnakyPrototype.Certificate21.required_exact_707 line 457
  178. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_707 line 461
  179. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_707 line 463
  180. def OAI.SnakyPrototype.Certificate21.checked_707 line 467