OAI/Computability/MaxCut/Encoding/FormulaEncoding.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

A checked parser for the concrete 3CNF serialization, including finite-index bounds, Boolean signs, clause count, and absence of trailing garbage.

  1. def OAI.MaxCutGames.Foundations.Complexity.parseLiteral line 13
  2. theorem OAI.MaxCutGames.Foundations.Complexity.parseLiteral_encoded line 22
  3. def OAI.MaxCutGames.Foundations.Complexity.parseClause line 28
  4. theorem OAI.MaxCutGames.Foundations.Complexity.clause_three_entries line 34
  5. theorem OAI.MaxCutGames.Foundations.Complexity.parseClause_encoded line 41
  6. def OAI.MaxCutGames.Foundations.Complexity.parseClauses line 46
  7. theorem OAI.MaxCutGames.Foundations.Complexity.parseClauses_encoded line 53
  8. def OAI.MaxCutGames.Foundations.Complexity.decodeFormulaWords line 60
  9. theorem OAI.MaxCutGames.Foundations.Complexity.decodeFormulaWords_encoded line 66
  10. def OAI.MaxCutGames.Foundations.Complexity.decodeFormulaBits line 74
  11. theorem OAI.MaxCutGames.Foundations.Complexity.decodeFormulaBits_encoded line 77
  12. theorem OAI.MaxCutGames.Foundations.Complexity.formulaBits_injective line 81
  13. def OAI.MaxCutGames.Foundations.Complexity.parseLabel line 90
  14. theorem OAI.MaxCutGames.Foundations.Complexity.parseLabel_value line 93
  15. theorem OAI.MaxCutGames.Foundations.Complexity.parseLabels_values line 96
  16. def OAI.MaxCutGames.Foundations.Complexity.parseImages line 102
  17. theorem OAI.MaxCutGames.Foundations.Complexity.parseImages_values line 108
  18. def OAI.MaxCutGames.Foundations.Complexity.findPreimage line 115
  19. theorem OAI.MaxCutGames.Foundations.Complexity.findPreimage_permutation line 118
  20. def OAI.MaxCutGames.Foundations.Complexity.searchedInverse line 137
  21. theorem OAI.MaxCutGames.Foundations.Complexity.searchedInverse_permutation line 140
  22. def OAI.MaxCutGames.Foundations.Complexity.tableWords line 146
  23. def OAI.MaxCutGames.Foundations.Complexity.parsePermutation line 149
  24. theorem OAI.MaxCutGames.Foundations.Complexity.parsePermutation_encoded line 158
  25. theorem OAI.MaxCutGames.Foundations.Complexity.tableWords_length line 165
  26. def OAI.MaxCutGames.Foundations.Complexity.constraintWords line 168
  27. def OAI.MaxCutGames.Foundations.Complexity.parseConstraint line 171
  28. theorem OAI.MaxCutGames.Foundations.Complexity.parseConstraint_encoded line 180
  29. def OAI.MaxCutGames.Foundations.Complexity.parseConstraints line 189
  30. theorem OAI.MaxCutGames.Foundations.Complexity.parseConstraints_encoded line 197
  31. def OAI.MaxCutGames.Foundations.Complexity.gameWords line 206
  32. def OAI.MaxCutGames.Foundations.Complexity.gameBits line 209
  33. def OAI.MaxCutGames.Foundations.Complexity.decodeGameWords line 211
  34. theorem OAI.MaxCutGames.Foundations.Complexity.decodeGameWords_encoded line 221
  35. def OAI.MaxCutGames.Foundations.Complexity.decodeGameBits line 229
  36. theorem OAI.MaxCutGames.Foundations.Complexity.decodeGameBits_encoded line 232
  37. theorem OAI.MaxCutGames.Foundations.Complexity.gameBits_injective line 236
  38. theorem OAI.MaxCutGames.Foundations.Complexity.constraintWords_length line 241
  39. theorem OAI.MaxCutGames.Foundations.Complexity.constraintsWords_length line 244
  40. theorem OAI.MaxCutGames.Foundations.Complexity.gameWords_length line 253