OAI/Computability/VertexCover/Reduction/CloneGap.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Reduction.CloneGap.cart line 41
  2. theorem OAI.UniqueGames.Reduction.CloneGap.count_const line 44
  3. theorem OAI.UniqueGames.Reduction.CloneGap.count_cart line 48
  4. theorem OAI.UniqueGames.Reduction.CloneGap.length_cart line 59
  5. theorem OAI.UniqueGames.Reduction.CloneGap.count_cart_left line 64
  6. theorem OAI.UniqueGames.Reduction.CloneGap.count_cart_right line 68
  7. theorem OAI.UniqueGames.Reduction.CloneGap.count_cart_le line 72
  8. theorem OAI.UniqueGames.Reduction.CloneGap.count_union_le line 85
  9. theorem OAI.UniqueGames.Reduction.CloneGap.count_remove line 93
  10. abbrev OAI.UniqueGames.Reduction.CloneGap.Index line 101
  11. def OAI.UniqueGames.Reduction.CloneGap.indices line 102
  12. def OAI.UniqueGames.Reduction.CloneGap.triples line 103
  13. def OAI.UniqueGames.Reduction.CloneGap.collision line 104
  14. def OAI.UniqueGames.Reduction.CloneGap.distinctTriples line 106
  15. theorem OAI.UniqueGames.Reduction.CloneGap.length_indices line 108
  16. theorem OAI.UniqueGames.Reduction.CloneGap.length_triples line 109
  17. theorem OAI.UniqueGames.Reduction.CloneGap.count_index_eq_le line 112
  18. theorem OAI.UniqueGames.Reduction.CloneGap.count_collision_le line 122
  19. theorem OAI.UniqueGames.Reduction.CloneGap.majority_exists line 151
  20. def OAI.UniqueGames.Reduction.CloneGap.allAgree line 165
  21. theorem OAI.UniqueGames.Reduction.CloneGap.count_agree_distinct line 168
  22. structure OAI.UniqueGames.Reduction.CloneGap.Equation line 185
  23. def OAI.UniqueGames.Reduction.CloneGap.satisfied line 191
  24. def OAI.UniqueGames.Reduction.CloneGap.clone line 194
  25. theorem OAI.UniqueGames.Reduction.CloneGap.lift_preserves line 197
  26. theorem OAI.UniqueGames.Reduction.CloneGap.clone_names_distinct line 200
  27. theorem OAI.UniqueGames.Reduction.CloneGap.agree_failure line 211
  28. theorem OAI.UniqueGames.Reduction.CloneGap.failed_occurrence_clones line 221
  29. def OAI.UniqueGames.Reduction.CloneGap.majorityBit line 237
  30. theorem OAI.UniqueGames.Reduction.CloneGap.majorityBit_count line 239
  31. def OAI.UniqueGames.Reduction.CloneGap.cloneList line 251
  32. theorem OAI.UniqueGames.Reduction.CloneGap.length_cloneList line 254
  33. theorem OAI.UniqueGames.Reduction.CloneGap.cloneList_failure_lower line 263
  34. theorem OAI.UniqueGames.Reduction.CloneGap.clone_gap line 282
  35. theorem OAI.UniqueGames.Reduction.CloneGap.clone_completeness_count line 301