OAI/Computability/VertexCover/Reduction/DenseEncodingBound.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.BinaryFormula.activeNames line 43
  2. theorem OAI.UniqueGames.BinaryFormula.literal_mem_active line 46
  3. def OAI.UniqueGames.BinaryFormula.compactIndex line 54
  4. def OAI.UniqueGames.BinaryFormula.decodeName line 58
  5. def OAI.UniqueGames.BinaryFormula.compactLiteral line 61
  6. def OAI.UniqueGames.BinaryFormula.compactClause line 65
  7. def OAI.UniqueGames.BinaryFormula.compactClauses line 71
  8. def OAI.UniqueGames.BinaryFormula.dense line 74
  9. def OAI.UniqueGames.BinaryFormula.restrictAssignment line 78
  10. def OAI.UniqueGames.BinaryFormula.extendAssignment line 81
  11. theorem OAI.UniqueGames.BinaryFormula.decode_compactIndex line 85
  12. theorem OAI.UniqueGames.BinaryFormula.compactIndex_injective line 89
  13. theorem OAI.UniqueGames.BinaryFormula.compactLiteral_positive line 95
  14. theorem OAI.UniqueGames.BinaryFormula.eval_compact_restrict line 98
  15. theorem OAI.UniqueGames.BinaryFormula.eval_compact_extend line 104
  16. def OAI.UniqueGames.BinaryFormula.evaluationList line 113
  17. theorem OAI.UniqueGames.BinaryFormula.evaluationList_restrict line 116
  18. theorem OAI.UniqueGames.BinaryFormula.evaluationList_extend line 124
  19. def OAI.UniqueGames.BinaryFormula.failedCount line 138
  20. theorem OAI.UniqueGames.BinaryFormula.failedCount_restrict line 141
  21. theorem OAI.UniqueGames.BinaryFormula.failedCount_extend line 145
  22. theorem OAI.UniqueGames.BinaryFormula.clauseNames_flat_length line 149
  23. theorem OAI.UniqueGames.BinaryFormula.dense_clause_count line 158
  24. theorem OAI.UniqueGames.BinaryFormula.dense_variable_bound line 162
  25. theorem OAI.UniqueGames.BinaryFormula.dense_completeness line 167
  26. theorem OAI.UniqueGames.BinaryFormula.dense_reflects line 176
  27. theorem OAI.UniqueGames.BinaryFormula.dense_satisfiable_iff line 186
  28. theorem OAI.UniqueGames.BinaryFormula.dense_preserves_gap line 190
  29. theorem OAI.UniqueGames.BinaryFormula.dense_encoding_bound line 197