FiniteTreeWords.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recursive row words for the finite tree

The recursion in equation (finite-word) uses an additive state group, node shifts and leaf symbols. It is instantiated with the product of cyclic groups in the manuscript.

def OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord line 20

Source documentation

A row is the ordered concatenation of the m child words. At a leaf the word consists of its single tagged state symbol.

def nodeWord {m : ℕ} (T : ℕ) (leaf : List (Fin m) → A → Γ)
    (u : List (Fin m) → A) : ℕ → List (Fin m) → A → List Γ
  | 0, p, x => [leaf p x]
  | h + 1, p, x => (List.range T).flatMap fun a =>
      (List.finRange m).flatMap fun i => nodeWord T leaf u h (p ++ [i]) (x + a • u p)

/-- All node words at a given height have exactly the manuscript's length. -/

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_length line 27

Source documentation

All node words at a given height have exactly the manuscript's length.

@[simp] theorem nodeWord_length {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (p : List (Fin m)) (x : A) :
    (nodeWord T leaf u h p x).length = (m * T) ^ h := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord

def OAI.TreeEdit.BinaryLower.FiniteTree.nodeRow line 38

Source documentation

One row at a node of height h+1.

def nodeRow {m : ℕ} (T : ℕ) (leaf : List (Fin m) → A → Γ)
    (u : List (Fin m) → A) (h : ℕ) (p : List (Fin m)) (x : A) : List Γ :=
…

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeRow_length line 42

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_translate line 49

Source documentation

Translating by the cheap vector advances the row parameter.

theorem nodeWord_translate {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (p : List (Fin m)) (x : A) (s : ℕ) :
    nodeWord T leaf u (h + 1) p (x + s • u p) =
      (List.range T).flatMap fun a => nodeRow T leaf u h p (x + (s + a) • u p) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord, OAI.TreeEdit.BinaryLower.FiniteTree.nodeRow

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_invariant line 59
Source documentation
A translation invisible at every descendant leaf is invisible in the complete recursive word. The hypothesis is required for all states, permitting all ancestor offsets without adding any invariance assumption on the shifts.
```
theorem nodeWord_invariant {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (p : List (Fin m)) (z : A)
    (hinv : ∀ q : List (Fin m), q.length = h → ∀ x : A,
      leaf (p ++ q) (x + z) = leaf (p ++ q) x) (x : A) :
    nodeWord T leaf u h p (x + z) = nodeWord T leaf u h p x := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord