OAI/GameTheory/SnakyConditional/Templates/Operations.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.placedSet line 6
2. theorem OAI.SnakyConditional.placedSet_eq_image line 8
3. theorem OAI.SnakyConditional.placed_template_map line 12
4. def OAI.SnakyConditional.commonEnvelope line 16
5. theorem OAI.SnakyConditional.mem_commonEnvelope line 18
6. def OAI.SnakyConditional.Internal.SnakyRows008.cf17CellKey line 21
7. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_multiset_nodup_of_key_chain line 22
8. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_key_chain_append line 25
9. def OAI.SnakyConditional.Internal.SnakyRows009.namedCellKey line 33
10. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_nodup_of_chain line 34
11. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_chain_append line 37
12. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_head_append line 51
13. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_last_append line 56
14. def OAI.SnakyConditional.Internal.SnakyRows011A.namedCellKey line 61
15. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_nodup_of_chain line 62
16. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_chain_append line 65
17. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_head_append line 79
18. theorem OAI.SnakyConditional.Internal.SnakyRows011A.named_last_append line 84
19. def OAI.SnakyConditional.Internal.SnakyRows011B.namedCellKey line 89
20. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_nodup_of_chain line 90
21. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_chain_append line 93
22. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_head_append line 107
23. theorem OAI.SnakyConditional.Internal.SnakyRows011B.named_last_append line 112
24. def OAI.SnakyConditional.Internal.SnakyRows011C.namedCellKey line 117
25. theorem OAI.SnakyConditional.Internal.SnakyRows011C.named_nodup_of_chain line 118
26. theorem OAI.SnakyConditional.Internal.SnakyRows011C.named_chain_append line 121
27. theorem OAI.SnakyConditional.Internal.SnakyRows011C.named_head_append line 135
28. theorem OAI.SnakyConditional.Internal.SnakyRows011C.named_last_append line 140
29. def OAI.SnakyConditional.Internal.SnakyRows011D.namedCellKey line 145
30. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_nodup_of_chain line 146
31. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_chain_append line 149
32. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_head_append line 163
33. theorem OAI.SnakyConditional.Internal.SnakyRows011D.named_last_append line 168
34. def OAI.SnakyConditional.Internal.SnakyRows011E.namedCellKey line 173
35. theorem OAI.SnakyConditional.Internal.SnakyRows011E.named_nodup_of_chain line 174
36. theorem OAI.SnakyConditional.Internal.SnakyRows011E.named_chain_append line 177
37. theorem OAI.SnakyConditional.Internal.SnakyRows011E.named_head_append line 191
38. theorem OAI.SnakyConditional.Internal.SnakyRows011E.named_last_append line 196
39. def OAI.SnakyConditional.Internal.SnakyRows011F.namedCellKey line 201
40. theorem OAI.SnakyConditional.Internal.SnakyRows011F.named_nodup_of_chain line 202
41. theorem OAI.SnakyConditional.Internal.SnakyRows011F.named_chain_append line 205
42. theorem OAI.SnakyConditional.Internal.SnakyRows011F.named_head_append line 219
43. theorem OAI.SnakyConditional.Internal.SnakyRows011F.named_last_append line 224
44. def OAI.SnakyConditional.Internal.SnakyRows011G.namedCellKey line 229
45. theorem OAI.SnakyConditional.Internal.SnakyRows011G.named_nodup_of_chain line 230
46. theorem OAI.SnakyConditional.Internal.SnakyRows011G.named_chain_append line 233
47. theorem OAI.SnakyConditional.Internal.SnakyRows011G.named_head_append line 247
48. theorem OAI.SnakyConditional.Internal.SnakyRows011G.named_last_append line 252
49. def OAI.SnakyConditional.Internal.SnakyRows011I.namedCellKey line 257
50. theorem OAI.SnakyConditional.Internal.SnakyRows011I.named_nodup_of_chain line 258
51. theorem OAI.SnakyConditional.Internal.SnakyRows011I.named_chain_append line 261
52. theorem OAI.SnakyConditional.Internal.SnakyRows011I.named_head_append line 275
53. theorem OAI.SnakyConditional.Internal.SnakyRows011I.named_last_append line 280
54. def OAI.SnakyConditional.Internal.SnakyRows011.namedCellKey line 285
55. theorem OAI.SnakyConditional.Internal.SnakyRows011.named_nodup_of_chain line 286
56. theorem OAI.SnakyConditional.Internal.SnakyRows011.named_chain_append line 289
57. theorem OAI.SnakyConditional.Internal.SnakyRows011.named_head_append line 303
58. theorem OAI.SnakyConditional.Internal.SnakyRows011.named_last_append line 308
59. def OAI.SnakyConditional.Internal.SnakyRows012A.namedCellKey line 313
60. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_nodup_of_chain line 314
61. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_chain_append line 317
62. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_head_append line 331
63. theorem OAI.SnakyConditional.Internal.SnakyRows012A.named_last_append line 336
64. def OAI.SnakyConditional.Internal.SnakyRows012B.namedCellKey line 341
65. theorem OAI.SnakyConditional.Internal.SnakyRows012B.named_nodup_of_chain line 342
66. theorem OAI.SnakyConditional.Internal.SnakyRows012B.named_chain_append line 345
67. theorem OAI.SnakyConditional.Internal.SnakyRows012B.named_head_append line 359
68. theorem OAI.SnakyConditional.Internal.SnakyRows012B.named_last_append line 364
69. def OAI.SnakyConditional.Internal.SnakyRows012C.namedCellKey line 369
70. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_nodup_of_chain line 370
71. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_chain_append line 373
72. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_head_append line 387
73. theorem OAI.SnakyConditional.Internal.SnakyRows012C.named_last_append line 392
74. theorem OAI.SnakyConditional.Internal.SnakyRows012C.placedSet_subset_of_points line 397
75. def OAI.SnakyConditional.Internal.SnakyRows012D.namedCellKey line 404
76. theorem OAI.SnakyConditional.Internal.SnakyRows012D.named_nodup_of_chain line 405
77. theorem OAI.SnakyConditional.Internal.SnakyRows012D.named_chain_append line 408
78. theorem OAI.SnakyConditional.Internal.SnakyRows012D.named_head_append line 422
79. theorem OAI.SnakyConditional.Internal.SnakyRows012D.named_last_append line 427
80. theorem OAI.SnakyConditional.Internal.SnakyRows012D.placedSet_subset_of_points line 432
81. def OAI.SnakyConditional.Internal.SnakyRows012.namedCellKey line 439
82. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_nodup_of_chain line 440
83. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_chain_append line 443
84. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_head_append line 457
85. theorem OAI.SnakyConditional.Internal.SnakyRows012.named_last_append line 462
86. theorem OAI.SnakyConditional.Internal.SnakyRows012.placedSet_subset_of_points line 467
87. def OAI.SnakyConditional.Internal.SnakyRows013.namedCellKey line 474
88. theorem OAI.SnakyConditional.Internal.SnakyRows013.named_nodup_of_chain line 475
89. theorem OAI.SnakyConditional.Internal.SnakyRows013.named_chain_append line 478
90. theorem OAI.SnakyConditional.Internal.SnakyRows013.named_head_append line 492
91. theorem OAI.SnakyConditional.Internal.SnakyRows013.named_last_append line 497
92. theorem OAI.SnakyConditional.Internal.SnakyRows013.placedSet_subset_of_points line 502
93. def OAI.SnakyConditional.Internal.SnakyRows014.namedCellKey line 509
94. theorem OAI.SnakyConditional.Internal.SnakyRows014.named_nodup_of_chain line 510
95. theorem OAI.SnakyConditional.Internal.SnakyRows014.named_chain_append line 513
96. theorem OAI.SnakyConditional.Internal.SnakyRows014.named_head_append line 527
97. theorem OAI.SnakyConditional.Internal.SnakyRows014.named_last_append line 532
98. theorem OAI.SnakyConditional.Internal.SnakyRows014.placedSet_subset_of_points line 537
99. def OAI.SnakyConditional.Internal.SnakyRows015.namedCellKey line 544
100. theorem OAI.SnakyConditional.Internal.SnakyRows015.named_nodup_of_chain line 545
101. theorem OAI.SnakyConditional.Internal.SnakyRows015.named_chain_append line 548
102. theorem OAI.SnakyConditional.Internal.SnakyRows015.named_head_append line 562
103. theorem OAI.SnakyConditional.Internal.SnakyRows015.named_last_append line 567
104. theorem OAI.SnakyConditional.Internal.SnakyRows015.placedSet_subset_of_points line 572
105. def OAI.SnakyConditional.Internal.SnakyRows016.namedCellKey line 579
106. theorem OAI.SnakyConditional.Internal.SnakyRows016.named_nodup_of_chain line 580
107. theorem OAI.SnakyConditional.Internal.SnakyRows016.named_chain_append line 583
108. theorem OAI.SnakyConditional.Internal.SnakyRows016.named_head_append line 597
109. theorem OAI.SnakyConditional.Internal.SnakyRows016.named_last_append line 602
110. theorem OAI.SnakyConditional.Internal.SnakyRows016.placedSet_subset_of_points line 607
111. theorem OAI.SnakyConditional.Internal.SnakyRows017.placedSet_subset_of_points line 614