OAI/GameTheory/SnakyTwentyOne/Cards/Height16Part03.lean

GitHub source file

180 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_724_i0 line 29
  2. def OAI.SnakyPrototype.Certificate21.envelope_724_i0 line 30
  3. def OAI.SnakyPrototype.Certificate21.childrenC_724_i0 line 31
  4. def OAI.SnakyPrototype.Certificate21.childrenD_724_i0 line 32
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i0 line 33
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i0 line 34
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i0 line 35
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i0 line 36
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i0 line 37
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i0 line 44
  11. def OAI.SnakyPrototype.Certificate21.required_724_i2 line 49
  12. def OAI.SnakyPrototype.Certificate21.envelope_724_i2 line 50
  13. def OAI.SnakyPrototype.Certificate21.childrenC_724_i2 line 51
  14. def OAI.SnakyPrototype.Certificate21.childrenD_724_i2 line 52
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i2 line 53
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i2 line 54
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i2 line 55
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i2 line 56
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i2 line 57
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i2 line 63
  21. def OAI.SnakyPrototype.Certificate21.required_724_i3 line 68
  22. def OAI.SnakyPrototype.Certificate21.envelope_724_i3 line 69
  23. def OAI.SnakyPrototype.Certificate21.childrenC_724_i3 line 70
  24. def OAI.SnakyPrototype.Certificate21.childrenD_724_i3 line 71
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i3 line 72
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i3 line 73
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i3 line 74
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i3 line 75
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i3 line 76
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i3 line 82
  31. def OAI.SnakyPrototype.Certificate21.required_724_i4 line 87
  32. def OAI.SnakyPrototype.Certificate21.envelope_724_i4 line 88
  33. def OAI.SnakyPrototype.Certificate21.childrenC_724_i4 line 89
  34. def OAI.SnakyPrototype.Certificate21.childrenD_724_i4 line 90
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i4 line 91
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i4 line 92
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i4 line 93
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i4 line 94
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i4 line 95
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i4 line 100
  41. def OAI.SnakyPrototype.Certificate21.required_724_i1 line 105
  42. def OAI.SnakyPrototype.Certificate21.envelope_724_i1 line 106
  43. def OAI.SnakyPrototype.Certificate21.childrenC_724_i1 line 107
  44. def OAI.SnakyPrototype.Certificate21.childrenD_724_i1 line 108
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i1 line 109
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i1 line 110
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i1 line 111
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i1 line 112
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i1 line 113
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i1 line 122
  51. def OAI.SnakyPrototype.Certificate21.required_724_i5 line 127
  52. def OAI.SnakyPrototype.Certificate21.envelope_724_i5 line 128
  53. def OAI.SnakyPrototype.Certificate21.childrenC_724_i5 line 129
  54. def OAI.SnakyPrototype.Certificate21.childrenD_724_i5 line 130
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i5 line 131
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i5 line 132
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i5 line 133
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i5 line 134
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i5 line 135
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i5 line 142
  61. def OAI.SnakyPrototype.Certificate21.required_724_i6 line 147
  62. def OAI.SnakyPrototype.Certificate21.envelope_724_i6 line 148
  63. def OAI.SnakyPrototype.Certificate21.childrenC_724_i6 line 149
  64. def OAI.SnakyPrototype.Certificate21.childrenD_724_i6 line 150
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i6 line 151
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i6 line 152
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i6 line 153
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i6 line 154
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i6 line 155
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i6 line 163
  71. def OAI.SnakyPrototype.Certificate21.required_724_i8 line 168
  72. def OAI.SnakyPrototype.Certificate21.envelope_724_i8 line 169
  73. def OAI.SnakyPrototype.Certificate21.childrenC_724_i8 line 170
  74. def OAI.SnakyPrototype.Certificate21.childrenD_724_i8 line 171
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i8 line 172
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i8 line 173
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i8 line 174
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i8 line 175
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i8 line 176
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i8 line 182
  81. def OAI.SnakyPrototype.Certificate21.required_724_i7 line 187
  82. def OAI.SnakyPrototype.Certificate21.envelope_724_i7 line 188
  83. def OAI.SnakyPrototype.Certificate21.childrenC_724_i7 line 189
  84. def OAI.SnakyPrototype.Certificate21.childrenD_724_i7 line 190
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_724_i7 line 191
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724_i7 line 192
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724_i7 line 193
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724_i7 line 194
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_724_i7 line 195
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_724_i7 line 202
  91. def OAI.SnakyPrototype.Certificate21.required_724 line 207
  92. def OAI.SnakyPrototype.Certificate21.envelope_724 line 208
  93. def OAI.SnakyPrototype.Certificate21.childrenC_724 line 209
  94. def OAI.SnakyPrototype.Certificate21.childrenD_724 line 210
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_724 line 211
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_724 line 212
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_724 line 213
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_724 line 214
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_724 line 215
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_724 line 228
  101. def OAI.SnakyPrototype.Certificate21.height_724_i0 line 233
  102. def OAI.SnakyPrototype.Certificate21.childrenH_724_i0 line 234
  103. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i0 line 235
  104. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i0 line 236
  105. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i0 line 238
  106. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i0 line 242
  107. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i0 line 244
  108. def OAI.SnakyPrototype.Certificate21.checked_724_i0 line 248
  109. def OAI.SnakyPrototype.Certificate21.height_724_i2 line 256
  110. def OAI.SnakyPrototype.Certificate21.childrenH_724_i2 line 257
  111. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i2 line 258
  112. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i2 line 259
  113. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i2 line 261
  114. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i2 line 265
  115. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i2 line 267
  116. def OAI.SnakyPrototype.Certificate21.checked_724_i2 line 271
  117. def OAI.SnakyPrototype.Certificate21.height_724_i3 line 279
  118. def OAI.SnakyPrototype.Certificate21.childrenH_724_i3 line 280
  119. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i3 line 281
  120. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i3 line 282
  121. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i3 line 284
  122. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i3 line 288
  123. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i3 line 290
  124. def OAI.SnakyPrototype.Certificate21.checked_724_i3 line 294
  125. def OAI.SnakyPrototype.Certificate21.height_724_i4 line 302
  126. def OAI.SnakyPrototype.Certificate21.childrenH_724_i4 line 303
  127. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i4 line 304
  128. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i4 line 305
  129. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i4 line 307
  130. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i4 line 311
  131. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i4 line 313
  132. def OAI.SnakyPrototype.Certificate21.checked_724_i4 line 317
  133. def OAI.SnakyPrototype.Certificate21.height_724_i1 line 325
  134. def OAI.SnakyPrototype.Certificate21.childrenH_724_i1 line 326
  135. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i1 line 327
  136. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i1 line 328
  137. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i1 line 330
  138. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i1 line 334
  139. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i1 line 336
  140. def OAI.SnakyPrototype.Certificate21.checked_724_i1 line 340
  141. def OAI.SnakyPrototype.Certificate21.height_724_i5 line 348
  142. def OAI.SnakyPrototype.Certificate21.childrenH_724_i5 line 349
  143. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i5 line 350
  144. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i5 line 351
  145. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i5 line 353
  146. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i5 line 357
  147. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i5 line 359
  148. def OAI.SnakyPrototype.Certificate21.checked_724_i5 line 363
  149. def OAI.SnakyPrototype.Certificate21.height_724_i6 line 371
  150. def OAI.SnakyPrototype.Certificate21.childrenH_724_i6 line 372
  151. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i6 line 373
  152. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i6 line 374
  153. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i6 line 376
  154. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i6 line 380
  155. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i6 line 382
  156. def OAI.SnakyPrototype.Certificate21.checked_724_i6 line 386
  157. def OAI.SnakyPrototype.Certificate21.height_724_i8 line 394
  158. def OAI.SnakyPrototype.Certificate21.childrenH_724_i8 line 395
  159. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i8 line 396
  160. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i8 line 397
  161. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i8 line 399
  162. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i8 line 403
  163. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i8 line 405
  164. def OAI.SnakyPrototype.Certificate21.checked_724_i8 line 409
  165. def OAI.SnakyPrototype.Certificate21.height_724_i7 line 417
  166. def OAI.SnakyPrototype.Certificate21.childrenH_724_i7 line 418
  167. theorem OAI.SnakyPrototype.Certificate21.height_exact_724_i7 line 419
  168. theorem OAI.SnakyPrototype.Certificate21.required_origin_724_i7 line 420
  169. theorem OAI.SnakyPrototype.Certificate21.required_exact_724_i7 line 422
  170. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724_i7 line 426
  171. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724_i7 line 428
  172. def OAI.SnakyPrototype.Certificate21.checked_724_i7 line 432
  173. def OAI.SnakyPrototype.Certificate21.height_724 line 440
  174. def OAI.SnakyPrototype.Certificate21.childrenH_724 line 441
  175. theorem OAI.SnakyPrototype.Certificate21.height_exact_724 line 442
  176. theorem OAI.SnakyPrototype.Certificate21.required_origin_724 line 443
  177. theorem OAI.SnakyPrototype.Certificate21.required_exact_724 line 445
  178. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_724 line 449
  179. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_724 line 451
  180. def OAI.SnakyPrototype.Certificate21.checked_724 line 455