OAI/Combinatorics/IndependentSets/Expansion/PreprocessingOverlayTables.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts line 13
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inl_val line 15
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inr_val line 18
4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts line 21
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_false_val line 24
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_true_val line 28
7. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.materialize line 32
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize line 46
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize_image line 57
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.accepts_materialize line 64
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.constraintGraph_ext line 71
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.baseGraph_materialize line 85
13. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlay line 101
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_old line 106
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_expander line 113
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_old line 120
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_expander line 127
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.overlay_semantics line 133
19. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazy line 141
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_false line 144
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_true line 150
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_false line 157
23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_true line 163
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayTables.lazy_semantics line 170