OAI/Computability/UniqueGames/PCP/BinaryParityReduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.output line 17
  2. def OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.formulaMachine line 21
  3. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.formulaMachine_finite line 29
  4. def OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.computation line 37
  5. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.computation_finite line 44
  6. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.complete line 51
  7. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.sound line 63
  8. structure OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.Reduction line 75
  9. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.exists_reduction line 86
  10. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.failure_completeness line 94
  11. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.parity_soundness line 103
  12. theorem OAI.UniqueGamesTheorem.Outer.BinaryParityReduction.ordinaryGame_soundness line 117