OAI/Combinatorics/TreeEdit/FiniteTree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.FiniteTree.State line 14
  2. instance OAI.TreeEdit.FiniteTree.stateAddCommGroup line 18
  3. def OAI.TreeEdit.FiniteTree.Symbol line 26
  4. def OAI.TreeEdit.FiniteTree.stateFintype line 30
  5. def OAI.TreeEdit.FiniteTree.symbolFintype line 41
  6. def OAI.TreeEdit.FiniteTree.w line 52
  7. def OAI.TreeEdit.FiniteTree.u line 56
  8. def OAI.TreeEdit.FiniteTree.word line 59
  9. lemma OAI.TreeEdit.FiniteTree.many_shifted_children line 65
  10. structure OAI.TreeEdit.FiniteTree.Admissible line 107
  11. lemma OAI.TreeEdit.FiniteTree.Admissible.child line 114
  12. lemma OAI.TreeEdit.FiniteTree.Admissible.many line 125
  13. theorem OAI.TreeEdit.FiniteTree.separation line 142