OAI/Combinatorics/IndependentSets/Encoding/Target.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IndependentSetsGames.Foundations.Target.Literal line 7
  2. def OAI.IndependentSetsGames.Foundations.Target.Literal.eval line 12
  3. abbrev OAI.IndependentSetsGames.Foundations.Target.Clause line 15
  4. def OAI.IndependentSetsGames.Foundations.Target.Clause.eval line 17
  5. structure OAI.IndependentSetsGames.Foundations.Target.Formula line 20
  6. def OAI.IndependentSetsGames.Foundations.Target.Formula.Satisfiable line 24
  7. structure OAI.IndependentSetsGames.Foundations.Target.PermutationTable line 28
  8. theorem OAI.IndependentSetsGames.Foundations.Target.PermutationTable.images_injective line 34
  9. theorem OAI.IndependentSetsGames.Foundations.Target.PermutationTable.images_surjective line 39
  10. structure OAI.IndependentSetsGames.Foundations.Target.Constraint line 43
  11. def OAI.IndependentSetsGames.Foundations.Target.Constraint.satisfied line 48
  12. structure OAI.IndependentSetsGames.Foundations.Target.Instance line 52
  13. def OAI.IndependentSetsGames.Foundations.Target.countSatisfied line 57
  14. theorem OAI.IndependentSetsGames.Foundations.Target.countSatisfied_le_length line 63
  15. theorem OAI.IndependentSetsGames.Foundations.Target.Instance.constraintCount_positive line 72
  16. structure OAI.IndependentSetsGames.Foundations.Target.RationalError line 78
  17. def OAI.IndependentSetsGames.Foundations.Target.CompleteAt line 85
  18. def OAI.IndependentSetsGames.Foundations.Target.SoundAt line 91
  19. structure OAI.IndependentSetsGames.Foundations.Target.SemanticGapReduction line 96
  20. def OAI.IndependentSetsGames.Foundations.Complexity.encodeWord line 109
  21. def OAI.IndependentSetsGames.Foundations.Complexity.encodeWords line 111
  22. def OAI.IndependentSetsGames.Foundations.Complexity.decodeWordsAux line 115
  23. def OAI.IndependentSetsGames.Foundations.Complexity.decodeWords line 121
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.decodeWordsAux_word line 123
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.decodeWords_encodeWords line 133
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.encodeWords_injective line 141
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.encodeWord_length line 146
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.encodeWords_append line 149
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.encodeWords_length line 155
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.encodeWords_length_le line 161
  31. def OAI.IndependentSetsGames.Foundations.Complexity.literalWords line 175
  32. def OAI.IndependentSetsGames.Foundations.Complexity.clauseWords line 178
  33. def OAI.IndependentSetsGames.Foundations.Complexity.formulaWords line 181
  34. def OAI.IndependentSetsGames.Foundations.Complexity.formulaBits line 184
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.literalWords_length line 186
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.clauseWords_length line 189
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.clausesWords_length line 192
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.formulaWords_length line 201
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.literalBits_length_le line 206
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.clauseBits_length_le line 211
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.clausesBits_length_le line 219
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.formulaBits_length_le line 229