Normalization.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.tapeSymbol_left_iff line 10
Source documentation
Only the first tape position carries the left endmarker.
```
theorem tapeSymbol_left_iff {Sigma : Type*} (w : List Sigma) (p : Fin (w.length + 2)) :
    tapeSymbol w p = Sum.inl 0 ↔ p.val = 0 := by
…
```
Mentions: OAI.TwoWayComplementation.tapeSymbol
theorem OAI.TwoWayComplementation.tapeSymbol_right_iff line 16
Source documentation
Only the last original tape position carries the right endmarker.
```
theorem tapeSymbol_right_iff {Sigma : Type*} (w : List Sigma) (p : Fin (w.length + 2)) :
    tapeSymbol w p = Sum.inl 1 ↔ p.val = w.length + 1 := by
…
```
Mentions: OAI.TwoWayComplementation.tapeSymbol
def OAI.TwoWayComplementation.TwoNFA.reindex line 24
Source documentation
Rename states along an equivalence, retaining all transitions and moves.
```
def reindex {Sigma Q Q' : Type*} (A : TwoNFA Sigma Q) (e : Q ≃ Q') : TwoNFA Sigma Q' where
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA
theorem OAI.TwoWayComplementation.TwoNFA.reindex_language line 29
def OAI.TwoWayComplementation.TwoNFA.augmentConfig line 47
Source documentation
Embed an original configuration while reserving one state and one exit position.
```
def augmentConfig {Q : Type*} {n : ℕ} (c : Q × Fin n) : Option Q × Fin (n + 1) :=
…
```
theorem OAI.TwoWayComplementation.TwoNFA.augmentConfig_injective line 50
def OAI.TwoWayComplementation.TwoNFA.augmentedStep line 59
Source documentation
Original moves, an accepting stay into the fresh state, and its rightward sweep.
```
def augmentedStep {Sigma Q : Type*} (A : TwoNFA Sigma Q) (w : List Sigma) :
    SetRel (Option Q × Fin (w.length + 3)) (Option Q × Fin (w.length + 3)) :=
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA

theorem OAI.TwoWayComplementation.TwoNFA.augmented_run_cases line 68

Source documentation

Before entering the fresh state, every augmented finite path is an original run.

theorem augmented_run_cases {Sigma Q : Type*} (A : TwoNFA Sigma Q) (w : List Sigma)
    {c : Option Q × Fin (w.length + 3)}
    (hrun : (augmentConfig (A.initial, ⟨0, by omega⟩), c) ∈ relStar (A.augmentedStep w)) :
    w ∈ A.language ∨ ∃ x : Q × Fin (w.length + 2),
      c = augmentConfig x ∧ ((A.initial, ⟨0, by omega⟩), x) ∈ relStar (A.step w) := by
…

Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.TwoNFA.augmentConfig, OAI.TwoWayComplementation.relStar

theorem OAI.TwoWayComplementation.TwoNFA.augmented_sink_exit line 86
Source documentation
The fresh state can sweep from any position to the designated right exit.
```
theorem augmented_sink_exit {Sigma Q : Type*} (A : TwoNFA Sigma Q) (w : List Sigma)
    (p : Fin (w.length + 3)) :
    ((none, p), (none, ⟨w.length + 2, by omega⟩)) ∈ relStar (A.augmentedStep w) := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.relStar
theorem OAI.TwoWayComplementation.TwoNFA.augmented_acceptance line 106
Source documentation
Finite acceptance is equivalent to reaching the designated augmented exit.
```
theorem augmented_acceptance {Sigma Q : Type*} (A : TwoNFA Sigma Q) (w : List Sigma) :
    w ∈ A.language ↔
      (augmentConfig (A.initial, ⟨0, by omega⟩), (none, ⟨w.length + 2, by omega⟩)) ∈
        relStar (A.augmentedStep w) := by
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.TwoNFA.augmentConfig, OAI.TwoWayComplementation.relStar
def OAI.TwoWayComplementation.TwoNFA.augmentedMove line 126
Source documentation
Augmented moves at one symbol, including the original endmarker restrictions.
```
def augmentedMove {Sigma Q : Type*} (A : TwoNFA Sigma Q) (symbol : Fin 2 ⊕ Sigma)
    (move : Fin 3) : SetRel (Option Q) (Option Q) :=
…
```
Mentions: OAI.TwoWayComplementation.TwoNFA

theorem OAI.TwoWayComplementation.TwoNFA.augmentedStep_local_iff line 136

Source documentation

The global augmented graph is exactly the graph of the local moves and head displacement.

theorem augmentedStep_local_iff {Sigma Q : Type*} (A : TwoNFA Sigma Q) (w : List Sigma)
    (c d : Option Q × Fin (w.length + 3)) :
    (c, d) ∈ A.augmentedStep w ↔
      ∃ p : Fin (w.length + 2), c.2 = p.castSucc ∧ ∃ move : Fin 3,
        (c.1, d.1) ∈ A.augmentedMove (tapeSymbol w p) move ∧
        (d.2.val : ℤ) = (p.val : ℤ) + (move.val : ℤ) - 1 := by
…

Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.tapeSymbol