OAI/GameTheory/SnakyConditional/Templates/Level29Part05.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_599 line 8
  2. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_4 line 9
  3. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_4_chain line 10
  4. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_4_head line 11
  5. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_4_last line 12
  6. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_5 line 13
  7. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_5_chain line 14
  8. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_5_head line 15
  9. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_5_last line 16
  10. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_3 line 17
  11. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_3_chain line 18
  12. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_3_head line 21
  13. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_3_last line 23
  14. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_7 line 25
  15. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_7_chain line 26
  16. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_7_head line 27
  17. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_7_last line 28
  18. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_8 line 29
  19. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_8_chain line 30
  20. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_8_head line 31
  21. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_8_last line 32
  22. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_6 line 33
  23. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_6_chain line 34
  24. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_6_head line 37
  25. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_6_last line 39
  26. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_2 line 41
  27. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_2_chain line 42
  28. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_2_head line 45
  29. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_2_last line 47
  30. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_11 line 49
  31. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_11_chain line 50
  32. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_11_head line 51
  33. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_11_last line 52
  34. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_12 line 53
  35. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_12_chain line 54
  36. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_12_head line 55
  37. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_12_last line 56
  38. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_10 line 57
  39. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_10_chain line 58
  40. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_10_head line 61
  41. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_10_last line 63
  42. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_14 line 65
  43. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_14_chain line 66
  44. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_14_head line 67
  45. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_14_last line 68
  46. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_15 line 69
  47. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_15_chain line 70
  48. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_15_head line 71
  49. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_15_last line 72
  50. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_13 line 73
  51. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_13_chain line 74
  52. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_13_head line 77
  53. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_13_last line 79
  54. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_9 line 81
  55. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_9_chain line 82
  56. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_9_head line 85
  57. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_9_last line 87
  58. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_1 line 89
  59. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_1_chain line 90
  60. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_1_head line 93
  61. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_1_last line 95
  62. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_19 line 97
  63. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_19_chain line 98
  64. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_19_head line 99
  65. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_19_last line 100
  66. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_20 line 101
  67. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_20_chain line 102
  68. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_20_head line 103
  69. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_20_last line 104
  70. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_18 line 105
  71. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_18_chain line 106
  72. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_18_head line 109
  73. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_18_last line 111
  74. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_22 line 113
  75. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_22_chain line 114
  76. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_22_head line 115
  77. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_22_last line 116
  78. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_23 line 117
  79. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_23_chain line 118
  80. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_23_head line 119
  81. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_23_last line 120
  82. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_21 line 121
  83. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_21_chain line 122
  84. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_21_head line 125
  85. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_21_last line 127
  86. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_17 line 129
  87. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_17_chain line 130
  88. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_17_head line 133
  89. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_17_last line 135
  90. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_26 line 137
  91. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_26_chain line 138
  92. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_26_head line 139
  93. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_26_last line 140
  94. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_27 line 141
  95. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_27_chain line 142
  96. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_27_head line 143
  97. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_27_last line 144
  98. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_25 line 145
  99. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_25_chain line 146
  100. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_25_head line 149
  101. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_25_last line 151
  102. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_29 line 153
  103. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_29_chain line 154
  104. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_29_head line 155
  105. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_29_last line 156
  106. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_30 line 157
  107. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_30_chain line 158
  108. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_30_head line 159
  109. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_30_last line 160
  110. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_28 line 161
  111. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_28_chain line 162
  112. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_28_head line 165
  113. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_28_last line 167
  114. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_24 line 169
  115. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_24_chain line 170
  116. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_24_head line 173
  117. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_24_last line 175
  118. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_16 line 177
  119. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_16_chain line 178
  120. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_16_head line 181
  121. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_16_last line 183
  122. def OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_0 line 185
  123. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_0_chain line 186
  124. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_0_head line 189
  125. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_0_last line 191
  126. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_envelope_599_nodup line 193
  127. def OAI.SnakyConditional.envelope_599 line 195
  128. def OAI.SnakyConditional.childrenC_599 line 196
  129. def OAI.SnakyConditional.childrenD_599 line 197
  130. theorem OAI.SnakyConditional.common_sub_599 line 198
  131. theorem OAI.SnakyConditional.child_required_sub_599 line 199
  132. theorem OAI.SnakyConditional.Internal.SnakyRows011D.containment_599_0 line 200
  133. theorem OAI.SnakyConditional.Internal.SnakyRows011D.containment_599_1 line 202
  134. theorem OAI.SnakyConditional.Internal.SnakyRows011D.containment_599_2 line 204
  135. theorem OAI.SnakyConditional.Internal.SnakyRows011D.containment_599_3 line 206
  136. theorem OAI.SnakyConditional.Internal.SnakyRows011D.containment_599_4 line 208
  137. theorem OAI.SnakyConditional.Internal.SnakyRows011D.containment_599_5 line 210
  138. theorem OAI.SnakyConditional.child_envelope_sub_599 line 212
  139. theorem OAI.SnakyConditional.pivot_mem_599 line 221
  140. theorem OAI.SnakyConditional.children_work_599 line 222
  141. theorem OAI.SnakyConditional.row_works_599 line 231