OAI/Computability/VertexCover/PCP/GraphTables.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.GraphTables.Label line 13
2. abbrev OAI.UniqueGames.Foundations.PCP.GraphTables.RelationTable line 14
3. def OAI.UniqueGames.Foundations.PCP.GraphTables.relationIndex line 16
4. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.relationIndex_val line 18
5. def OAI.UniqueGames.Foundations.PCP.GraphTables.relationAt line 21
6. def OAI.UniqueGames.Foundations.PCP.GraphTables.relationOf line 24
7. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.relationAt_relationOf line 27
8. structure OAI.UniqueGames.Foundations.PCP.GraphTables.DartRow line 31
9. abbrev OAI.UniqueGames.Foundations.PCP.GraphTables.Rows line 36
10. def OAI.UniqueGames.Foundations.PCP.GraphTables.reverseAt line 38
11. def OAI.UniqueGames.Foundations.PCP.GraphTables.acceptsAt line 41
12. def OAI.UniqueGames.Foundations.PCP.GraphTables.Valid line 44
13. instance OAI.UniqueGames.Foundations.PCP.GraphTables.(instance at line 48) line 48
14. structure OAI.UniqueGames.Foundations.PCP.GraphTables.Table line 52
15. def OAI.UniqueGames.Foundations.PCP.GraphTables.rowList line 58
16. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.rowList_length line 60
17. def OAI.UniqueGames.Foundations.PCP.GraphTables.semantics line 63
18. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_reverse line 74
19. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_tail line 77
20. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_accepts line 80
21. def OAI.UniqueGames.Foundations.PCP.GraphTables.graphRows line 83
22. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.reverseAt_graphRows line 86
23. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.acceptsAt_graphRows line 91
24. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.graphRows_valid line 96
25. def OAI.UniqueGames.Foundations.PCP.GraphTables.ofGraph line 104
26. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 107
27. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 112
28. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 118
29. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 123
30. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.constraintGraph_ext line 128
31. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_ofGraph line 142
32. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 151
33. def OAI.UniqueGames.Foundations.PCP.GraphTables.enumeratedGraph line 157
34. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 173
35. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 181
36. def OAI.UniqueGames.Foundations.PCP.GraphTables.ofEnumeratedGraph line 193
37. def OAI.UniqueGames.Foundations.PCP.GraphTables.bitWord line 197
38. def OAI.UniqueGames.Foundations.PCP.GraphTables.parseBit line 199
39. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.parseBit_bitWord line 204
40. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.parseBits_bitWords line 207
41. def OAI.UniqueGames.Foundations.PCP.GraphTables.relationWords line 213
42. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.relationWords_length line 215
43. def OAI.UniqueGames.Foundations.PCP.GraphTables.parseRelation line 218
44. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.parseRelation_encoded line 224
45. def OAI.UniqueGames.Foundations.PCP.GraphTables.rowWords line 231
46. def OAI.UniqueGames.Foundations.PCP.GraphTables.parseRow line 234
47. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.parseRow_encoded line 242
48. def OAI.UniqueGames.Foundations.PCP.GraphTables.parseRows line 250
49. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.parseRows_encoded line 258
50. def OAI.UniqueGames.Foundations.PCP.GraphTables.tableWords line 264
51. def OAI.UniqueGames.Foundations.PCP.GraphTables.tableBits line 267
52. def OAI.UniqueGames.Foundations.PCP.GraphTables.decodeTableWords line 269
53. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.decodeTableWords_encoded line 280
54. def OAI.UniqueGames.Foundations.PCP.GraphTables.decodeTableBits line 288
55. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.decodeTableBits_encoded line 291
56. def OAI.UniqueGames.Foundations.PCP.GraphTables.encoding line 295
57. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.tableBits_injective line 300
58. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.rowWords_length line 302
59. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.rowsWords_length line 305
60. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.tableWords_length line 311
61. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.tableWords_length_le_bits line 316
62. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.relationBits_length_le line 321
63. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.rowBits_length_le line 329
64. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.rowsBits_length_le line 338
65. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.tableBits_length_le line 348
66. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 357
67. theorem OAI.UniqueGames.Foundations.PCP.GraphTables.darts_le_tableBits_length line 363