OAI/GameTheory/SnakyConditional/Templates/Level26Part06.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_576 line 9
  2. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_4 line 10
  3. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_4_chain line 11
  4. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_4_head line 12
  5. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_4_last line 13
  6. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_5 line 14
  7. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_5_chain line 15
  8. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_5_head line 16
  9. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_5_last line 17
  10. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_3 line 18
  11. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_3_chain line 19
  12. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_3_head line 22
  13. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_3_last line 24
  14. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_7 line 26
  15. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_7_chain line 27
  16. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_7_head line 28
  17. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_7_last line 29
  18. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_8 line 30
  19. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_8_chain line 31
  20. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_8_head line 32
  21. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_8_last line 33
  22. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_6 line 34
  23. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_6_chain line 35
  24. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_6_head line 38
  25. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_6_last line 40
  26. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_2 line 42
  27. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_2_chain line 43
  28. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_2_head line 46
  29. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_2_last line 48
  30. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_11 line 50
  31. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_11_chain line 51
  32. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_11_head line 52
  33. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_11_last line 53
  34. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_12 line 54
  35. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_12_chain line 55
  36. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_12_head line 56
  37. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_12_last line 57
  38. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_10 line 58
  39. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_10_chain line 59
  40. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_10_head line 62
  41. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_10_last line 64
  42. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_14 line 66
  43. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_14_chain line 67
  44. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_14_head line 68
  45. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_14_last line 69
  46. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_15 line 70
  47. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_15_chain line 71
  48. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_15_head line 72
  49. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_15_last line 73
  50. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_13 line 74
  51. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_13_chain line 75
  52. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_13_head line 78
  53. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_13_last line 80
  54. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_9 line 82
  55. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_9_chain line 83
  56. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_9_head line 86
  57. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_9_last line 88
  58. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_1 line 90
  59. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_1_chain line 91
  60. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_1_head line 94
  61. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_1_last line 96
  62. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_19 line 98
  63. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_19_chain line 99
  64. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_19_head line 100
  65. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_19_last line 101
  66. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_20 line 102
  67. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_20_chain line 103
  68. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_20_head line 104
  69. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_20_last line 105
  70. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_18 line 106
  71. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_18_chain line 107
  72. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_18_head line 110
  73. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_18_last line 112
  74. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_22 line 114
  75. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_22_chain line 115
  76. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_22_head line 116
  77. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_22_last line 117
  78. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_23 line 118
  79. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_23_chain line 119
  80. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_23_head line 120
  81. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_23_last line 121
  82. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_21 line 122
  83. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_21_chain line 123
  84. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_21_head line 126
  85. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_21_last line 128
  86. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_17 line 130
  87. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_17_chain line 131
  88. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_17_head line 134
  89. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_17_last line 136
  90. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_26 line 138
  91. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_26_chain line 139
  92. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_26_head line 140
  93. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_26_last line 141
  94. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_27 line 142
  95. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_27_chain line 143
  96. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_27_head line 144
  97. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_27_last line 145
  98. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_25 line 146
  99. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_25_chain line 147
  100. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_25_head line 150
  101. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_25_last line 152
  102. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_29 line 154
  103. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_29_chain line 155
  104. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_29_head line 156
  105. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_29_last line 157
  106. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_30 line 158
  107. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_30_chain line 159
  108. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_30_head line 160
  109. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_30_last line 161
  110. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_28 line 162
  111. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_28_chain line 163
  112. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_28_head line 166
  113. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_28_last line 168
  114. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_24 line 170
  115. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_24_chain line 171
  116. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_24_head line 174
  117. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_24_last line 176
  118. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_16 line 178
  119. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_16_chain line 179
  120. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_16_head line 182
  121. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_16_last line 184
  122. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_0 line 186
  123. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_0_chain line 187
  124. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_0_head line 190
  125. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_0_last line 192
  126. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_576_nodup line 194
  127. def OAI.SnakyConditional.envelope_576 line 196
  128. def OAI.SnakyConditional.childrenC_576 line 197
  129. def OAI.SnakyConditional.childrenD_576 line 198
  130. theorem OAI.SnakyConditional.common_sub_576 line 199
  131. theorem OAI.SnakyConditional.child_required_sub_576 line 200
  132. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_0 line 201
  133. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_1 line 203
  134. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_2 line 205
  135. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_3 line 207
  136. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_4 line 209
  137. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_5 line 211
  138. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_6 line 213
  139. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_7 line 215
  140. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_8 line 217
  141. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_576_9 line 219
  142. theorem OAI.SnakyConditional.child_envelope_sub_576 line 221
  143. theorem OAI.SnakyConditional.pivot_mem_576 line 234
  144. theorem OAI.SnakyConditional.children_work_576 line 235
  145. theorem OAI.SnakyConditional.row_works_576 line 248