OAI/Computability/PerfectCompleteness/Machines/BinaryOccurrenceRename.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.literal_mem_names line 11
  2. def OAI.PerfectCompleteness.BinaryOccurrenceRename.nameIndex line 18
  3. def OAI.PerfectCompleteness.BinaryOccurrenceRename.literal line 22
  4. def OAI.PerfectCompleteness.BinaryOccurrenceRename.clause line 26
  5. def OAI.PerfectCompleteness.BinaryOccurrenceRename.renamed line 32
  6. def OAI.PerfectCompleteness.BinaryOccurrenceRename.restrictAssignment line 36
  7. def OAI.PerfectCompleteness.BinaryOccurrenceRename.extendAssignment line 40
  8. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.nameIndex_reads_name line 43
  9. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.clause_eval_restrict line 47
  10. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.clause_eval_extend line 52
  11. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.renamed_clause_count line 62
  12. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.renamed_variable_count line 65
  13. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.renamed_satisfiable_iff line 69
  14. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.nat_bits_injective line 84
  15. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.idxOf_binary_payloads line 89
  16. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.renamed_encoding_bound line 101
  17. theorem OAI.PerfectCompleteness.BinaryOccurrenceRename.renamed_encoding_bound_bits line 108