OAI/Computability/VertexCover/PCP/DegreeReplacement.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.DegreeReplacement.Cloud line 16
  2. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 18
  3. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.cloudRotation line 28
  4. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 33
  5. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.innerRotation line 40
  6. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 44
  7. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.innerRotation_tail line 52
  8. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacementStep line 58
  9. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 65
  10. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacementPortGraph line 77
  11. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacementGraph line 86
  12. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.liftLabel line 102
  13. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 105
  14. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 115
  15. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacement_complete line 121
  16. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 131
  17. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 137
  18. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 145
  19. abbrev OAI.UniqueGames.Foundations.PCP.DegreeReplacement.PaddedDart line 158
  20. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedOwner line 161
  21. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedReverse line 166
  22. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 170
  23. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedGraph line 179
  24. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 193
  25. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 198
  26. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.padded_complete line 202
  27. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.padded_satisfiable line 210
  28. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.card_paddedDart line 215
  29. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 221
  30. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 233
  31. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 238
  32. theorem OAI.UniqueGames.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 244
  33. def OAI.UniqueGames.Foundations.PCP.DegreeReplacement.noDummyEquiv line 253