OAI/Computability/PerfectCompleteness/Construction/CanonicalLocalCompletion.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalLocalCompletion.alphabet line 19
  2. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.alphabet_positive line 21
  3. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.partitionWidth_le_alphabet line 24
  4. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.partitionWidth_le_leftAlphabet line 27
  5. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.alphabet_ge_two line 32
  6. def OAI.PerfectCompleteness.CanonicalLocalCompletion.legalL line 52
  7. def OAI.PerfectCompleteness.CanonicalLocalCompletion.legalR line 55
  8. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.legalL_val line 59
  9. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.legalR_val line 63
  10. def OAI.PerfectCompleteness.CanonicalLocalCompletion.defaultL line 66
  11. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.leftLabel_card_le line 74
  12. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.rightLabel_card_le line 82
  13. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.small line 89
  14. def OAI.PerfectCompleteness.CanonicalLocalCompletion.input line 97
  15. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.input_mask line 104
  16. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.input_image_legal line 115
  17. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.input_independent_of_law line 125
  18. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.input_admissible line 130
  19. def OAI.PerfectCompleteness.CanonicalLocalCompletion.result line 140
  20. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.result_correct line 146
  21. def OAI.PerfectCompleteness.CanonicalLocalCompletion.family line 150
  22. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.family_size line 162
  23. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.family_map line 167
  24. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.family_size_le line 172
  25. def OAI.PerfectCompleteness.CanonicalLocalCompletion.machine_output line 176
  26. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.payload_parses line 185
  27. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.parsed_projection_eq_family_map line 195
  28. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.payload_length_le line 204
  29. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.family_value_le line 209
  30. theorem OAI.PerfectCompleteness.CanonicalLocalCompletion.family_value_of_satisfying line 222