OAI/Computability/VertexCover/PCP/PoweringPortReindex.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.wordEquiv line 17
  2. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.walkEquiv line 23
  3. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.addressEquiv line 26
  4. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.labelEquiv line 32
  5. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.wordEnd_map line 44
  6. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.endpoint_map line 52
  7. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.reach_iff line 56
  8. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.ballEquiv line 67
  9. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.wordToBall_map line 73
  10. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.pullSelector line 79
  11. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 87
  12. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.decode_transport line 93
  13. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 103
  14. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.advanceTail_map line 116
  15. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.edgeAt_map line 124
  16. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.pullAccepts line 139
  17. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 142
  18. def OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.dartEquiv line 168
  19. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 171
  20. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 184
  21. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 205
  22. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.pullReverse line 222
  23. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 228
  24. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 238
  25. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 266
  26. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 305
  27. theorem OAI.UniqueGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 344