OAI/Combinatorics/IndependentSets/Encoding/BinarySyntax.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.LargeIndependentSets.BinarySyntax.Phase line 8
  2. def OAI.LargeIndependentSets.BinarySyntax.after line 19
  3. def OAI.LargeIndependentSets.BinarySyntax.width line 22
  4. def OAI.LargeIndependentSets.BinarySyntax.transition line 25
  5. def OAI.LargeIndependentSets.BinarySyntax.run line 44
  6. lemma OAI.LargeIndependentSets.BinarySyntax.run_nil line 46
  7. lemma OAI.LargeIndependentSets.BinarySyntax.run_cons line 47
  8. lemma OAI.LargeIndependentSets.BinarySyntax.run_append line 49
  9. lemma OAI.LargeIndependentSets.BinarySyntax.run_header line 52
  10. lemma OAI.LargeIndependentSets.BinarySyntax.run_name line 57
  11. lemma OAI.LargeIndependentSets.BinarySyntax.run_literal line 62
  12. lemma OAI.LargeIndependentSets.BinarySyntax.run_width line 66
  13. lemma OAI.LargeIndependentSets.BinarySyntax.run_clause line 69
  14. lemma OAI.LargeIndependentSets.BinarySyntax.run_clauses line 102
  15. lemma OAI.LargeIndependentSets.BinarySyntax.run_formula line 110
  16. def OAI.LargeIndependentSets.BinarySyntax.phaseEquiv line 115
  17. def OAI.LargeIndependentSets.BinarySyntax.finiteTransition line 116
  18. lemma OAI.LargeIndependentSets.BinarySyntax.finite_run line 119
  19. def OAI.LargeIndependentSets.BinarySyntax.annotated line 125
  20. lemma OAI.LargeIndependentSets.BinarySyntax.annotated_history line 128
  21. def OAI.LargeIndependentSets.BinarySyntax.certificate line 132
  22. lemma OAI.LargeIndependentSets.BinarySyntax.finiteAlphabet line 136