Tape.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.chainSymbol_getElem line 11
Source documentation
Chain symbols agree with ordinary zero-based lookup of the nonempty symbol list.
```
theorem chainSymbol_getElem {Sigma : Type*} {m : ℕ} (w : List Sigma) (last : Sigma)
    (c : ChainNode m w.length) :
    chainSymbol w last c = (w ++ [last])[c.position]'(by
      have := c.position_le
…
```
Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.chainSymbol

theorem OAI.TwoWayComplementation.marked_getElem line 26

Source documentation

Lookup of the explicitly marked list agrees with the automaton's tape lookup.

theorem marked_getElem {Sigma : Type*} (w : List Sigma) (p : Fin (w.length + 2)) :
    ((Sum.inl 0 : Fin 2 ⊕ Sigma) :: (w.map Sum.inr ++ [Sum.inl 1]))[p.val]'(by simp; omega) =
      tapeSymbol w p := by
…

Mentions: OAI.TwoWayComplementation.tapeSymbol

def OAI.TwoWayComplementation.ChainNode.exitEquiv line 42
Source documentation
Convert the recursively joined cells and one terminal exit into tape coordinates.
```
noncomputable def ChainNode.exitEquiv (m n : ℕ) :
    (ChainNode m n ⊕ Fin m) ≃ (Fin m × Fin (n + 2)) :=
…
```
Mentions: OAI.TwoWayComplementation.ChainNode

theorem OAI.TwoWayComplementation.relStar_equiv_iff line 67

Source documentation

A graph equivalence transports finite paths in both directions.

theorem relStar_equiv_iff {V W : Type*} (e : V ≃ W) (R : SetRel V V) (S : SetRel W W)
    (h : ∀ x y, (e x, e y) ∈ S ↔ (x, y) ∈ R) (x y : V) :
    (e x, e y) ∈ relStar S ↔ (x, y) ∈ relStar R := by
…

Mentions: OAI.TwoWayComplementation.relStar

theorem OAI.TwoWayComplementation.blockRelation_terminal line 81
Source documentation
A terminal block with no outgoing edges is reached by an internal path and one exit.
```
theorem blockRelation_terminal {V Q : Type*} (E : SetRel V V) (O : SetRel V Q)
    (c : V) (q : Q) :
    (Sum.inl c, Sum.inr q) ∈ relStar (blockRelation E O ∅ ∅) ↔
      (c, q) ∈ relStar E ○ O := by
…
```
Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.blockRelation
theorem OAI.TwoWayComplementation.chainSymbol_position line 89
Source documentation
A cell's scanned symbol depends only on its position.
```
theorem chainSymbol_position {Sigma : Type*} {m : ℕ} (w : List Sigma) (last : Sigma)
    (c d : ChainNode m w.length) (hp : c.position = d.position) :
    chainSymbol w last c = chainSymbol w last d := by
…
```
Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.chainSymbol

def OAI.TwoWayComplementation.chainStep line 96

Source documentation

Local moves on the bounded tape, with a final terminal position beyond the last cell.

def chainStep {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) :
    SetRel (Fin m × Fin (w.length + 2)) (Fin m × Fin (w.length + 2)) :=
…

theorem OAI.TwoWayComplementation.chainStep_exitEquiv line 104

Source documentation

The joined network with terminal exits has exactly the bounded tape's local edges.

theorem chainStep_exitEquiv {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma)
    (x y : ChainNode m w.length ⊕ Fin m) :
    (ChainNode.exitEquiv m w.length x, ChainNode.exitEquiv m w.length y) ∈
        chainStep moves w last ↔
      (x, y) ∈ blockRelation (chainNetwork moves w last).edge
        (chainNetwork moves w last).rightOut ∅ ∅ := by
…

Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.ChainNode.exitEquiv, OAI.TwoWayComplementation.chainStep, OAI.TwoWayComplementation.blockRelation, OAI.TwoWayComplementation.chainNetwork

theorem OAI.TwoWayComplementation.chainStep_recognition line 149

Source documentation

The designated forward edge of a diagram product is exactly a successful tape run.

theorem chainStep_recognition {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma)
    (q r : Fin m) :
    ((q, ⟨0, by omega⟩), (r, ⟨w.length + 1, by omega⟩)) ∈ relStar (chainStep moves w last) ↔
      (q, r) ∈ (chainNetwork moves w last).summary.forward := by
…

Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.chainStep, OAI.TwoWayComplementation.chainNetwork