OAI/Computability/VertexCover/PCP/QueryIncidence.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.PCP.QueryIncidence.Verifier line 10
  2. abbrev OAI.UniqueGames.Foundations.PCP.QueryIncidence.Label line 14
  3. abbrev OAI.UniqueGames.Foundations.PCP.QueryIncidence.Vertex line 15
  4. abbrev OAI.UniqueGames.Foundations.PCP.QueryIncidence.Dart line 16
  5. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.response line 20
  6. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.zeroSlot line 23
  7. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.decodeRight line 25
  8. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.encodeRight line 27
  9. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.decode_encodeRight line 29
  10. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.canonicalSlot line 32
  11. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.canonicalSlot_query line 35
  12. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.RepeatedConsistent line 39
  13. instance OAI.UniqueGames.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 42
  14. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.LeftValid line 48
  15. instance OAI.UniqueGames.Foundations.PCP.QueryIncidence.leftValidDecidable line 51
  16. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.incidenceAccept line 57
  17. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.reverse line 62
  18. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.reverse_involutive line 64
  19. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.reverseEquiv line 68
  20. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.tail line 74
  21. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.predicate line 78
  22. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.graph line 83
  23. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 93
  24. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.honestLabeling line 101
  25. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.honest_leftValid line 105
  26. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.honest_incidence line 112
  27. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.perfect_completeness line 123
  28. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 131
  29. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.decodedAssignment line 139
  30. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.incidenceAccept_true line 142
  31. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 151
  32. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 166
  33. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.rejectedEvents line 184
  34. def OAI.UniqueGames.Foundations.PCP.QueryIncidence.verifierRejectionCount line 187
  35. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.rejection_count_bound line 190
  36. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.card_label line 219
  37. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.card_vertex line 222
  38. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.card_dart line 226
  39. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.gap_transfer line 230
  40. theorem OAI.UniqueGames.Foundations.PCP.QueryIncidence.six_query_alphabet line 245