OAI/GameTheory/SnakyConditional/Templates/Level24Part05.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_587 line 9
2. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_4 line 10
3. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_4_chain line 11
4. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_4_head line 12
5. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_4_last line 13
6. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_5 line 14
7. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_5_chain line 15
8. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_5_head line 16
9. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_5_last line 17
10. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_3 line 18
11. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_3_chain line 19
12. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_3_head line 22
13. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_3_last line 24
14. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_7 line 26
15. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_7_chain line 27
16. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_7_head line 28
17. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_7_last line 29
18. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_8 line 30
19. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_8_chain line 31
20. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_8_head line 32
21. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_8_last line 33
22. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_6 line 34
23. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_6_chain line 35
24. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_6_head line 38
25. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_6_last line 40
26. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_2 line 42
27. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_2_chain line 43
28. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_2_head line 46
29. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_2_last line 48
30. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_11 line 50
31. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_11_chain line 51
32. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_11_head line 52
33. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_11_last line 53
34. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_12 line 54
35. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_12_chain line 55
36. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_12_head line 56
37. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_12_last line 57
38. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_10 line 58
39. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_10_chain line 59
40. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_10_head line 62
41. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_10_last line 64
42. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_14 line 66
43. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_14_chain line 67
44. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_14_head line 68
45. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_14_last line 69
46. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_15 line 70
47. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_15_chain line 71
48. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_15_head line 72
49. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_15_last line 73
50. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_13 line 74
51. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_13_chain line 75
52. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_13_head line 78
53. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_13_last line 80
54. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_9 line 82
55. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_9_chain line 83
56. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_9_head line 86
57. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_9_last line 88
58. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_1 line 90
59. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_1_chain line 91
60. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_1_head line 94
61. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_1_last line 96
62. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_19 line 98
63. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_19_chain line 99
64. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_19_head line 100
65. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_19_last line 101
66. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_20 line 102
67. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_20_chain line 103
68. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_20_head line 104
69. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_20_last line 105
70. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_18 line 106
71. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_18_chain line 107
72. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_18_head line 110
73. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_18_last line 112
74. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_22 line 114
75. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_22_chain line 115
76. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_22_head line 116
77. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_22_last line 117
78. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_23 line 118
79. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_23_chain line 119
80. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_23_head line 120
81. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_23_last line 121
82. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_21 line 122
83. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_21_chain line 123
84. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_21_head line 126
85. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_21_last line 128
86. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_17 line 130
87. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_17_chain line 131
88. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_17_head line 134
89. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_17_last line 136
90. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_26 line 138
91. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_26_chain line 139
92. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_26_head line 140
93. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_26_last line 141
94. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_27 line 142
95. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_27_chain line 143
96. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_27_head line 144
97. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_27_last line 145
98. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_25 line 146
99. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_25_chain line 147
100. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_25_head line 150
101. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_25_last line 152
102. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_29 line 154
103. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_29_chain line 155
104. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_29_head line 156
105. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_29_last line 157
106. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_30 line 158
107. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_30_chain line 159
108. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_30_head line 160
109. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_30_last line 161
110. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_28 line 162
111. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_28_chain line 163
112. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_28_head line 166
113. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_28_last line 168
114. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_24 line 170
115. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_24_chain line 171
116. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_24_head line 174
117. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_24_last line 176
118. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_16 line 178
119. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_16_chain line 179
120. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_16_head line 182
121. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_16_last line 184
122. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_0 line 186
123. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_0_chain line 187
124. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_0_head line 190
125. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_0_last line 192
126. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_587_nodup line 194
127. def OAI.SnakyConditional.envelope_587 line 196
128. def OAI.SnakyConditional.childrenC_587 line 197
129. def OAI.SnakyConditional.childrenD_587 line 198
130. theorem OAI.SnakyConditional.common_sub_587 line 199
131. theorem OAI.SnakyConditional.child_required_sub_587 line 200
132. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_587_0 line 201
133. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_587_1 line 203
134. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_587_2 line 205
135. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_587_3 line 207
136. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_587_4 line 209
137. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_587_5 line 211
138. theorem OAI.SnakyConditional.child_envelope_sub_587 line 213
139. theorem OAI.SnakyConditional.pivot_mem_587 line 222
140. theorem OAI.SnakyConditional.children_work_587 line 223
141. theorem OAI.SnakyConditional.row_works_587 line 232