OAI/Combinatorics/IndependentSets/Expansion/PreprocessingPaddingTables.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 13
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 16
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 19
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 22
5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 26
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 30
7. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 34
8. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 39
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 56
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 64
11. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.pad line 71
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 77
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 81
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 86
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext line 92
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 106
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 114
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 122
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 129
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 136
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 142
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 148
23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 154
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.relation_ext line 160
25. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 169
26. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 177
27. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 187
28. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 200
29. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 207
30. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 215
31. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 221
32. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 239
33. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 254
34. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 257
35. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 261