OAI/Computability/VertexCover/PCP/AlphabetTableTable.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rowFromDart line 14
2. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rows line 32
3. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rows_at line 38
4. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 44
5. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.dartRow_ext line 52
6. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.relation_ext line 62
7. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 73
8. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 113
9. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rows_valid line 124
10. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.build line 128
11. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.build_vertices line 134
12. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.build_darts line 137
13. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.table_rows_congr line 140
14. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr line 146
15. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 153
16. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.semantics_build line 161
17. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.decode_build line 169
18. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 177
19. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 190
20. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 201
21. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.gap_transfer line 215
22. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 239
23. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 248
24. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.rowList_length line 257
25. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.tableWords_length line 261
26. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 266