OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part07.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_722_i1 line 17
  2. def OAI.SnakyPrototype.Certificate21.envelope_722_i1 line 18
  3. def OAI.SnakyPrototype.Certificate21.childrenC_722_i1 line 19
  4. def OAI.SnakyPrototype.Certificate21.childrenD_722_i1 line 20
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_722_i1 line 21
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_722_i1 line 22
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_722_i1 line 23
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_722_i1 line 24
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_722_i1 line 25
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_722_i1 line 30
  11. def OAI.SnakyPrototype.Certificate21.required_722_i0 line 35
  12. def OAI.SnakyPrototype.Certificate21.envelope_722_i0 line 36
  13. def OAI.SnakyPrototype.Certificate21.childrenC_722_i0 line 37
  14. def OAI.SnakyPrototype.Certificate21.childrenD_722_i0 line 38
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_722_i0 line 39
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_722_i0 line 40
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_722_i0 line 41
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_722_i0 line 42
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_722_i0 line 43
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_722_i0 line 50
  21. def OAI.SnakyPrototype.Certificate21.required_722_i2 line 55
  22. def OAI.SnakyPrototype.Certificate21.envelope_722_i2 line 56
  23. def OAI.SnakyPrototype.Certificate21.childrenC_722_i2 line 57
  24. def OAI.SnakyPrototype.Certificate21.childrenD_722_i2 line 58
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_722_i2 line 59
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_722_i2 line 60
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_722_i2 line 61
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_722_i2 line 62
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_722_i2 line 63
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_722_i2 line 68
  31. def OAI.SnakyPrototype.Certificate21.required_722_i3 line 73
  32. def OAI.SnakyPrototype.Certificate21.envelope_722_i3 line 74
  33. def OAI.SnakyPrototype.Certificate21.childrenC_722_i3 line 75
  34. def OAI.SnakyPrototype.Certificate21.childrenD_722_i3 line 76
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_722_i3 line 77
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_722_i3 line 78
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_722_i3 line 79
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_722_i3 line 80
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_722_i3 line 81
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_722_i3 line 86
  41. def OAI.SnakyPrototype.Certificate21.required_722_i4 line 91
  42. def OAI.SnakyPrototype.Certificate21.envelope_722_i4 line 92
  43. def OAI.SnakyPrototype.Certificate21.childrenC_722_i4 line 93
  44. def OAI.SnakyPrototype.Certificate21.childrenD_722_i4 line 94
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_722_i4 line 95
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_722_i4 line 96
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_722_i4 line 97
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_722_i4 line 98
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_722_i4 line 99
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_722_i4 line 104
  51. def OAI.SnakyPrototype.Certificate21.required_722 line 109
  52. def OAI.SnakyPrototype.Certificate21.envelope_722 line 110
  53. def OAI.SnakyPrototype.Certificate21.childrenC_722 line 111
  54. def OAI.SnakyPrototype.Certificate21.childrenD_722 line 112
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_722 line 113
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_722 line 114
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_722 line 115
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_722 line 116
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_722 line 117
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_722 line 126
  61. def OAI.SnakyPrototype.Certificate21.height_722_i1 line 131
  62. def OAI.SnakyPrototype.Certificate21.childrenH_722_i1 line 132
  63. theorem OAI.SnakyPrototype.Certificate21.height_exact_722_i1 line 133
  64. theorem OAI.SnakyPrototype.Certificate21.required_origin_722_i1 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.required_exact_722_i1 line 136
  66. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_722_i1 line 140
  67. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_722_i1 line 142
  68. def OAI.SnakyPrototype.Certificate21.checked_722_i1 line 146
  69. def OAI.SnakyPrototype.Certificate21.height_722_i0 line 154
  70. def OAI.SnakyPrototype.Certificate21.childrenH_722_i0 line 155
  71. theorem OAI.SnakyPrototype.Certificate21.height_exact_722_i0 line 156
  72. theorem OAI.SnakyPrototype.Certificate21.required_origin_722_i0 line 157
  73. theorem OAI.SnakyPrototype.Certificate21.required_exact_722_i0 line 159
  74. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_722_i0 line 163
  75. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_722_i0 line 165
  76. def OAI.SnakyPrototype.Certificate21.checked_722_i0 line 169
  77. def OAI.SnakyPrototype.Certificate21.height_722_i2 line 177
  78. def OAI.SnakyPrototype.Certificate21.childrenH_722_i2 line 178
  79. theorem OAI.SnakyPrototype.Certificate21.height_exact_722_i2 line 179
  80. theorem OAI.SnakyPrototype.Certificate21.required_origin_722_i2 line 180
  81. theorem OAI.SnakyPrototype.Certificate21.required_exact_722_i2 line 182
  82. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_722_i2 line 186
  83. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_722_i2 line 188
  84. def OAI.SnakyPrototype.Certificate21.checked_722_i2 line 192
  85. def OAI.SnakyPrototype.Certificate21.height_722_i3 line 200
  86. def OAI.SnakyPrototype.Certificate21.childrenH_722_i3 line 201
  87. theorem OAI.SnakyPrototype.Certificate21.height_exact_722_i3 line 202
  88. theorem OAI.SnakyPrototype.Certificate21.required_origin_722_i3 line 203
  89. theorem OAI.SnakyPrototype.Certificate21.required_exact_722_i3 line 205
  90. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_722_i3 line 209
  91. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_722_i3 line 211
  92. def OAI.SnakyPrototype.Certificate21.checked_722_i3 line 215
  93. def OAI.SnakyPrototype.Certificate21.height_722_i4 line 223
  94. def OAI.SnakyPrototype.Certificate21.childrenH_722_i4 line 224
  95. theorem OAI.SnakyPrototype.Certificate21.height_exact_722_i4 line 225
  96. theorem OAI.SnakyPrototype.Certificate21.required_origin_722_i4 line 226
  97. theorem OAI.SnakyPrototype.Certificate21.required_exact_722_i4 line 228
  98. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_722_i4 line 232
  99. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_722_i4 line 234
  100. def OAI.SnakyPrototype.Certificate21.checked_722_i4 line 238
  101. def OAI.SnakyPrototype.Certificate21.height_722 line 246
  102. def OAI.SnakyPrototype.Certificate21.childrenH_722 line 247
  103. theorem OAI.SnakyPrototype.Certificate21.height_exact_722 line 248
  104. theorem OAI.SnakyPrototype.Certificate21.required_origin_722 line 249
  105. theorem OAI.SnakyPrototype.Certificate21.required_exact_722 line 251
  106. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_722 line 255
  107. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_722 line 257
  108. def OAI.SnakyPrototype.Certificate21.checked_722 line 261