TransitionBridge.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.CompanionBridge.encodeSymbol line 12
Source documentation
The encodings have the same two distinct endmarkers.
```
def encodeSymbol {Alpha : Type*} : Symbol Alpha → Fin 2 ⊕ Alpha
  | .left => .inl 0
  | .letter a => .inr a
  | .right => .inl 1
```
theorem OAI.TwoWayComplementation.CompanionBridge.encode_scanned line 17
def OAI.TwoWayComplementation.CompanionBridge.encodeMove line 22
def OAI.TwoWayComplementation.CompanionBridge.decodeMove line 27
theorem OAI.TwoWayComplementation.CompanionBridge.encode_decode line 30
theorem OAI.TwoWayComplementation.CompanionBridge.encodeMove_injective line 33
theorem OAI.TwoWayComplementation.CompanionBridge.move_rel_iff line 37
def OAI.TwoWayComplementation.CompanionBridge.Guard line 42
Source documentation
A marker-outward transition is never usable on this bounded tape.
```
def Guard {Alpha : Type*} (a : Symbol Alpha) (m : Move) : Prop :=
…
```
theorem OAI.TwoWayComplementation.CompanionBridge.guard_of_legal_move line 45
def OAI.TwoWayComplementation.CompanionBridge.select line 63
Source documentation
Option-valued form of a partial transition. Only the single allowed element is selected.
```
noncomputable def select {X : Type*} (S : Set X) : Option X := by
…
```
theorem OAI.TwoWayComplementation.CompanionBridge.select_eq_some_iff line 67
def OAI.TwoWayComplementation.CompanionBridge.convertedTransitions line 78
Source documentation
Recode moves and remove only impossible outward marker transitions.
```
def convertedTransitions {Alpha : Type*} {s : ℕ} (A : TwoNFA Alpha (Fin s))
    (q : Fin s) (a : Symbol Alpha) : Set (Fin s × Move) :=
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA
theorem OAI.TwoWayComplementation.CompanionBridge.convertedTransitions_subsingleton line 82
def OAI.TwoWayComplementation.CompanionBridge.toDMachine line 93
Source documentation
A deterministic machine with exactly the same states and finite accepting runs. No halting or totality condition is introduced.
```
noncomputable def toDMachine {Alpha : Type*} {s : ℕ}
    (A : TwoNFA Alpha (Fin s)) (hA : A.Deterministic) : DMachine Alpha s where
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA
theorem OAI.TwoWayComplementation.CompanionBridge.toDMachine_step line 105
theorem OAI.TwoWayComplementation.CompanionBridge.toDMachine_accepts line 123