OAI/GameTheory/SnakyConditional/Templates/Level25Part07.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_591 line 9
2. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_4 line 10
3. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_4_chain line 11
4. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_4_head line 12
5. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_4_last line 13
6. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_5 line 14
7. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_5_chain line 15
8. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_5_head line 16
9. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_5_last line 17
10. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_3 line 18
11. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_3_chain line 19
12. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_3_head line 22
13. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_3_last line 24
14. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_7 line 26
15. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_7_chain line 27
16. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_7_head line 28
17. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_7_last line 29
18. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_8 line 30
19. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_8_chain line 31
20. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_8_head line 32
21. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_8_last line 33
22. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_6 line 34
23. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_6_chain line 35
24. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_6_head line 38
25. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_6_last line 40
26. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_2 line 42
27. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_2_chain line 43
28. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_2_head line 46
29. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_2_last line 48
30. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_11 line 50
31. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_11_chain line 51
32. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_11_head line 52
33. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_11_last line 53
34. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_12 line 54
35. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_12_chain line 55
36. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_12_head line 56
37. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_12_last line 57
38. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_10 line 58
39. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_10_chain line 59
40. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_10_head line 62
41. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_10_last line 64
42. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_14 line 66
43. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_14_chain line 67
44. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_14_head line 68
45. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_14_last line 69
46. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_15 line 70
47. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_15_chain line 71
48. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_15_head line 72
49. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_15_last line 73
50. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_13 line 74
51. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_13_chain line 75
52. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_13_head line 78
53. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_13_last line 80
54. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_9 line 82
55. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_9_chain line 83
56. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_9_head line 86
57. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_9_last line 88
58. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_1 line 90
59. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_1_chain line 91
60. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_1_head line 94
61. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_1_last line 96
62. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_19 line 98
63. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_19_chain line 99
64. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_19_head line 100
65. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_19_last line 101
66. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_20 line 102
67. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_20_chain line 103
68. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_20_head line 104
69. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_20_last line 105
70. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_18 line 106
71. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_18_chain line 107
72. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_18_head line 110
73. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_18_last line 112
74. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_22 line 114
75. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_22_chain line 115
76. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_22_head line 116
77. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_22_last line 117
78. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_23 line 118
79. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_23_chain line 119
80. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_23_head line 120
81. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_23_last line 121
82. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_21 line 122
83. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_21_chain line 123
84. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_21_head line 126
85. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_21_last line 128
86. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_17 line 130
87. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_17_chain line 131
88. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_17_head line 134
89. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_17_last line 136
90. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_26 line 138
91. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_26_chain line 139
92. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_26_head line 140
93. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_26_last line 141
94. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_27 line 142
95. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_27_chain line 143
96. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_27_head line 144
97. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_27_last line 145
98. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_25 line 146
99. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_25_chain line 147
100. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_25_head line 150
101. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_25_last line 152
102. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_29 line 154
103. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_29_chain line 155
104. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_29_head line 156
105. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_29_last line 157
106. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_30 line 158
107. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_30_chain line 159
108. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_30_head line 160
109. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_30_last line 161
110. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_28 line 162
111. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_28_chain line 163
112. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_28_head line 166
113. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_28_last line 168
114. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_24 line 170
115. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_24_chain line 171
116. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_24_head line 174
117. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_24_last line 176
118. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_16 line 178
119. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_16_chain line 179
120. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_16_head line 182
121. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_16_last line 184
122. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_0 line 186
123. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_0_chain line 187
124. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_0_head line 190
125. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_0_last line 192
126. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_591_nodup line 194
127. def OAI.SnakyConditional.envelope_591 line 196
128. def OAI.SnakyConditional.childrenC_591 line 197
129. def OAI.SnakyConditional.childrenD_591 line 198
130. theorem OAI.SnakyConditional.common_sub_591 line 199
131. theorem OAI.SnakyConditional.child_required_sub_591 line 200
132. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_591_0 line 201
133. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_591_1 line 203
134. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_591_2 line 205
135. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_591_3 line 207
136. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_591_4 line 209
137. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_591_5 line 211
138. theorem OAI.SnakyConditional.child_envelope_sub_591 line 213
139. theorem OAI.SnakyConditional.pivot_mem_591 line 222
140. theorem OAI.SnakyConditional.children_work_591 line 223
141. theorem OAI.SnakyConditional.row_works_591 line 232