OAI/Computability/PerfectCompleteness/Machines/BinaryParsingLemmas.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.BinaryParsing.frame_eq line 13
  2. theorem OAI.PerfectCompleteness.BinaryParsing.canonical_cons_cons line 18
  3. theorem OAI.PerfectCompleteness.BinaryParsing.canonical_iff line 21
  4. theorem OAI.PerfectCompleteness.BinaryParsing.canonical_nat_bits line 46
  5. theorem OAI.PerfectCompleteness.BinaryParsing.parseFrame_sound line 51
  6. theorem OAI.PerfectCompleteness.BinaryParsing.parseName_sound line 75
  7. theorem OAI.PerfectCompleteness.BinaryParsing.parseLiteral_sound line 91
  8. theorem OAI.PerfectCompleteness.BinaryParsing.parseClause_sound line 106
  9. theorem OAI.PerfectCompleteness.BinaryParsing.parseClauses_sound line 130
  10. theorem OAI.PerfectCompleteness.BinaryParsing.decodeFormula_sound line 158
  11. theorem OAI.PerfectCompleteness.BinaryParsing.decodeFormula_eq_some_iff line 172
  12. theorem OAI.PerfectCompleteness.BinaryParsing.scanSpec_nameBits line 176
  13. def OAI.PerfectCompleteness.BinaryLanguage.rejectBinary line 194
  14. theorem OAI.PerfectCompleteness.BinaryLanguage.rejectBinary_unsatisfiable line 198
  15. def OAI.PerfectCompleteness.BinaryLanguage.rejectFormula line 207
  16. theorem OAI.PerfectCompleteness.BinaryLanguage.reject_unsatisfiable line 209
  17. def OAI.PerfectCompleteness.BinaryLanguage.totalParsed line 213
  18. def OAI.PerfectCompleteness.BinaryLanguage.totalRename line 216
  19. theorem OAI.PerfectCompleteness.BinaryLanguage.totalParsed_satisfiable_iff line 219
  20. theorem OAI.PerfectCompleteness.BinaryLanguage.totalRename_satisfiable_iff line 225
  21. theorem OAI.PerfectCompleteness.BinaryLanguage.totalRename_encoded line 230
  22. theorem OAI.PerfectCompleteness.BinaryLanguage.language_encoded line 234
  23. theorem OAI.PerfectCompleteness.BinaryLanguage.reject_bits_length line 238
  24. theorem OAI.PerfectCompleteness.BinaryLanguage.totalRename_output_length line 240