OAI/Computability/MaxCut/Encoding/BinaryParityReduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaxCutGames.Outer.BinaryParityReduction.output line 14
  2. def OAI.MaxCutGames.Outer.BinaryParityReduction.formulaMachine line 18
  3. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.formulaMachine_finite line 26
  4. def OAI.MaxCutGames.Outer.BinaryParityReduction.computation line 34
  5. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.computation_finite line 41
  6. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.complete line 48
  7. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.sound line 60
  8. structure OAI.MaxCutGames.Outer.BinaryParityReduction.Reduction line 72
  9. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.exists_reduction line 83
  10. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.failure_completeness line 91
  11. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.parity_soundness line 100
  12. theorem OAI.MaxCutGames.Outer.BinaryParityReduction.ordinaryGame_soundness line 114