Model.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.relStar line 10
Source documentation
Reflexive transitive closure, including the empty path.
Also declared: ComparatorChallenges/TwoWayComplementation.lean:9 (same declaration text), ComparatorChallenges/TwoWayDeterminization.lean:10 (same declaration text).
```
def relStar {α : Type*} (R : SetRel α α) : SetRel α α :=
…
```
structure OAI.TwoWayComplementation.TwoNFA line 15
Source documentation
A read-only 2NFA. The two endmarkers are Sum.inl 0 and Sum.inl 1. Move codes 0, 1, 2 mean left, stay, right.
Also declared: ComparatorChallenges/TwoWayComplementation.lean:12 (same declaration text), ComparatorChallenges/TwoWayDeterminization.lean:15 (same declaration text).
```
structure TwoNFA (Sigma Q : Type*) where
…
```
def OAI.TwoWayComplementation.tapeSymbol line 24
Source documentation
Tape lookup includes two distinct endmarkers, even on empty input.
Also declared: ComparatorChallenges/TwoWayComplementation.lean:17 (same declaration text), ComparatorChallenges/TwoWayDeterminization.lean:24 (same declaration text).
```
def tapeSymbol {Sigma : Type*} (w : List Sigma) (p : Fin (w.length + 2)) : Fin 2 ⊕ Sigma :=
…
```
def OAI.TwoWayComplementation.TwoNFA.step line 32
Source documentation
One legal step: both head positions stay within the marked input.
Also declared: ComparatorChallenges/TwoWayComplementation.lean:24 (same declaration text), ComparatorChallenges/TwoWayDeterminization.lean:32 (same declaration text).
```
def step {Sigma Q : Type*} (A : TwoNFA Sigma Q) (w : List Sigma) :
    SetRel (Q × Fin (w.length + 2)) (Q × Fin (w.length + 2)) :=
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA
def OAI.TwoWayComplementation.TwoNFA.language line 39
Source documentation
Existential finite-run acceptance, allowing a run of length zero.
Also declared: ComparatorChallenges/TwoWayComplementation.lean:30 (same declaration text), ComparatorChallenges/TwoWayDeterminization.lean:39 (same declaration text).
```
def language {Sigma Q : Type*} (A : TwoNFA Sigma Q) : Set (List Sigma) :=
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA