OAI/GameTheory/SnakyTwentyOne/Cards/Height18Part02.lean

GitHub source file

162 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_701_i1 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_701_i1 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_701_i1 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_701_i1 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i1 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i1 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i1 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i1 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i1 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i1 line 33
  11. def OAI.SnakyPrototype.Certificate21.required_701_i2 line 38
  12. def OAI.SnakyPrototype.Certificate21.envelope_701_i2 line 39
  13. def OAI.SnakyPrototype.Certificate21.childrenC_701_i2 line 40
  14. def OAI.SnakyPrototype.Certificate21.childrenD_701_i2 line 41
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i2 line 42
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i2 line 43
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i2 line 44
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i2 line 45
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i2 line 46
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i2 line 51
  21. def OAI.SnakyPrototype.Certificate21.required_701_i3 line 56
  22. def OAI.SnakyPrototype.Certificate21.envelope_701_i3 line 57
  23. def OAI.SnakyPrototype.Certificate21.childrenC_701_i3 line 58
  24. def OAI.SnakyPrototype.Certificate21.childrenD_701_i3 line 59
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i3 line 60
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i3 line 61
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i3 line 62
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i3 line 63
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i3 line 64
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i3 line 69
  31. def OAI.SnakyPrototype.Certificate21.required_701_i4 line 74
  32. def OAI.SnakyPrototype.Certificate21.envelope_701_i4 line 75
  33. def OAI.SnakyPrototype.Certificate21.childrenC_701_i4 line 76
  34. def OAI.SnakyPrototype.Certificate21.childrenD_701_i4 line 77
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i4 line 78
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i4 line 79
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i4 line 80
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i4 line 81
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i4 line 82
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i4 line 87
  41. def OAI.SnakyPrototype.Certificate21.required_701_i6 line 92
  42. def OAI.SnakyPrototype.Certificate21.envelope_701_i6 line 93
  43. def OAI.SnakyPrototype.Certificate21.childrenC_701_i6 line 94
  44. def OAI.SnakyPrototype.Certificate21.childrenD_701_i6 line 95
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i6 line 96
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i6 line 97
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i6 line 98
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i6 line 99
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i6 line 100
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i6 line 105
  51. def OAI.SnakyPrototype.Certificate21.required_701_i7 line 110
  52. def OAI.SnakyPrototype.Certificate21.envelope_701_i7 line 111
  53. def OAI.SnakyPrototype.Certificate21.childrenC_701_i7 line 112
  54. def OAI.SnakyPrototype.Certificate21.childrenD_701_i7 line 113
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i7 line 114
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i7 line 115
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i7 line 116
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i7 line 117
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i7 line 118
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i7 line 123
  61. def OAI.SnakyPrototype.Certificate21.required_701_i5 line 128
  62. def OAI.SnakyPrototype.Certificate21.envelope_701_i5 line 129
  63. def OAI.SnakyPrototype.Certificate21.childrenC_701_i5 line 130
  64. def OAI.SnakyPrototype.Certificate21.childrenD_701_i5 line 131
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i5 line 132
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i5 line 133
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i5 line 134
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i5 line 135
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i5 line 136
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i5 line 142
  71. def OAI.SnakyPrototype.Certificate21.required_701_i0 line 147
  72. def OAI.SnakyPrototype.Certificate21.envelope_701_i0 line 148
  73. def OAI.SnakyPrototype.Certificate21.childrenC_701_i0 line 149
  74. def OAI.SnakyPrototype.Certificate21.childrenD_701_i0 line 150
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_701_i0 line 151
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701_i0 line 152
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701_i0 line 153
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701_i0 line 154
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_701_i0 line 155
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_701_i0 line 165
  81. def OAI.SnakyPrototype.Certificate21.required_701 line 170
  82. def OAI.SnakyPrototype.Certificate21.envelope_701 line 171
  83. def OAI.SnakyPrototype.Certificate21.childrenC_701 line 172
  84. def OAI.SnakyPrototype.Certificate21.childrenD_701 line 173
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_701 line 174
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_701 line 175
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_701 line 176
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_701 line 177
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_701 line 178
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_701 line 187
  91. def OAI.SnakyPrototype.Certificate21.height_701_i1 line 192
  92. def OAI.SnakyPrototype.Certificate21.childrenH_701_i1 line 193
  93. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i1 line 194
  94. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i1 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i1 line 197
  96. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i1 line 201
  97. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i1 line 203
  98. def OAI.SnakyPrototype.Certificate21.checked_701_i1 line 207
  99. def OAI.SnakyPrototype.Certificate21.height_701_i2 line 215
  100. def OAI.SnakyPrototype.Certificate21.childrenH_701_i2 line 216
  101. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i2 line 217
  102. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i2 line 218
  103. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i2 line 220
  104. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i2 line 224
  105. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i2 line 226
  106. def OAI.SnakyPrototype.Certificate21.checked_701_i2 line 230
  107. def OAI.SnakyPrototype.Certificate21.height_701_i3 line 238
  108. def OAI.SnakyPrototype.Certificate21.childrenH_701_i3 line 239
  109. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i3 line 240
  110. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i3 line 241
  111. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i3 line 243
  112. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i3 line 247
  113. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i3 line 249
  114. def OAI.SnakyPrototype.Certificate21.checked_701_i3 line 253
  115. def OAI.SnakyPrototype.Certificate21.height_701_i4 line 261
  116. def OAI.SnakyPrototype.Certificate21.childrenH_701_i4 line 262
  117. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i4 line 263
  118. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i4 line 264
  119. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i4 line 266
  120. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i4 line 270
  121. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i4 line 272
  122. def OAI.SnakyPrototype.Certificate21.checked_701_i4 line 276
  123. def OAI.SnakyPrototype.Certificate21.height_701_i6 line 284
  124. def OAI.SnakyPrototype.Certificate21.childrenH_701_i6 line 285
  125. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i6 line 286
  126. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i6 line 287
  127. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i6 line 289
  128. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i6 line 293
  129. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i6 line 295
  130. def OAI.SnakyPrototype.Certificate21.checked_701_i6 line 299
  131. def OAI.SnakyPrototype.Certificate21.height_701_i7 line 307
  132. def OAI.SnakyPrototype.Certificate21.childrenH_701_i7 line 308
  133. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i7 line 309
  134. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i7 line 310
  135. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i7 line 312
  136. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i7 line 316
  137. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i7 line 318
  138. def OAI.SnakyPrototype.Certificate21.checked_701_i7 line 322
  139. def OAI.SnakyPrototype.Certificate21.height_701_i5 line 330
  140. def OAI.SnakyPrototype.Certificate21.childrenH_701_i5 line 331
  141. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i5 line 332
  142. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i5 line 333
  143. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i5 line 335
  144. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i5 line 339
  145. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i5 line 341
  146. def OAI.SnakyPrototype.Certificate21.checked_701_i5 line 345
  147. def OAI.SnakyPrototype.Certificate21.height_701_i0 line 353
  148. def OAI.SnakyPrototype.Certificate21.childrenH_701_i0 line 354
  149. theorem OAI.SnakyPrototype.Certificate21.height_exact_701_i0 line 355
  150. theorem OAI.SnakyPrototype.Certificate21.required_origin_701_i0 line 356
  151. theorem OAI.SnakyPrototype.Certificate21.required_exact_701_i0 line 358
  152. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701_i0 line 362
  153. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701_i0 line 364
  154. def OAI.SnakyPrototype.Certificate21.checked_701_i0 line 368
  155. def OAI.SnakyPrototype.Certificate21.height_701 line 376
  156. def OAI.SnakyPrototype.Certificate21.childrenH_701 line 377
  157. theorem OAI.SnakyPrototype.Certificate21.height_exact_701 line 378
  158. theorem OAI.SnakyPrototype.Certificate21.required_origin_701 line 379
  159. theorem OAI.SnakyPrototype.Certificate21.required_exact_701 line 381
  160. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_701 line 385
  161. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_701 line 387
  162. def OAI.SnakyPrototype.Certificate21.checked_701 line 391