OAI/Computability/MinUncut/PCP/InitialGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.InitialGraph.Label line 12
  2. abbrev OAI.MinUncutGames.Foundations.PCP.InitialGraph.Vertex line 13
  3. abbrev OAI.MinUncutGames.Foundations.PCP.InitialGraph.Dart line 14
  4. instance OAI.MinUncutGames.Foundations.PCP.InitialGraph.slotFintype line 16
  5. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.card_slot line 20
  6. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.card_label line 21
  7. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.variableVertex line 24
  8. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.clauseVertex line 25
  9. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.dummyVertex line 26
  10. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.dummyDart line 27
  11. instance OAI.MinUncutGames.Foundations.PCP.InitialGraph.vertexNonempty line 29
  12. instance OAI.MinUncutGames.Foundations.PCP.InitialGraph.dartNonempty line 30
  13. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.reverse line 32
  14. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.reverse_involutive line 36
  15. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.reverseEquiv line 42
  16. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.tail line 48
  17. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.toClauseAnswer line 53
  18. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.fromClauseAnswer line 54
  19. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.variableLabel line 55
  20. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 57
  21. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.variableValid line 61
  22. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.incidenceAccept line 64
  23. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.predicate line 70
  24. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.raw line 75
  25. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.raw_forward line 86
  26. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.incidenceAccept_true line 91
  27. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.honestLabeling line 98
  28. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.incidence_honest line 103
  29. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.raw_completeness line 111
  30. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 120
  31. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.raw_reflects line 129
  32. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 148
  33. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.card_vertex line 151
  34. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.card_dart line 155
  35. abbrev OAI.MinUncutGames.Foundations.PCP.InitialGraph.CompactVertex line 160
  36. abbrev OAI.MinUncutGames.Foundations.PCP.InitialGraph.CompactDart line 161
  37. def OAI.MinUncutGames.Foundations.PCP.InitialGraph.build line 163
  38. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.build_satisfiable_iff line 166
  39. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.build_vertex_bound line 170
  40. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.build_dart_count line 176
  41. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.build_initial_gap line 180
  42. theorem OAI.MinUncutGames.Foundations.PCP.InitialGraph.build_inverse_size_gap line 186