OAI/GameTheory/SnakyTwentyOne/Cards/Height15Part04.lean

GitHub source file

162 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_719_i5 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_719_i5 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_719_i5 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_719_i5 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i5 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i5 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i5 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i5 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i5 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i5 line 33
  11. def OAI.SnakyPrototype.Certificate21.required_719_i4 line 38
  12. def OAI.SnakyPrototype.Certificate21.envelope_719_i4 line 39
  13. def OAI.SnakyPrototype.Certificate21.childrenC_719_i4 line 40
  14. def OAI.SnakyPrototype.Certificate21.childrenD_719_i4 line 41
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i4 line 42
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i4 line 43
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i4 line 44
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i4 line 45
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i4 line 46
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i4 line 52
  21. def OAI.SnakyPrototype.Certificate21.required_719_i3 line 57
  22. def OAI.SnakyPrototype.Certificate21.envelope_719_i3 line 58
  23. def OAI.SnakyPrototype.Certificate21.childrenC_719_i3 line 59
  24. def OAI.SnakyPrototype.Certificate21.childrenD_719_i3 line 60
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i3 line 61
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i3 line 62
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i3 line 63
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i3 line 64
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i3 line 65
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i3 line 70
  31. def OAI.SnakyPrototype.Certificate21.required_719_i2 line 75
  32. def OAI.SnakyPrototype.Certificate21.envelope_719_i2 line 76
  33. def OAI.SnakyPrototype.Certificate21.childrenC_719_i2 line 77
  34. def OAI.SnakyPrototype.Certificate21.childrenD_719_i2 line 78
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i2 line 79
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i2 line 80
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i2 line 81
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i2 line 82
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i2 line 83
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i2 line 88
  41. def OAI.SnakyPrototype.Certificate21.required_719_i1 line 93
  42. def OAI.SnakyPrototype.Certificate21.envelope_719_i1 line 94
  43. def OAI.SnakyPrototype.Certificate21.childrenC_719_i1 line 95
  44. def OAI.SnakyPrototype.Certificate21.childrenD_719_i1 line 96
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i1 line 97
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i1 line 98
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i1 line 99
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i1 line 100
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i1 line 101
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i1 line 108
  51. def OAI.SnakyPrototype.Certificate21.required_719_i0 line 113
  52. def OAI.SnakyPrototype.Certificate21.envelope_719_i0 line 114
  53. def OAI.SnakyPrototype.Certificate21.childrenC_719_i0 line 115
  54. def OAI.SnakyPrototype.Certificate21.childrenD_719_i0 line 116
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i0 line 117
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i0 line 118
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i0 line 119
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i0 line 120
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i0 line 121
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i0 line 128
  61. def OAI.SnakyPrototype.Certificate21.required_719_i6 line 133
  62. def OAI.SnakyPrototype.Certificate21.envelope_719_i6 line 134
  63. def OAI.SnakyPrototype.Certificate21.childrenC_719_i6 line 135
  64. def OAI.SnakyPrototype.Certificate21.childrenD_719_i6 line 136
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i6 line 137
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i6 line 138
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i6 line 139
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i6 line 140
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i6 line 141
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i6 line 147
  71. def OAI.SnakyPrototype.Certificate21.required_719_i7 line 152
  72. def OAI.SnakyPrototype.Certificate21.envelope_719_i7 line 153
  73. def OAI.SnakyPrototype.Certificate21.childrenC_719_i7 line 154
  74. def OAI.SnakyPrototype.Certificate21.childrenD_719_i7 line 155
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_719_i7 line 156
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719_i7 line 157
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719_i7 line 158
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719_i7 line 159
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_719_i7 line 160
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_719_i7 line 166
  81. def OAI.SnakyPrototype.Certificate21.required_719 line 171
  82. def OAI.SnakyPrototype.Certificate21.envelope_719 line 172
  83. def OAI.SnakyPrototype.Certificate21.childrenC_719 line 173
  84. def OAI.SnakyPrototype.Certificate21.childrenD_719 line 174
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_719 line 175
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_719 line 176
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_719 line 177
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_719 line 178
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_719 line 179
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_719 line 187
  91. def OAI.SnakyPrototype.Certificate21.height_719_i5 line 192
  92. def OAI.SnakyPrototype.Certificate21.childrenH_719_i5 line 193
  93. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i5 line 194
  94. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i5 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i5 line 197
  96. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i5 line 201
  97. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i5 line 203
  98. def OAI.SnakyPrototype.Certificate21.checked_719_i5 line 207
  99. def OAI.SnakyPrototype.Certificate21.height_719_i4 line 215
  100. def OAI.SnakyPrototype.Certificate21.childrenH_719_i4 line 216
  101. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i4 line 217
  102. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i4 line 218
  103. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i4 line 220
  104. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i4 line 224
  105. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i4 line 226
  106. def OAI.SnakyPrototype.Certificate21.checked_719_i4 line 230
  107. def OAI.SnakyPrototype.Certificate21.height_719_i3 line 238
  108. def OAI.SnakyPrototype.Certificate21.childrenH_719_i3 line 239
  109. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i3 line 240
  110. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i3 line 241
  111. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i3 line 243
  112. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i3 line 247
  113. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i3 line 249
  114. def OAI.SnakyPrototype.Certificate21.checked_719_i3 line 253
  115. def OAI.SnakyPrototype.Certificate21.height_719_i2 line 261
  116. def OAI.SnakyPrototype.Certificate21.childrenH_719_i2 line 262
  117. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i2 line 263
  118. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i2 line 264
  119. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i2 line 266
  120. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i2 line 270
  121. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i2 line 272
  122. def OAI.SnakyPrototype.Certificate21.checked_719_i2 line 276
  123. def OAI.SnakyPrototype.Certificate21.height_719_i1 line 284
  124. def OAI.SnakyPrototype.Certificate21.childrenH_719_i1 line 285
  125. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i1 line 286
  126. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i1 line 287
  127. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i1 line 289
  128. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i1 line 293
  129. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i1 line 295
  130. def OAI.SnakyPrototype.Certificate21.checked_719_i1 line 299
  131. def OAI.SnakyPrototype.Certificate21.height_719_i0 line 307
  132. def OAI.SnakyPrototype.Certificate21.childrenH_719_i0 line 308
  133. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i0 line 309
  134. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i0 line 310
  135. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i0 line 312
  136. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i0 line 316
  137. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i0 line 318
  138. def OAI.SnakyPrototype.Certificate21.checked_719_i0 line 322
  139. def OAI.SnakyPrototype.Certificate21.height_719_i6 line 330
  140. def OAI.SnakyPrototype.Certificate21.childrenH_719_i6 line 331
  141. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i6 line 332
  142. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i6 line 333
  143. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i6 line 335
  144. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i6 line 339
  145. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i6 line 341
  146. def OAI.SnakyPrototype.Certificate21.checked_719_i6 line 345
  147. def OAI.SnakyPrototype.Certificate21.height_719_i7 line 353
  148. def OAI.SnakyPrototype.Certificate21.childrenH_719_i7 line 354
  149. theorem OAI.SnakyPrototype.Certificate21.height_exact_719_i7 line 355
  150. theorem OAI.SnakyPrototype.Certificate21.required_origin_719_i7 line 356
  151. theorem OAI.SnakyPrototype.Certificate21.required_exact_719_i7 line 358
  152. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719_i7 line 362
  153. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719_i7 line 364
  154. def OAI.SnakyPrototype.Certificate21.checked_719_i7 line 368
  155. def OAI.SnakyPrototype.Certificate21.height_719 line 376
  156. def OAI.SnakyPrototype.Certificate21.childrenH_719 line 377
  157. theorem OAI.SnakyPrototype.Certificate21.height_exact_719 line 378
  158. theorem OAI.SnakyPrototype.Certificate21.required_origin_719 line 379
  159. theorem OAI.SnakyPrototype.Certificate21.required_exact_719 line 381
  160. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_719 line 385
  161. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_719 line 387
  162. def OAI.SnakyPrototype.Certificate21.checked_719 line 391