OAI/Computability/MinUncut/Machines/OuterAlphabets.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Outer.Triple line 11
  2. structure OAI.MinUncut.Outer.Equation line 13
  3. def OAI.MinUncut.Outer.parity line 20
  4. lemma OAI.MinUncut.Outer.parity_apply line 25
  5. def OAI.MinUncut.Outer.Valid line 27
  6. def OAI.MinUncut.Outer.alphabet line 30
  7. lemma OAI.MinUncut.Outer.mem_alphabet line 40
  8. def OAI.MinUncut.Outer.origin line 43
  9. instance OAI.MinUncut.Outer.alphabetNonempty line 47
  10. instance OAI.MinUncut.Outer.alphabetFintype line 48
  11. instance OAI.MinUncut.Outer.directionFintype line 49
  12. lemma OAI.MinUncut.Outer.direction_parity line 51
  13. def OAI.MinUncut.Outer.firstTwo line 59
  14. lemma OAI.MinUncut.Outer.firstTwo_injective line 62
  15. lemma OAI.MinUncut.Outer.alphabet_dimension_le line 76
  16. def OAI.MinUncut.Outer.coordinates line 81
  17. def OAI.MinUncut.Outer.directionEmbedding line 85
  18. lemma OAI.MinUncut.Outer.directionEmbedding_injective line 89
  19. def OAI.MinUncut.Outer.alphabetCoordinates line 93
  20. lemma OAI.MinUncut.Outer.alphabetCoordinates_val line 97