OAI/Computability/MinUncut/PCP/Hastad.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Outer.HastadSource.success line 18
  2. def OAI.MinUncutGames.Outer.HastadSource.asSource line 22
  3. theorem OAI.MinUncutGames.Outer.HastadSource.failure_add_success line 25
  4. def OAI.MinUncutGames.Outer.HastadSource.gapInput line 33
  5. def OAI.MinUncutGames.Outer.HastadSource.sourceMap line 37
  6. def OAI.MinUncutGames.Outer.HastadSource.output line 41
  7. theorem OAI.MinUncutGames.Outer.HastadSource.complete line 45
  8. theorem OAI.MinUncutGames.Outer.HastadSource.sound line 52
  9. def OAI.MinUncutGames.Outer.HastadSource.roundMachine line 61
  10. theorem OAI.MinUncutGames.Outer.HastadSource.roundMachine_finite line 64
  11. def OAI.MinUncutGames.Outer.HastadSource.gapMachine line 69
  12. def OAI.MinUncutGames.Outer.HastadSource.sourceMachine line 77
  13. def OAI.MinUncutGames.Outer.HastadSource.computation line 83
  14. theorem OAI.MinUncutGames.Outer.HastadSource.finiteAlphabet line 88
  15. structure OAI.MinUncutGames.Outer.HastadSource.Reduction line 95
  16. theorem OAI.MinUncutGames.Outer.HastadSource.exists_reduction line 102