OAI/Computability/PerfectCompleteness/Machines/PreprocessingMachineLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.PreprocessingMachine.preprocessing line 17
  2. theorem OAI.PerfectCompleteness.PreprocessingMachine.preprocessing_finite_alphabet line 20
  3. def OAI.PerfectCompleteness.PreprocessingMachine.round line 24
  4. theorem OAI.PerfectCompleteness.PreprocessingMachine.round_finite_alphabet line 29
  5. def OAI.PerfectCompleteness.PreprocessingMachine.computableInPolyTime line 33
  6. theorem OAI.PerfectCompleteness.PreprocessingMachine.finite_alphabet line 37
  7. def OAI.PerfectCompleteness.PCPSourceMachine.normalizedComputation line 51
  8. theorem OAI.PerfectCompleteness.PCPSourceMachine.normalized_finiteAlphabet line 58
  9. def OAI.PerfectCompleteness.PCPSourceMachine.rawSource line 64
  10. def OAI.PerfectCompleteness.PCPSourceMachine.rawComputation line 67
  11. theorem OAI.PerfectCompleteness.PCPSourceMachine.raw_finiteAlphabet line 72
  12. theorem OAI.PerfectCompleteness.PCPSourceMachine.rawSource_nonempty line 76
  13. theorem OAI.PerfectCompleteness.PCPSourceMachine.rawSource_satisfiable_iff line 79
  14. theorem OAI.PerfectCompleteness.PCPSourceMachine.rawSource_distinct line 84
  15. theorem OAI.PerfectCompleteness.PCPSourceMachine.rawSource_clauseGap line 89
  16. theorem OAI.PerfectCompleteness.PCPSourceMachine.amplifiedSource_complete line 95
  17. theorem OAI.PerfectCompleteness.PCPSourceMachine.amplifiedSource_sound line 101