OAI/GameTheory/SnakyConditional/Templates/Level28Part04.lean

GitHub source file

148 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_586 line 12
2. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_4 line 13
3. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_4_chain line 14
4. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_4_head line 15
5. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_4_last line 16
6. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_5 line 17
7. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_5_chain line 18
8. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_5_head line 19
9. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_5_last line 20
10. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_3 line 21
11. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_3_chain line 22
12. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_3_head line 25
13. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_3_last line 27
14. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_7 line 29
15. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_7_chain line 30
16. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_7_head line 31
17. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_7_last line 32
18. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_8 line 33
19. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_8_chain line 34
20. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_8_head line 35
21. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_8_last line 36
22. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_6 line 37
23. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_6_chain line 38
24. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_6_head line 41
25. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_6_last line 43
26. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_2 line 45
27. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_2_chain line 46
28. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_2_head line 49
29. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_2_last line 51
30. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_11 line 53
31. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_11_chain line 54
32. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_11_head line 55
33. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_11_last line 56
34. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_12 line 57
35. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_12_chain line 58
36. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_12_head line 59
37. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_12_last line 60
38. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_10 line 61
39. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_10_chain line 62
40. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_10_head line 65
41. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_10_last line 67
42. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_14 line 69
43. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_14_chain line 70
44. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_14_head line 71
45. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_14_last line 72
46. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_15 line 73
47. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_15_chain line 74
48. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_15_head line 75
49. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_15_last line 76
50. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_13 line 77
51. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_13_chain line 78
52. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_13_head line 81
53. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_13_last line 83
54. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_9 line 85
55. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_9_chain line 86
56. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_9_head line 89
57. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_9_last line 91
58. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_1 line 93
59. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_1_chain line 94
60. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_1_head line 97
61. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_1_last line 99
62. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_19 line 101
63. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_19_chain line 102
64. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_19_head line 103
65. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_19_last line 104
66. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_20 line 105
67. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_20_chain line 106
68. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_20_head line 107
69. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_20_last line 108
70. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_18 line 109
71. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_18_chain line 110
72. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_18_head line 113
73. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_18_last line 115
74. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_22 line 117
75. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_22_chain line 118
76. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_22_head line 119
77. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_22_last line 120
78. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_23 line 121
79. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_23_chain line 122
80. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_23_head line 123
81. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_23_last line 124
82. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_21 line 125
83. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_21_chain line 126
84. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_21_head line 129
85. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_21_last line 131
86. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_17 line 133
87. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_17_chain line 134
88. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_17_head line 137
89. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_17_last line 139
90. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_26 line 141
91. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_26_chain line 142
92. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_26_head line 143
93. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_26_last line 144
94. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_27 line 145
95. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_27_chain line 146
96. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_27_head line 147
97. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_27_last line 148
98. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_25 line 149
99. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_25_chain line 150
100. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_25_head line 153
101. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_25_last line 155
102. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_29 line 157
103. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_29_chain line 158
104. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_29_head line 159
105. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_29_last line 160
106. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_30 line 161
107. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_30_chain line 162
108. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_30_head line 163
109. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_30_last line 164
110. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_28 line 165
111. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_28_chain line 166
112. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_28_head line 169
113. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_28_last line 171
114. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_24 line 173
115. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_24_chain line 174
116. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_24_head line 177
117. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_24_last line 179
118. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_16 line 181
119. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_16_chain line 182
120. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_16_head line 185
121. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_16_last line 187
122. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_0 line 189
123. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_0_chain line 190
124. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_0_head line 193
125. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_0_last line 195
126. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_586_nodup line 197
127. def OAI.SnakyConditional.envelope_586 line 199
128. def OAI.SnakyConditional.childrenC_586 line 200
129. def OAI.SnakyConditional.childrenD_586 line 201
130. theorem OAI.SnakyConditional.common_sub_586 line 202
131. theorem OAI.SnakyConditional.child_required_sub_586 line 203
132. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_0 line 204
133. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_1 line 206
134. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_2 line 208
135. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_3 line 210
136. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_4 line 212
137. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_5 line 214
138. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_6 line 216
139. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_7 line 218
140. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_8 line 220
141. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_9 line 222
142. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_10 line 224
143. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_11 line 226
144. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_586_12 line 228
145. theorem OAI.SnakyConditional.child_envelope_sub_586 line 230
146. theorem OAI.SnakyConditional.pivot_mem_586 line 246
147. theorem OAI.SnakyConditional.children_work_586 line 247
148. theorem OAI.SnakyConditional.row_works_586 line 263