OAI/Computability/VertexCover/PCP/PreprocessingOverlayTables.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

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