OAI/Combinatorics/IndependentSets/Reduction/MapEquiv.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.ExplicitEnum.mapEquiv line 13
  2. def OAI.LargeIndependentSets.ExplicitEnum.bool line 18
  3. def OAI.LargeIndependentSets.ExplicitEnum.clauseAnswer line 20
  4. def OAI.LargeIndependentSets.ExplicitEnum.slot line 22
  5. def OAI.LargeIndependentSets.ExplicitEnum.leftAnswer line 24
  6. def OAI.LargeIndependentSets.ExplicitEnum.rightAnswer line 25
  7. def OAI.LargeIndependentSets.ExplicitEnum.clauses line 26
  8. def OAI.LargeIndependentSets.ExplicitEnum.variablesEnum line 28
  9. def OAI.LargeIndependentSets.ExplicitEnum.events line 30
  10. def OAI.LargeIndependentSets.NamedReduction.staticCopies line 38
  11. instance OAI.LargeIndependentSets.NamedReduction.cubeDecidableEq line 46
  12. def OAI.LargeIndependentSets.NamedReduction.vertexDecidable line 52
  13. def OAI.LargeIndependentSets.NamedReduction.formula line 71
  14. def OAI.LargeIndependentSets.NamedReduction.formula_renaming line 81
  15. lemma OAI.LargeIndependentSets.NamedReduction.bits_length_of_vertices line 93
  16. def OAI.LargeIndependentSets.NamedReduction.total line 109
  17. theorem OAI.LargeIndependentSets.NamedReduction.total_named_semantic_reduction line 113