OAI/GameTheory/SnakyConditional/Templates/Level28Part03.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_581 line 6
  2. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_4 line 7
  3. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_4_chain line 8
  4. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_4_head line 9
  5. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_4_last line 10
  6. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_5 line 11
  7. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_5_chain line 12
  8. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_5_head line 13
  9. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_5_last line 14
  10. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_3 line 15
  11. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_3_chain line 16
  12. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_3_head line 19
  13. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_3_last line 21
  14. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_7 line 23
  15. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_7_chain line 24
  16. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_7_head line 25
  17. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_7_last line 26
  18. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_8 line 27
  19. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_8_chain line 28
  20. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_8_head line 29
  21. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_8_last line 30
  22. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_6 line 31
  23. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_6_chain line 32
  24. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_6_head line 35
  25. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_6_last line 37
  26. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_2 line 39
  27. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_2_chain line 40
  28. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_2_head line 43
  29. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_2_last line 45
  30. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_11 line 47
  31. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_11_chain line 48
  32. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_11_head line 49
  33. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_11_last line 50
  34. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_12 line 51
  35. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_12_chain line 52
  36. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_12_head line 53
  37. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_12_last line 54
  38. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_10 line 55
  39. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_10_chain line 56
  40. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_10_head line 59
  41. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_10_last line 61
  42. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_14 line 63
  43. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_14_chain line 64
  44. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_14_head line 65
  45. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_14_last line 66
  46. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_15 line 67
  47. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_15_chain line 68
  48. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_15_head line 69
  49. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_15_last line 70
  50. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_13 line 71
  51. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_13_chain line 72
  52. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_13_head line 75
  53. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_13_last line 77
  54. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_9 line 79
  55. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_9_chain line 80
  56. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_9_head line 83
  57. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_9_last line 85
  58. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_1 line 87
  59. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_1_chain line 88
  60. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_1_head line 91
  61. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_1_last line 93
  62. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_19 line 95
  63. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_19_chain line 96
  64. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_19_head line 97
  65. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_19_last line 98
  66. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_20 line 99
  67. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_20_chain line 100
  68. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_20_head line 101
  69. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_20_last line 102
  70. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_18 line 103
  71. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_18_chain line 104
  72. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_18_head line 107
  73. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_18_last line 109
  74. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_22 line 111
  75. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_22_chain line 112
  76. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_22_head line 113
  77. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_22_last line 114
  78. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_23 line 115
  79. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_23_chain line 116
  80. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_23_head line 117
  81. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_23_last line 118
  82. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_21 line 119
  83. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_21_chain line 120
  84. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_21_head line 123
  85. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_21_last line 125
  86. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_17 line 127
  87. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_17_chain line 128
  88. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_17_head line 131
  89. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_17_last line 133
  90. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_26 line 135
  91. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_26_chain line 136
  92. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_26_head line 137
  93. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_26_last line 138
  94. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_27 line 139
  95. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_27_chain line 140
  96. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_27_head line 141
  97. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_27_last line 142
  98. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_25 line 143
  99. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_25_chain line 144
  100. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_25_head line 147
  101. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_25_last line 149
  102. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_29 line 151
  103. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_29_chain line 152
  104. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_29_head line 153
  105. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_29_last line 154
  106. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_30 line 155
  107. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_30_chain line 156
  108. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_30_head line 157
  109. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_30_last line 158
  110. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_28 line 159
  111. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_28_chain line 160
  112. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_28_head line 163
  113. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_28_last line 165
  114. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_24 line 167
  115. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_24_chain line 168
  116. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_24_head line 171
  117. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_24_last line 173
  118. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_16 line 175
  119. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_16_chain line 176
  120. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_16_head line 179
  121. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_16_last line 181
  122. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_0 line 183
  123. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_0_chain line 184
  124. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_0_head line 187
  125. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_0_last line 189
  126. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_581_nodup line 191
  127. def OAI.SnakyConditional.envelope_581 line 193
  128. def OAI.SnakyConditional.childrenC_581 line 194
  129. def OAI.SnakyConditional.childrenD_581 line 195
  130. theorem OAI.SnakyConditional.common_sub_581 line 196
  131. theorem OAI.SnakyConditional.child_required_sub_581 line 197
  132. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_581_0 line 198
  133. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_581_1 line 200
  134. theorem OAI.SnakyConditional.child_envelope_sub_581 line 202
  135. theorem OAI.SnakyConditional.pivot_mem_581 line 207
  136. theorem OAI.SnakyConditional.children_work_581 line 208
  137. theorem OAI.SnakyConditional.row_works_581 line 213