OAI/GameTheory/SnakyConditional/Templates/Level26Part07.lean

GitHub source file

140 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_582 line 7
  2. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_4 line 8
  3. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_4_chain line 9
  4. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_4_head line 10
  5. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_4_last line 11
  6. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_5 line 12
  7. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_5_chain line 13
  8. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_5_head line 14
  9. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_5_last line 15
  10. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_3 line 16
  11. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_3_chain line 17
  12. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_3_head line 20
  13. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_3_last line 22
  14. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_7 line 24
  15. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_7_chain line 25
  16. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_7_head line 26
  17. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_7_last line 27
  18. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_8 line 28
  19. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_8_chain line 29
  20. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_8_head line 30
  21. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_8_last line 31
  22. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_6 line 32
  23. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_6_chain line 33
  24. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_6_head line 36
  25. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_6_last line 38
  26. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_2 line 40
  27. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_2_chain line 41
  28. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_2_head line 44
  29. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_2_last line 46
  30. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_11 line 48
  31. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_11_chain line 49
  32. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_11_head line 50
  33. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_11_last line 51
  34. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_12 line 52
  35. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_12_chain line 53
  36. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_12_head line 54
  37. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_12_last line 55
  38. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_10 line 56
  39. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_10_chain line 57
  40. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_10_head line 60
  41. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_10_last line 62
  42. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_14 line 64
  43. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_14_chain line 65
  44. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_14_head line 66
  45. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_14_last line 67
  46. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_15 line 68
  47. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_15_chain line 69
  48. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_15_head line 70
  49. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_15_last line 71
  50. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_13 line 72
  51. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_13_chain line 73
  52. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_13_head line 76
  53. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_13_last line 78
  54. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_9 line 80
  55. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_9_chain line 81
  56. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_9_head line 84
  57. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_9_last line 86
  58. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_1 line 88
  59. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_1_chain line 89
  60. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_1_head line 92
  61. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_1_last line 94
  62. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_19 line 96
  63. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_19_chain line 97
  64. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_19_head line 98
  65. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_19_last line 99
  66. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_20 line 100
  67. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_20_chain line 101
  68. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_20_head line 102
  69. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_20_last line 103
  70. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_18 line 104
  71. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_18_chain line 105
  72. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_18_head line 108
  73. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_18_last line 110
  74. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_22 line 112
  75. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_22_chain line 113
  76. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_22_head line 114
  77. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_22_last line 115
  78. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_23 line 116
  79. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_23_chain line 117
  80. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_23_head line 118
  81. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_23_last line 119
  82. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_21 line 120
  83. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_21_chain line 121
  84. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_21_head line 124
  85. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_21_last line 126
  86. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_17 line 128
  87. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_17_chain line 129
  88. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_17_head line 132
  89. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_17_last line 134
  90. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_26 line 136
  91. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_26_chain line 137
  92. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_26_head line 138
  93. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_26_last line 139
  94. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_27 line 140
  95. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_27_chain line 141
  96. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_27_head line 142
  97. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_27_last line 143
  98. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_25 line 144
  99. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_25_chain line 145
  100. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_25_head line 148
  101. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_25_last line 150
  102. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_29 line 152
  103. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_29_chain line 153
  104. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_29_head line 154
  105. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_29_last line 155
  106. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_30 line 156
  107. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_30_chain line 157
  108. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_30_head line 158
  109. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_30_last line 159
  110. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_28 line 160
  111. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_28_chain line 161
  112. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_28_head line 164
  113. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_28_last line 166
  114. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_24 line 168
  115. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_24_chain line 169
  116. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_24_head line 172
  117. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_24_last line 174
  118. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_16 line 176
  119. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_16_chain line 177
  120. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_16_head line 180
  121. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_16_last line 182
  122. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_0 line 184
  123. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_0_chain line 185
  124. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_0_head line 188
  125. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_0_last line 190
  126. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_582_nodup line 192
  127. def OAI.SnakyConditional.envelope_582 line 194
  128. def OAI.SnakyConditional.childrenC_582 line 195
  129. def OAI.SnakyConditional.childrenD_582 line 196
  130. theorem OAI.SnakyConditional.common_sub_582 line 197
  131. theorem OAI.SnakyConditional.child_required_sub_582 line 198
  132. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_582_0 line 199
  133. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_582_1 line 201
  134. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_582_2 line 203
  135. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_582_3 line 205
  136. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_582_4 line 207
  137. theorem OAI.SnakyConditional.child_envelope_sub_582 line 209
  138. theorem OAI.SnakyConditional.pivot_mem_582 line 217
  139. theorem OAI.SnakyConditional.children_work_582 line 218
  140. theorem OAI.SnakyConditional.row_works_582 line 226