OAI/GameTheory/SnakyConditional/Templates/Level27Part04.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_579 line 7
  2. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_4 line 8
  3. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_4_chain line 9
  4. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_4_head line 10
  5. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_4_last line 11
  6. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_5 line 12
  7. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_5_chain line 13
  8. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_5_head line 14
  9. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_5_last line 15
  10. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_3 line 16
  11. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_3_chain line 17
  12. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_3_head line 20
  13. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_3_last line 22
  14. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_7 line 24
  15. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_7_chain line 25
  16. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_7_head line 26
  17. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_7_last line 27
  18. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_8 line 28
  19. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_8_chain line 29
  20. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_8_head line 30
  21. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_8_last line 31
  22. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_6 line 32
  23. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_6_chain line 33
  24. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_6_head line 36
  25. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_6_last line 38
  26. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_2 line 40
  27. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_2_chain line 41
  28. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_2_head line 44
  29. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_2_last line 46
  30. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_11 line 48
  31. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_11_chain line 49
  32. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_11_head line 50
  33. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_11_last line 51
  34. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_12 line 52
  35. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_12_chain line 53
  36. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_12_head line 54
  37. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_12_last line 55
  38. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_10 line 56
  39. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_10_chain line 57
  40. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_10_head line 60
  41. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_10_last line 62
  42. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_14 line 64
  43. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_14_chain line 65
  44. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_14_head line 66
  45. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_14_last line 67
  46. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_15 line 68
  47. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_15_chain line 69
  48. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_15_head line 70
  49. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_15_last line 71
  50. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_13 line 72
  51. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_13_chain line 73
  52. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_13_head line 76
  53. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_13_last line 78
  54. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_9 line 80
  55. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_9_chain line 81
  56. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_9_head line 84
  57. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_9_last line 86
  58. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_1 line 88
  59. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_1_chain line 89
  60. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_1_head line 92
  61. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_1_last line 94
  62. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_19 line 96
  63. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_19_chain line 97
  64. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_19_head line 98
  65. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_19_last line 99
  66. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_20 line 100
  67. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_20_chain line 101
  68. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_20_head line 102
  69. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_20_last line 103
  70. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_18 line 104
  71. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_18_chain line 105
  72. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_18_head line 108
  73. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_18_last line 110
  74. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_22 line 112
  75. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_22_chain line 113
  76. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_22_head line 114
  77. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_22_last line 115
  78. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_23 line 116
  79. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_23_chain line 117
  80. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_23_head line 118
  81. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_23_last line 119
  82. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_21 line 120
  83. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_21_chain line 121
  84. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_21_head line 124
  85. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_21_last line 126
  86. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_17 line 128
  87. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_17_chain line 129
  88. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_17_head line 132
  89. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_17_last line 134
  90. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_26 line 136
  91. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_26_chain line 137
  92. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_26_head line 138
  93. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_26_last line 139
  94. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_27 line 140
  95. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_27_chain line 141
  96. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_27_head line 142
  97. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_27_last line 143
  98. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_25 line 144
  99. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_25_chain line 145
  100. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_25_head line 148
  101. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_25_last line 150
  102. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_29 line 152
  103. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_29_chain line 153
  104. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_29_head line 154
  105. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_29_last line 155
  106. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_30 line 156
  107. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_30_chain line 157
  108. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_30_head line 158
  109. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_30_last line 159
  110. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_28 line 160
  111. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_28_chain line 161
  112. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_28_head line 164
  113. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_28_last line 166
  114. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_24 line 168
  115. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_24_chain line 169
  116. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_24_head line 172
  117. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_24_last line 174
  118. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_16 line 176
  119. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_16_chain line 177
  120. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_16_head line 180
  121. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_16_last line 182
  122. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_0 line 184
  123. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_0_chain line 185
  124. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_0_head line 188
  125. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_0_last line 190
  126. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_579_nodup line 192
  127. def OAI.SnakyConditional.envelope_579 line 194
  128. def OAI.SnakyConditional.childrenC_579 line 195
  129. def OAI.SnakyConditional.childrenD_579 line 196
  130. theorem OAI.SnakyConditional.common_sub_579 line 197
  131. theorem OAI.SnakyConditional.child_required_sub_579 line 198
  132. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_579_0 line 199
  133. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_579_1 line 201
  134. theorem OAI.SnakyConditional.child_envelope_sub_579 line 203
  135. theorem OAI.SnakyConditional.pivot_mem_579 line 208
  136. theorem OAI.SnakyConditional.children_work_579 line 209
  137. theorem OAI.SnakyConditional.row_works_579 line 214