OAI/GameTheory/SnakyConditional/Templates/Level30Part03.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_594 line 6
2. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_4 line 7
3. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_4_chain line 8
4. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_4_head line 9
5. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_4_last line 10
6. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_5 line 11
7. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_5_chain line 12
8. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_5_head line 13
9. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_5_last line 14
10. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_3 line 15
11. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_3_chain line 16
12. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_3_head line 19
13. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_3_last line 21
14. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_7 line 23
15. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_7_chain line 24
16. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_7_head line 25
17. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_7_last line 26
18. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_8 line 27
19. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_8_chain line 28
20. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_8_head line 29
21. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_8_last line 30
22. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_6 line 31
23. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_6_chain line 32
24. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_6_head line 35
25. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_6_last line 37
26. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_2 line 39
27. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_2_chain line 40
28. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_2_head line 43
29. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_2_last line 45
30. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_11 line 47
31. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_11_chain line 48
32. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_11_head line 49
33. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_11_last line 50
34. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_12 line 51
35. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_12_chain line 52
36. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_12_head line 53
37. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_12_last line 54
38. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_10 line 55
39. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_10_chain line 56
40. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_10_head line 59
41. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_10_last line 61
42. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_14 line 63
43. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_14_chain line 64
44. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_14_head line 65
45. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_14_last line 66
46. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_15 line 67
47. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_15_chain line 68
48. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_15_head line 69
49. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_15_last line 70
50. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_13 line 71
51. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_13_chain line 72
52. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_13_head line 75
53. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_13_last line 77
54. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_9 line 79
55. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_9_chain line 80
56. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_9_head line 83
57. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_9_last line 85
58. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_1 line 87
59. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_1_chain line 88
60. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_1_head line 91
61. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_1_last line 93
62. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_19 line 95
63. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_19_chain line 96
64. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_19_head line 97
65. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_19_last line 98
66. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_20 line 99
67. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_20_chain line 100
68. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_20_head line 101
69. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_20_last line 102
70. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_18 line 103
71. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_18_chain line 104
72. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_18_head line 107
73. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_18_last line 109
74. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_22 line 111
75. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_22_chain line 112
76. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_22_head line 113
77. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_22_last line 114
78. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_23 line 115
79. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_23_chain line 116
80. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_23_head line 117
81. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_23_last line 118
82. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_21 line 119
83. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_21_chain line 120
84. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_21_head line 123
85. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_21_last line 125
86. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_17 line 127
87. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_17_chain line 128
88. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_17_head line 131
89. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_17_last line 133
90. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_26 line 135
91. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_26_chain line 136
92. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_26_head line 137
93. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_26_last line 138
94. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_27 line 139
95. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_27_chain line 140
96. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_27_head line 141
97. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_27_last line 142
98. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_25 line 143
99. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_25_chain line 144
100. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_25_head line 147
101. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_25_last line 149
102. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_29 line 151
103. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_29_chain line 152
104. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_29_head line 153
105. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_29_last line 154
106. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_30 line 155
107. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_30_chain line 156
108. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_30_head line 157
109. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_30_last line 158
110. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_28 line 159
111. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_28_chain line 160
112. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_28_head line 163
113. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_28_last line 165
114. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_24 line 167
115. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_24_chain line 168
116. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_24_head line 171
117. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_24_last line 173
118. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_16 line 175
119. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_16_chain line 176
120. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_16_head line 179
121. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_16_last line 181
122. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_0 line 183
123. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_0_chain line 184
124. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_0_head line 187
125. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_0_last line 189
126. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_594_nodup line 191
127. def OAI.SnakyConditional.envelope_594 line 193
128. def OAI.SnakyConditional.childrenC_594 line 194
129. def OAI.SnakyConditional.childrenD_594 line 195
130. theorem OAI.SnakyConditional.common_sub_594 line 196
131. theorem OAI.SnakyConditional.child_required_sub_594 line 197
132. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_594_0 line 198
133. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_594_1 line 200
134. theorem OAI.SnakyConditional.Internal.SnakyRows010.containment_594_2 line 202
135. theorem OAI.SnakyConditional.child_envelope_sub_594 line 204
136. theorem OAI.SnakyConditional.pivot_mem_594 line 210
137. theorem OAI.SnakyConditional.children_work_594 line 211
138. theorem OAI.SnakyConditional.row_works_594 line 217