OAI/Computability/MinUncut/Encoding/FormulaEncoding.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.parseLiteral line 12
  2. theorem OAI.MinUncutGames.Foundations.Complexity.parseLiteral_encoded line 21
  3. def OAI.MinUncutGames.Foundations.Complexity.parseClause line 27
  4. theorem OAI.MinUncutGames.Foundations.Complexity.clause_three_entries line 33
  5. theorem OAI.MinUncutGames.Foundations.Complexity.parseClause_encoded line 40
  6. def OAI.MinUncutGames.Foundations.Complexity.parseClauses line 45
  7. theorem OAI.MinUncutGames.Foundations.Complexity.parseClauses_encoded line 52
  8. def OAI.MinUncutGames.Foundations.Complexity.decodeFormulaWords line 59
  9. theorem OAI.MinUncutGames.Foundations.Complexity.decodeFormulaWords_encoded line 65
  10. def OAI.MinUncutGames.Foundations.Complexity.decodeFormulaBits line 73
  11. theorem OAI.MinUncutGames.Foundations.Complexity.decodeFormulaBits_encoded line 76
  12. theorem OAI.MinUncutGames.Foundations.Complexity.formulaBits_injective line 80
  13. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.clauseNames line 93
  14. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.sourceNames line 96
  15. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.activeNames line 99
  16. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.literal_mem_active line 102
  17. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.compactIndex line 111
  18. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.decodeName line 115
  19. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.compactLiteral line 118
  20. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.compactClause line 122
  21. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.compactClauses line 128
  22. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact line 131
  23. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.restrictAssignment line 135
  24. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.extendAssignment line 138
  25. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.decode_compactIndex line 142
  26. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.eval_compact_restrict line 146
  27. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.eval_compact_extend line 152
  28. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.map_attach_val line 162
  29. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.evaluationList line 166
  30. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.satisfiedCount line 169
  31. def OAI.MinUncutGames.Foundations.PCP.NameCompaction.failedCount line 172
  32. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.evaluationList_restrict line 175
  33. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.evaluationList_extend line 181
  34. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 192
  35. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.failedCount_restrict line 196
  36. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.satisfiedCount_extend line 200
  37. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.failedCount_extend line 204
  38. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.clauseNames_flat_length line 208
  39. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_clause_count line 217
  40. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.length_eraseDups_le line 221
  41. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_active_bound line 235
  42. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_completeness line 240
  43. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_reflects line 249
  44. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 260
  45. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_preserves_gap line 264
  46. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_encoding_bound line 271
  47. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.failureCount_evaluations line 289
  48. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.evaluations_allIndices line 299
  49. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.verifier_failureCount line 307
  50. theorem OAI.MinUncutGames.Foundations.PCP.NameCompaction.compact_verifier_soundness line 312