OAI/Computability/VertexCover/Encoding/BinaryEncoding.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.BinaryEncoding.bitsValue line 12

    Also declared: ComparatorChallenges/VertexCover.lean:32 (same declaration text).

  2. theorem OAI.UniqueGames.BinaryEncoding.bitsValue_bits line 16
  3. def OAI.UniqueGames.BinaryEncoding.frame line 23

    Also declared: ComparatorChallenges/VertexCover.lean:36 (same declaration text).

  4. def OAI.UniqueGames.BinaryEncoding.parseFrame line 27

    Also declared: ComparatorChallenges/VertexCover.lean:40 (same declaration text).

  5. theorem OAI.UniqueGames.BinaryEncoding.parseFrame_encoded line 34
  6. theorem OAI.UniqueGames.BinaryEncoding.frame_length line 40
  7. def OAI.UniqueGames.BinaryEncoding.nameBits line 46

    Also declared: ComparatorChallenges/VertexCover.lean:47 (same declaration text).

  8. def OAI.UniqueGames.BinaryEncoding.parseName line 48

    Also declared: ComparatorChallenges/VertexCover.lean:49 (same declaration text).

  9. theorem OAI.UniqueGames.BinaryEncoding.parseName_encoded line 53
  10. theorem OAI.UniqueGames.BinaryEncoding.nameBits_length line 57
  11. theorem OAI.UniqueGames.BinaryEncoding.nameBits_length_le_of_lt_pow line 61
  12. def OAI.UniqueGames.BinaryEncoding.literalBits line 67
  13. def OAI.UniqueGames.BinaryEncoding.parseLiteral line 70

    Also declared: ComparatorChallenges/VertexCover.lean:54 (same declaration text).

  14. theorem OAI.UniqueGames.BinaryEncoding.parseLiteral_encoded line 76
  15. theorem OAI.UniqueGames.BinaryEncoding.literalBits_length line 81
  16. def OAI.UniqueGames.BinaryEncoding.clauseBits line 85
  17. def OAI.UniqueGames.BinaryEncoding.parseClause line 88

    Also declared: ComparatorChallenges/VertexCover.lean:60 (same declaration text).

  18. theorem OAI.UniqueGames.BinaryEncoding.clause_three_entries line 94
  19. theorem OAI.UniqueGames.BinaryEncoding.parseClause_encoded line 100
  20. def OAI.UniqueGames.BinaryEncoding.clauseNameSize line 104
  21. theorem OAI.UniqueGames.BinaryEncoding.clauseBits_length line 107
  22. def OAI.UniqueGames.BinaryEncoding.clausesBits line 112
  23. def OAI.UniqueGames.BinaryEncoding.formulaBits line 116
  24. def OAI.UniqueGames.BinaryEncoding.namesBitSize line 118
  25. theorem OAI.UniqueGames.BinaryEncoding.namesBitSize_nil line 121
  26. theorem OAI.UniqueGames.BinaryEncoding.namesBitSize_cons line 123
  27. theorem OAI.UniqueGames.BinaryEncoding.clausesBits_length line 127
  28. theorem OAI.UniqueGames.BinaryEncoding.formulaBits_length line 136
  29. theorem OAI.UniqueGames.BinaryEncoding.clauses_length_lt_bits line 141
  30. def OAI.UniqueGames.BinaryEncoding.ordinarySize line 146
  31. theorem OAI.UniqueGames.BinaryEncoding.ordinarySize_le_bits line 149
  32. theorem OAI.UniqueGames.BinaryEncoding.bits_le_three_ordinarySize line 155
  33. def OAI.UniqueGames.BinaryEncoding.parseClauses line 161

    Also declared: ComparatorChallenges/VertexCover.lean:66 (same declaration text).

  34. theorem OAI.UniqueGames.BinaryEncoding.parseClauses_encoded line 170
  35. def OAI.UniqueGames.BinaryEncoding.decodeFormula line 185

    Also declared: ComparatorChallenges/VertexCover.lean:75 (same declaration text).

  36. theorem OAI.UniqueGames.BinaryEncoding.decodeFormula_encoded line 189
  37. theorem OAI.UniqueGames.BinaryEncoding.formulaBits_injective line 198