OAI/Combinatorics/IndependentSets/PCP/Enumeration.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 11
2. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 13
3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 15
4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 18
5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 22
6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 28
7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 32
8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 36
9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 40
10. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 41
11. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 42
12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.localCount line 43
13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 44
14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 45
15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 46
16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 47
17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 49
18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 52
19. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 53
20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 56
21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 59
22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 62
23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 70
24. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 76
25. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 78
26. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 83
27. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 86
28. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 89
29. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 92
30. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 95
31. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 98
32. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 103
33. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 107
34. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 116
35. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 121
36. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 125
37. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 130
38. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 135
39. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 140
40. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 142
41. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 146
42. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 151
43. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 159
44. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 168
45. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 175
46. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 182
47. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 189
48. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 193
49. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 200
50. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 208
51. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 216
52. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered line 222
53. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 225
54. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 228
55. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 233
56. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 238
57. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 240
58. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 242
59. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 248
60. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 264
61. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 284
62. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 287
63. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 290
64. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 297
65. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 308
66. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 311
67. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 315
68. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_event line 319
69. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_address line 323
70. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 327
71. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 332
72. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 337