OAI/Combinatorics/IndependentSets/PCP/GraphTables.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.GraphTables.Label line 11
2. abbrev OAI.IndependentSetsGames.Foundations.PCP.GraphTables.RelationTable line 12
3. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationIndex line 14
4. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationIndex_val line 16
5. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationAt line 19
6. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationOf line 22
7. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationAt_relationOf line 25
8. structure OAI.IndependentSetsGames.Foundations.PCP.GraphTables.DartRow line 29
9. abbrev OAI.IndependentSetsGames.Foundations.PCP.GraphTables.Rows line 34
10. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.reverseAt line 36
11. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.acceptsAt line 39
12. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.Valid line 42
13. instance OAI.IndependentSetsGames.Foundations.PCP.GraphTables.(instance at line 46) line 46
14. structure OAI.IndependentSetsGames.Foundations.PCP.GraphTables.Table line 50
15. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowList line 56
16. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowList_length line 58
17. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics line 61
18. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_reverse line 72
19. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_tail line 75
20. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_accepts line 78
21. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.graphRows line 81
22. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.reverseAt_graphRows line 84
23. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.acceptsAt_graphRows line 89
24. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.graphRows_valid line 94
25. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.ofGraph line 102
26. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 105
27. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 110
28. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 116
29. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 121
30. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.constraintGraph_ext line 126
31. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_ofGraph line 140
32. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 149
33. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.enumeratedGraph line 155
34. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 171
35. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 179
36. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.ofEnumeratedGraph line 191
37. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.bitWord line 195
38. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseBit line 197
39. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseBit_bitWord line 202
40. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseBits_bitWords line 205
41. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationWords line 211
42. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationWords_length line 213
43. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseRelation line 216
44. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseRelation_encoded line 222
45. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowWords line 229
46. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseRow line 232
47. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseRow_encoded line 240
48. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseRows line 248
49. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.parseRows_encoded line 256
50. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.tableWords line 262
51. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.tableBits line 265
52. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.decodeTableWords line 267
53. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.decodeTableWords_encoded line 278
54. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.decodeTableBits line 286
55. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.decodeTableBits_encoded line 289
56. def OAI.IndependentSetsGames.Foundations.PCP.GraphTables.encoding line 293
57. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.tableBits_injective line 298
58. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowWords_length line 300
59. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowsWords_length line 303
60. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.tableWords_length line 309
61. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.tableWords_length_le_bits line 314
62. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.relationBits_length_le line 319
63. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowBits_length_le line 327
64. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.rowsBits_length_le line 336
65. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.tableBits_length_le line 346
66. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 355
67. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTables.darts_le_tableBits_length line 361