OAI/Combinatorics/IndependentSets/PCP/NameCompaction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.clauseNames line 10
  2. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.sourceNames line 13
  3. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.activeNames line 16
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.literal_mem_active line 19
  5. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compactIndex line 28
  6. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.decodeName line 32
  7. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compactLiteral line 35
  8. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compactClause line 39
  9. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compactClauses line 45
  10. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact line 48
  11. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.restrictAssignment line 52
  12. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.extendAssignment line 55
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.decode_compactIndex line 59
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.eval_compact_restrict line 63
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.eval_compact_extend line 69
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.map_attach_val line 79
  17. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.evaluationList line 83
  18. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.satisfiedCount line 86
  19. def OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.failedCount line 89
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.evaluationList_restrict line 92
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.evaluationList_extend line 98
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 109
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.failedCount_restrict line 113
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.satisfiedCount_extend line 117
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.failedCount_extend line 121
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.clauseNames_flat_length line 125
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_clause_count line 134
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.length_eraseDups_le line 138
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_active_bound line 152
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_completeness line 157
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_reflects line 166
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 177
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_preserves_gap line 181
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_encoding_bound line 188
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.failureCount_evaluations line 206
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.evaluations_allIndices line 216
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.verifier_failureCount line 224
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.NameCompaction.compact_verifier_soundness line 229