OAI/Computability/VertexCover/PCP/GenericGraphTables.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.GenericGraphTables.Label line 12
2. abbrev OAI.UniqueGames.Foundations.PCP.GenericGraphTables.RelationTable line 13
3. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationIndex line 17
4. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationIndex_val line 19
5. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationAt line 22
6. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationOf line 25
7. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationAt_relationOf line 28
8. structure OAI.UniqueGames.Foundations.PCP.GenericGraphTables.DartRow line 32
9. abbrev OAI.UniqueGames.Foundations.PCP.GenericGraphTables.Rows line 37
10. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.reverseAt line 39
11. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.acceptsAt line 42
12. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.Valid line 45
13. instance OAI.UniqueGames.Foundations.PCP.GenericGraphTables.(instance at line 49) line 49
14. structure OAI.UniqueGames.Foundations.PCP.GenericGraphTables.Table line 53
15. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowList line 59
16. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowList_length line 61
17. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics line 64
18. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_reverse line 75
19. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_tail line 78
20. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_accepts line 81
21. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.graphRows line 84
22. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.reverseAt_graphRows line 87
23. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.acceptsAt_graphRows line 92
24. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.graphRows_valid line 97
25. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.ofGraph line 105
26. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_reverse line 108
27. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_tail line 113
28. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_accepts line 119
29. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_edgeSatisfied line 124
30. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.constraintGraph_ext line 129
31. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph line 143
32. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_rejectionCount line 152
33. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.enumeratedGraph line 158
34. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_edgeSatisfied line 174
35. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_rejectionCount line 182
36. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.ofEnumeratedGraph line 194
37. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.bitWord line 198
38. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseBit line 200
39. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseBit_bitWord line 205
40. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseBits_bitWords line 208
41. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationWords line 214
42. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationWords_length line 216
43. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseRelation line 219
44. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseRelation_encoded line 225
45. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowWords line 232
46. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseRow line 235
47. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseRow_encoded line 243
48. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseRows line 251
49. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.parseRows_encoded line 259
50. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.tableWords line 265
51. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.tableBits line 268
52. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.decodeTableWords line 270
53. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.decodeTableWords_encoded line 281
54. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.decodeTableBits line 289
55. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.decodeTableBits_encoded line 292
56. def OAI.UniqueGames.Foundations.PCP.GenericGraphTables.encoding line 296
57. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.tableBits_injective line 301
58. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowWords_length line 303
59. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowsWords_length line 309
60. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.tableWords_length line 315
61. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.tableWords_length_le_bits line 320
62. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.relationBits_length_le line 325
63. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowBits_length_le line 333
64. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.rowsBits_length_le line 342
65. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.tableBits_length_le line 352
66. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.vertices_le_tableBits_length line 361
67. theorem OAI.UniqueGames.Foundations.PCP.GenericGraphTables.darts_le_tableBits_length line 367