OAI/Computability/PerfectCompleteness/Reduction/FinitePreliminaryCompletion.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FinitePreliminaryCompletion.alphabet line 20
  2. def OAI.PerfectCompleteness.FinitePreliminaryCompletion.finiteInput line 23
  3. def OAI.PerfectCompleteness.FinitePreliminaryCompletion.finiteResult line 31
  4. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.finiteResult_correct line 37
  5. abbrev OAI.PerfectCompleteness.FinitePreliminaryCompletion.blockFamily line 48
  6. def OAI.PerfectCompleteness.FinitePreliminaryCompletion.rawInput line 57
  7. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.rawInput_mask line 61
  8. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.rawInput_image_legal line 69
  9. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.compatible line 121
  10. def OAI.PerfectCompleteness.FinitePreliminaryCompletion.family line 133
  11. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.family_size line 148
  12. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.family_map line 154
  13. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.family_size_le line 160
  14. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.family_value_le line 166
  15. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.family_value_of_satisfying line 183
  16. def OAI.PerfectCompleteness.FinitePreliminaryCompletion.actualFamily line 192
  17. def OAI.PerfectCompleteness.FinitePreliminaryCompletion.actualValue line 196
  18. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.actualValue_le line 200
  19. theorem OAI.PerfectCompleteness.FinitePreliminaryCompletion.actualValue_of_satisfying line 209