OAI/Computability/BinPacking/PCP/BinaryOccurrenceRename.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.literal_mem_names line 9
  2. def OAI.BinPackingCompleteness.BinaryOccurrenceRename.nameIndex line 16
  3. def OAI.BinPackingCompleteness.BinaryOccurrenceRename.literal line 20
  4. def OAI.BinPackingCompleteness.BinaryOccurrenceRename.clause line 24
  5. def OAI.BinPackingCompleteness.BinaryOccurrenceRename.renamed line 30
  6. def OAI.BinPackingCompleteness.BinaryOccurrenceRename.restrictAssignment line 34
  7. def OAI.BinPackingCompleteness.BinaryOccurrenceRename.extendAssignment line 38
  8. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.nameIndex_reads_name line 41
  9. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.clause_eval_restrict line 45
  10. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.clause_eval_extend line 50
  11. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.renamed_clause_count line 60
  12. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.renamed_variable_count line 63
  13. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.renamed_satisfiable_iff line 67
  14. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.nat_bits_injective line 82
  15. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.idxOf_binary_payloads line 87
  16. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.renamed_encoding_bound line 99
  17. theorem OAI.BinPackingCompleteness.BinaryOccurrenceRename.renamed_encoding_bound_bits line 106