OAI/Combinatorics/IndependentSets/Main.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.CompleteReduction.gapInput line 24
  2. def OAI.LargeIndependentSets.CompleteReduction.gapView line 27
  3. def OAI.LargeIndependentSets.CompleteReduction.lcComputer line 36
  4. lemma OAI.LargeIndependentSets.CompleteReduction.lcComputer_finiteAlphabet line 41
  5. def OAI.LargeIndependentSets.CompleteReduction.reduce line 46
  6. def OAI.LargeIndependentSets.CompleteReduction.certificate line 49
  7. lemma OAI.LargeIndependentSets.CompleteReduction.finiteAlphabet line 55
  8. lemma OAI.LargeIndependentSets.CompleteReduction.normalize_bits line 60
  9. def OAI.LargeIndependentSets.CompleteReduction.clausePolynomial line 68
  10. lemma OAI.LargeIndependentSets.CompleteReduction.clauses_bound line 71
  11. def OAI.LargeIndependentSets.CompleteReduction.vertexPolynomial line 80
  12. lemma OAI.LargeIndependentSets.CompleteReduction.vertices_bound line 84
  13. def OAI.LargeIndependentSets.CompleteReduction.outputPolynomial line 103
  14. lemma OAI.LargeIndependentSets.CompleteReduction.output_bound line 106
  15. lemma OAI.LargeIndependentSets.CompleteReduction.complete line 114
  16. theorem OAI.LargeIndependentSets.mainTheoremReal line 124

    Distinct definitions of this name: ComparatorChallenges/IndependentSets.lean:77 (same statement text; different proof or body). Qualify references as OAI.LargeIndependentSets.mainTheoremReal@path.