OAI/Computability/VertexCover/PCP/PreprocessingPaddingTables.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 14
2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 17
3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 20
4. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 23
5. def OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 27
6. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 31
7. def OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 35
8. def OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 40
9. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 57
10. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 65
11. def OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.pad line 72
12. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 78
13. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 82
14. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 87
15. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext line 93
16. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 107
17. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 115
18. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 123
19. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 130
20. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 137
21. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 143
22. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 149
23. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 155
24. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.relation_ext line 161
25. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 170
26. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 178
27. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 188
28. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 200
29. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 207
30. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 215
31. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 221
32. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 239
33. def OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 254
34. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 257
35. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 261