OAI/GameTheory/SnakyConditional/Regions/Region595.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.Internal.SnakyRows010.namedCellKey line 6
2. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_nodup_of_chain line 7
3. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_chain_append line 10
4. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_head_append line 24
5. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_last_append line 29
6. theorem OAI.SnakyConditional.Internal.SnakyRows010.required_595_nodup line 34
7. def OAI.SnakyConditional.required_595 line 36
8. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_4 line 38
9. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_4_chain line 39
10. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_4_last line 40
11. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_5 line 41
12. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_5_chain line 42
13. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_5_head line 43
14. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_5_last line 44
15. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_3 line 45
16. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_3_chain line 46
17. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_3_last line 49
18. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_7 line 51
19. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_7_chain line 52
20. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_7_head line 53
21. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_7_last line 54
22. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_8 line 55
23. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_8_chain line 56
24. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_8_head line 57
25. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_8_last line 58
26. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_6 line 59
27. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_6_chain line 60
28. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_6_head line 63
29. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_6_last line 65
30. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_2 line 67
31. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_2_chain line 68
32. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_2_last line 71
33. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_11 line 73
34. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_11_chain line 74
35. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_11_head line 75
36. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_11_last line 76
37. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_12 line 77
38. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_12_chain line 78
39. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_12_head line 79
40. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_12_last line 80
41. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_10 line 81
42. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_10_chain line 82
43. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_10_head line 85
44. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_10_last line 87
45. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_14 line 89
46. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_14_chain line 90
47. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_14_head line 91
48. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_14_last line 92
49. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_15 line 93
50. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_15_chain line 94
51. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_15_head line 95
52. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_15_last line 96
53. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_13 line 97
54. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_13_chain line 98
55. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_13_head line 101
56. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_13_last line 103
57. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_9 line 105
58. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_9_chain line 106
59. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_9_head line 109
60. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_9_last line 111
61. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_1 line 113
62. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_1_chain line 114
63. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_1_last line 117
64. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_19 line 119
65. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_19_chain line 120
66. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_19_head line 121
67. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_19_last line 122
68. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_20 line 123
69. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_20_chain line 124
70. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_20_head line 125
71. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_20_last line 126
72. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_18 line 127
73. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_18_chain line 128
74. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_18_head line 131
75. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_18_last line 133
76. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_22 line 135
77. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_22_chain line 136
78. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_22_head line 137
79. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_22_last line 138
80. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_23 line 139
81. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_23_chain line 140
82. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_23_head line 141
83. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_23_last line 142
84. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_21 line 143
85. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_21_chain line 144
86. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_21_head line 147
87. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_21_last line 149
88. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_17 line 151
89. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_17_chain line 152
90. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_17_head line 155
91. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_17_last line 157
92. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_26 line 159
93. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_26_chain line 160
94. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_26_head line 161
95. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_26_last line 162
96. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_27 line 163
97. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_27_chain line 164
98. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_27_head line 165
99. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_27_last line 166
100. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_25 line 167
101. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_25_chain line 168
102. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_25_head line 171
103. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_25_last line 173
104. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_29 line 175
105. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_29_chain line 176
106. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_29_head line 177
107. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_29_last line 178
108. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_30 line 179
109. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_30_chain line 180
110. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_30_head line 181
111. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_28 line 182
112. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_28_chain line 183
113. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_28_head line 186
114. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_24 line 188
115. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_24_chain line 189
116. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_24_head line 192
117. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_16 line 194
118. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_16_chain line 195
119. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_16_head line 198
120. def OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_0 line 200
121. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_0_chain line 201
122. theorem OAI.SnakyConditional.Internal.SnakyRows010.named_envelope_595_nodup line 204
123. def OAI.SnakyConditional.envelope_595 line 206