OAI/Computability/VertexCover/PCP/NameCompaction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.NameCompaction.clauseNames line 13
  2. def OAI.UniqueGames.Foundations.PCP.NameCompaction.sourceNames line 16
  3. def OAI.UniqueGames.Foundations.PCP.NameCompaction.activeNames line 19
  4. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.literal_mem_active line 22
  5. def OAI.UniqueGames.Foundations.PCP.NameCompaction.compactIndex line 31
  6. def OAI.UniqueGames.Foundations.PCP.NameCompaction.decodeName line 35
  7. def OAI.UniqueGames.Foundations.PCP.NameCompaction.compactLiteral line 38
  8. def OAI.UniqueGames.Foundations.PCP.NameCompaction.compactClause line 42
  9. def OAI.UniqueGames.Foundations.PCP.NameCompaction.compactClauses line 48
  10. def OAI.UniqueGames.Foundations.PCP.NameCompaction.compact line 51
  11. def OAI.UniqueGames.Foundations.PCP.NameCompaction.restrictAssignment line 55
  12. def OAI.UniqueGames.Foundations.PCP.NameCompaction.extendAssignment line 58
  13. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.decode_compactIndex line 62
  14. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.eval_compact_restrict line 66
  15. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.eval_compact_extend line 72
  16. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.map_attach_val line 82
  17. def OAI.UniqueGames.Foundations.PCP.NameCompaction.evaluationList line 86
  18. def OAI.UniqueGames.Foundations.PCP.NameCompaction.satisfiedCount line 89
  19. def OAI.UniqueGames.Foundations.PCP.NameCompaction.failedCount line 92
  20. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.evaluationList_restrict line 95
  21. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.evaluationList_extend line 101
  22. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 112
  23. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.failedCount_restrict line 116
  24. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.satisfiedCount_extend line 120
  25. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.failedCount_extend line 124
  26. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.clauseNames_flat_length line 128
  27. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_clause_count line 137
  28. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.length_eraseDups_le line 141
  29. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_active_bound line 155
  30. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_completeness line 160
  31. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_reflects line 169
  32. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 180
  33. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_preserves_gap line 184
  34. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_encoding_bound line 191
  35. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.failureCount_evaluations line 209
  36. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.evaluations_allIndices line 219
  37. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.verifier_failureCount line 227
  38. theorem OAI.UniqueGames.Foundations.PCP.NameCompaction.compact_verifier_soundness line 232