Source.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.relationProduct line 11
Source documentation
Relation product for an input word; the empty product is the identity.
Also declared: ComparatorChallenges/TwoWayDeterminization.lean:50 (same declaration text).
```
def relationProduct {H : Type*} (w : List (SetRel H H)) : SetRel H H :=
…
```
theorem OAI.TwoWayComplementation.relationProduct_append line 14
def OAI.TwoWayComplementation.sourceLanguage line 21
Source documentation
The source language consists of the words with nonempty relation product.
Also declared: ComparatorChallenges/TwoWayDeterminization.lean:54 (same declaration text).
```
def sourceLanguage (H : Type*) : Set (List (SetRel H H)) :=
…
```
def OAI.TwoWayComplementation.sourceAutomaton line 26
Source documentation
The explicit source machine: none starts, some none accepts, and some (some h) is the state labelled by h.
```
def sourceAutomaton (H : Type*) : TwoNFA (SetRel H H) (Option (Option H)) where
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA
def OAI.TwoWayComplementation.sourceProductive line 39
Source documentation
Configurations from which the explicit source machine has a suffix witness.
```
def sourceProductive {H : Type*} (w : List (SetRel H H)) :
    Set (Option (Option H) × Fin (w.length + 2)) :=
…
```
theorem OAI.TwoWayComplementation.sourceProductive_of_step line 46
theorem OAI.TwoWayComplementation.sourceAutomaton_sound line 96
theorem OAI.TwoWayComplementation.sourceAutomaton_suffix_run line 111
theorem OAI.TwoWayComplementation.sourceAutomaton_language line 141
Source documentation
The explicit machine recognizes nonempty relation products.
```
theorem sourceAutomaton_language (H : Type*) :
    (sourceAutomaton H).language = sourceLanguage H := by
…
```
Mentions: OAI.TwoWayComplementation.sourceAutomaton, OAI.TwoWayComplementation.sourceLanguage
theorem OAI.TwoWayComplementation.sourceLanguage_state_bound line 155
Source documentation
The source language on h labels is recognized using exactly h + 2 states.
```
theorem sourceLanguage_state_bound (H : Type*) [Fintype H] :
    ∃ A : TwoNFA (SetRel H H) (Fin (Fintype.card H + 2)), A.language = sourceLanguage H := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.sourceLanguage
theorem OAI.TwoWayComplementation.singleton_word_context line 164
Source documentation
Singleton letters on the two sides test one edge of a word's relation product.
```
theorem singleton_word_context {H : Type*} (w : List (SetRel H H)) (p q : H) :
    (relationProduct ([restrictedIdentity {p}] ++ w ++ [restrictedIdentity {q}])).Nonempty ↔
      (p, q) ∈ relationProduct w := by
…
```
Mentions: OAI.TwoWayComplementation.relationProduct, OAI.TwoWayComplementation.restrictedIdentity