OAI/Combinatorics/IndependentSets/PCP/CloneGap.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Reduction.CloneGap.cart line 9
  2. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_const line 12
  3. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_cart line 16
  4. theorem OAI.IndependentSetsGames.Reduction.CloneGap.length_cart line 27
  5. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_cart_left line 32
  6. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_cart_right line 36
  7. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_cart_le line 40
  8. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_union_le line 53
  9. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_remove line 61
  10. abbrev OAI.IndependentSetsGames.Reduction.CloneGap.Index line 69
  11. def OAI.IndependentSetsGames.Reduction.CloneGap.indices line 70
  12. def OAI.IndependentSetsGames.Reduction.CloneGap.triples line 71
  13. def OAI.IndependentSetsGames.Reduction.CloneGap.collision line 72
  14. def OAI.IndependentSetsGames.Reduction.CloneGap.distinctTriples line 74
  15. theorem OAI.IndependentSetsGames.Reduction.CloneGap.length_indices line 76
  16. theorem OAI.IndependentSetsGames.Reduction.CloneGap.length_triples line 77
  17. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_index_eq_le line 80
  18. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_collision_le line 90
  19. theorem OAI.IndependentSetsGames.Reduction.CloneGap.majority_exists line 119
  20. def OAI.IndependentSetsGames.Reduction.CloneGap.allAgree line 133
  21. theorem OAI.IndependentSetsGames.Reduction.CloneGap.count_agree_distinct line 136
  22. structure OAI.IndependentSetsGames.Reduction.CloneGap.Equation line 153
  23. def OAI.IndependentSetsGames.Reduction.CloneGap.satisfied line 161
  24. def OAI.IndependentSetsGames.Reduction.CloneGap.clone line 164
  25. theorem OAI.IndependentSetsGames.Reduction.CloneGap.lift_preserves line 167
  26. theorem OAI.IndependentSetsGames.Reduction.CloneGap.clone_names_distinct line 170
  27. theorem OAI.IndependentSetsGames.Reduction.CloneGap.agree_failure line 181
  28. theorem OAI.IndependentSetsGames.Reduction.CloneGap.failed_occurrence_clones line 191
  29. def OAI.IndependentSetsGames.Reduction.CloneGap.majorityBit line 207
  30. theorem OAI.IndependentSetsGames.Reduction.CloneGap.majorityBit_count line 209
  31. def OAI.IndependentSetsGames.Reduction.CloneGap.cloneList line 221
  32. theorem OAI.IndependentSetsGames.Reduction.CloneGap.length_cloneList line 224
  33. theorem OAI.IndependentSetsGames.Reduction.CloneGap.cloneList_failure_lower line 233
  34. theorem OAI.IndependentSetsGames.Reduction.CloneGap.clone_gap line 252
  35. theorem OAI.IndependentSetsGames.Reduction.CloneGap.clone_completeness_count line 271