OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part07.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_720_i0 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_720_i0 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_720_i0 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_720_i0 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_720_i0 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720_i0 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720_i0 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720_i0 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_720_i0 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_720_i0 line 34
  11. def OAI.SnakyPrototype.Certificate21.required_720_i4 line 39
  12. def OAI.SnakyPrototype.Certificate21.envelope_720_i4 line 40
  13. def OAI.SnakyPrototype.Certificate21.childrenC_720_i4 line 41
  14. def OAI.SnakyPrototype.Certificate21.childrenD_720_i4 line 42
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_720_i4 line 43
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720_i4 line 44
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720_i4 line 45
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720_i4 line 46
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_720_i4 line 47
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_720_i4 line 52
  21. def OAI.SnakyPrototype.Certificate21.required_720_i5 line 57
  22. def OAI.SnakyPrototype.Certificate21.envelope_720_i5 line 58
  23. def OAI.SnakyPrototype.Certificate21.childrenC_720_i5 line 59
  24. def OAI.SnakyPrototype.Certificate21.childrenD_720_i5 line 60
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_720_i5 line 61
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720_i5 line 62
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720_i5 line 63
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720_i5 line 64
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_720_i5 line 65
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_720_i5 line 70
  31. def OAI.SnakyPrototype.Certificate21.required_720_i3 line 75
  32. def OAI.SnakyPrototype.Certificate21.envelope_720_i3 line 76
  33. def OAI.SnakyPrototype.Certificate21.childrenC_720_i3 line 77
  34. def OAI.SnakyPrototype.Certificate21.childrenD_720_i3 line 78
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_720_i3 line 79
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720_i3 line 80
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720_i3 line 81
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720_i3 line 82
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_720_i3 line 83
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_720_i3 line 92
  41. def OAI.SnakyPrototype.Certificate21.required_720_i2 line 97
  42. def OAI.SnakyPrototype.Certificate21.envelope_720_i2 line 98
  43. def OAI.SnakyPrototype.Certificate21.childrenC_720_i2 line 99
  44. def OAI.SnakyPrototype.Certificate21.childrenD_720_i2 line 100
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_720_i2 line 101
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720_i2 line 102
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720_i2 line 103
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720_i2 line 104
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_720_i2 line 105
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_720_i2 line 110
  51. def OAI.SnakyPrototype.Certificate21.required_720_i1 line 115
  52. def OAI.SnakyPrototype.Certificate21.envelope_720_i1 line 116
  53. def OAI.SnakyPrototype.Certificate21.childrenC_720_i1 line 117
  54. def OAI.SnakyPrototype.Certificate21.childrenD_720_i1 line 118
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_720_i1 line 119
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720_i1 line 120
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720_i1 line 121
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720_i1 line 122
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_720_i1 line 123
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_720_i1 line 129
  61. def OAI.SnakyPrototype.Certificate21.required_720 line 134
  62. def OAI.SnakyPrototype.Certificate21.envelope_720 line 135
  63. def OAI.SnakyPrototype.Certificate21.childrenC_720 line 136
  64. def OAI.SnakyPrototype.Certificate21.childrenD_720 line 137
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_720 line 138
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_720 line 139
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_720 line 140
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_720 line 141
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_720 line 142
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_720 line 149
  71. def OAI.SnakyPrototype.Certificate21.height_720_i0 line 154
  72. def OAI.SnakyPrototype.Certificate21.childrenH_720_i0 line 155
  73. theorem OAI.SnakyPrototype.Certificate21.height_exact_720_i0 line 156
  74. theorem OAI.SnakyPrototype.Certificate21.required_origin_720_i0 line 157
  75. theorem OAI.SnakyPrototype.Certificate21.required_exact_720_i0 line 159
  76. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720_i0 line 163
  77. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720_i0 line 165
  78. def OAI.SnakyPrototype.Certificate21.checked_720_i0 line 169
  79. def OAI.SnakyPrototype.Certificate21.height_720_i4 line 177
  80. def OAI.SnakyPrototype.Certificate21.childrenH_720_i4 line 178
  81. theorem OAI.SnakyPrototype.Certificate21.height_exact_720_i4 line 179
  82. theorem OAI.SnakyPrototype.Certificate21.required_origin_720_i4 line 180
  83. theorem OAI.SnakyPrototype.Certificate21.required_exact_720_i4 line 182
  84. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720_i4 line 186
  85. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720_i4 line 188
  86. def OAI.SnakyPrototype.Certificate21.checked_720_i4 line 192
  87. def OAI.SnakyPrototype.Certificate21.height_720_i5 line 200
  88. def OAI.SnakyPrototype.Certificate21.childrenH_720_i5 line 201
  89. theorem OAI.SnakyPrototype.Certificate21.height_exact_720_i5 line 202
  90. theorem OAI.SnakyPrototype.Certificate21.required_origin_720_i5 line 203
  91. theorem OAI.SnakyPrototype.Certificate21.required_exact_720_i5 line 205
  92. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720_i5 line 209
  93. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720_i5 line 211
  94. def OAI.SnakyPrototype.Certificate21.checked_720_i5 line 215
  95. def OAI.SnakyPrototype.Certificate21.height_720_i3 line 223
  96. def OAI.SnakyPrototype.Certificate21.childrenH_720_i3 line 224
  97. theorem OAI.SnakyPrototype.Certificate21.height_exact_720_i3 line 225
  98. theorem OAI.SnakyPrototype.Certificate21.required_origin_720_i3 line 226
  99. theorem OAI.SnakyPrototype.Certificate21.required_exact_720_i3 line 228
  100. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720_i3 line 232
  101. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720_i3 line 234
  102. def OAI.SnakyPrototype.Certificate21.checked_720_i3 line 238
  103. def OAI.SnakyPrototype.Certificate21.height_720_i2 line 246
  104. def OAI.SnakyPrototype.Certificate21.childrenH_720_i2 line 247
  105. theorem OAI.SnakyPrototype.Certificate21.height_exact_720_i2 line 248
  106. theorem OAI.SnakyPrototype.Certificate21.required_origin_720_i2 line 249
  107. theorem OAI.SnakyPrototype.Certificate21.required_exact_720_i2 line 251
  108. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720_i2 line 255
  109. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720_i2 line 257
  110. def OAI.SnakyPrototype.Certificate21.checked_720_i2 line 261
  111. def OAI.SnakyPrototype.Certificate21.height_720_i1 line 269
  112. def OAI.SnakyPrototype.Certificate21.childrenH_720_i1 line 270
  113. theorem OAI.SnakyPrototype.Certificate21.height_exact_720_i1 line 271
  114. theorem OAI.SnakyPrototype.Certificate21.required_origin_720_i1 line 272
  115. theorem OAI.SnakyPrototype.Certificate21.required_exact_720_i1 line 274
  116. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720_i1 line 278
  117. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720_i1 line 280
  118. def OAI.SnakyPrototype.Certificate21.checked_720_i1 line 284
  119. def OAI.SnakyPrototype.Certificate21.height_720 line 292
  120. def OAI.SnakyPrototype.Certificate21.childrenH_720 line 293
  121. theorem OAI.SnakyPrototype.Certificate21.height_exact_720 line 294
  122. theorem OAI.SnakyPrototype.Certificate21.required_origin_720 line 295
  123. theorem OAI.SnakyPrototype.Certificate21.required_exact_720 line 297
  124. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_720 line 301
  125. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_720 line 303
  126. def OAI.SnakyPrototype.Certificate21.checked_720 line 307