OAI/Combinatorics/Automata/Syntactic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OneWayLiveness.BRel.singleton_context line 10
2. lemma OAI.OneWayLiveness.BRel.context_separates line 15
3. theorem OAI.OneWayLiveness.matching_recognition_degree line 25

   Source documentation

   Any matching recognition of liveness induces the full relation divisor. The recognizer predicate may in particular sandwich the fixed endmarkers and inspect the designated test ports.

   theorem matching_recognition_degree {H A : Type} [Fintype H] [Fintype A]
       (η : BRel H → Pairing (A ⊕ A)) (test : Pairing (A ⊕ A) → Prop)
       (hη : ∀ w : List (BRel H), test (w.map η).prod ↔ BRel.live w)
       (x y : H) (hxy : x ≠ y) : rankLoss (Fintype.card H) ≤ Fintype.card A := by
   …

   Mentions: OAI.OneWayLiveness.BRel, OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.BRel.live, OAI.OneWayLiveness.rankLoss