Counted derivations for indexed normal form

Exact-step derivations, append splitting, terminal-source rigidity, and the four normal-form rule cases used to turn derivations into data-carrying parse certificates.

Minimal sentential counting support

Counted derivations

def IndexedGrammar.DerivesIn {T : Type} (g : IndexedGrammar T) : ℕ → List g.ISym → List g.ISym → Prop

DerivesIn g n w₁ w₂ means that w₁ derives w₂ in exactly n indexed-grammar steps. This is a counted counterpart to Derives, useful when extracting minimal accepting derivations.

Equations

• g.DerivesIn 0 x✝¹ x✝ = (x✝¹ = x✝)
• g.DerivesIn n.succ x✝¹ x✝ = ∃ (w : List g.ISym), g.DerivesIn n x✝¹ w ∧ g.Transforms w x✝

@[simp]

theorem IndexedGrammar.derivesIn_zero {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} : g.DerivesIn 0 w₁ w₂ ↔ w₁ = w₂

@[simp]

theorem IndexedGrammar.derivesIn_succ {T : Type} {g : IndexedGrammar T} {n : ℕ} {w₁ w₂ : List g.ISym} : g.DerivesIn (n + 1) w₁ w₂ ↔ ∃ (w : List g.ISym), g.DerivesIn n w₁ w ∧ g.Transforms w w₂

theorem IndexedGrammar.derivesIn_one_of_transforms {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : g.DerivesIn 1 w₁ w₂

theorem IndexedGrammar.derives_of_derivesIn {T : Type} {g : IndexedGrammar T} {n : ℕ} {w₁ w₂ : List g.ISym} (h : g.DerivesIn n w₁ w₂) : g.Derives w₁ w₂

theorem IndexedGrammar.exists_derivesIn_of_derives {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) : ∃ (n : ℕ), g.DerivesIn n w₁ w₂

theorem IndexedGrammar.derives_iff_exists_derivesIn {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} : g.Derives w₁ w₂ ↔ ∃ (n : ℕ), g.DerivesIn n w₁ w₂

theorem IndexedGrammar.derivesIn_trans {T : Type} {g : IndexedGrammar T} {m n : ℕ} {w₁ w₂ w₃ : List g.ISym} (h₁ : g.DerivesIn m w₁ w₂) (h₂ : g.DerivesIn n w₂ w₃) : g.DerivesIn (m + n) w₁ w₃

theorem IndexedGrammar.derivesIn_split {T : Type} {g : IndexedGrammar T} {m n : ℕ} {w₁ w₃ : List g.ISym} (h : g.DerivesIn (m + n) w₁ w₃) : ∃ (w₂ : List g.ISym), g.DerivesIn m w₁ w₂ ∧ g.DerivesIn n w₂ w₃

Split a counted derivation after m steps.

theorem IndexedGrammar.generates_iff_exists_derivesIn {T : Type} (g : IndexedGrammar T) (w : List T) : g.Generates w ↔ ∃ (n : ℕ), g.DerivesIn n [ISym.indexed g.initial []] (List.map ISym.terminal w)

Split a counted derivation at any index i ≤ n.

Append splitting

theorem IndexedGrammar.transforms_append_left {T : Type} {g : IndexedGrammar T} {u u' : List g.ISym} (h : g.Transforms u u') (v : List g.ISym) : g.Transforms (u ++ v) (u' ++ v)

A one-step indexed rewrite remains valid after appending an unchanged right context.

theorem IndexedGrammar.transforms_append_right {T : Type} {g : IndexedGrammar T} {v v' : List g.ISym} (h : g.Transforms v v') (u : List g.ISym) : g.Transforms (u ++ v) (u ++ v')

A one-step indexed rewrite remains valid after prepending an unchanged left context.

theorem IndexedGrammar.derivesIn_append_left {T : Type} {g : IndexedGrammar T} {n : ℕ} {u u' : List g.ISym} (h : g.DerivesIn n u u') (v : List g.ISym) : g.DerivesIn n (u ++ v) (u' ++ v)

Counted indexed derivations are closed under appending an unchanged right context.

theorem IndexedGrammar.derivesIn_append_right {T : Type} {g : IndexedGrammar T} {n : ℕ} {v v' : List g.ISym} (h : g.DerivesIn n v v') (u : List g.ISym) : g.DerivesIn n (u ++ v) (u ++ v')

Counted indexed derivations are closed under prepending an unchanged left context.

theorem IndexedGrammar.derivesIn_append {T : Type} {g : IndexedGrammar T} {m n : ℕ} {u u' v v' : List g.ISym} (hu : g.DerivesIn m u u') (hv : g.DerivesIn n v v') : g.DerivesIn (m + n) (u ++ v) (u' ++ v')

Independent counted indexed derivations compose over append.

theorem IndexedGrammar.derivesIn_append_to_terminals_of_derivesIn {T : Type} {g : IndexedGrammar T} {m n : ℕ} {u v : List g.ISym} {wu wv : List T} (hu : g.DerivesIn m u (List.map (fun (a : T) => ISym.terminal a) wu)) (hv : g.DerivesIn n v (List.map (fun (a : T) => ISym.terminal a) wv)) : g.DerivesIn (m + n) (u ++ v) (List.map (fun (a : T) => ISym.terminal a) (wu ++ wv))

Counted terminal-word composition over append.

theorem IndexedGrammar.not_transforms_nil {T : Type} {g : IndexedGrammar T} {w : List g.ISym} : ¬g.Transforms [] w

There is no indexed-grammar rewrite step whose source sentential form is empty.

theorem IndexedGrammar.derivesIn_nil_left_eq {T : Type} {g : IndexedGrammar T} {n : ℕ} {w : List g.ISym} (h : g.DerivesIn n [] w) : n = 0 ∧ w = []

A counted derivation starting from the empty sentential form is necessarily the zero-step derivation to the empty sentential form.

theorem IndexedGrammar.derivesIn_pair_to_terminals_of_derivesIn {T : Type} {g : IndexedGrammar T} {m n : ℕ} {A B : g.nt} {σ τ : List g.flag} {u v : List T} (hleft : g.DerivesIn m [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) u)) (hright : g.DerivesIn n [ISym.indexed B τ] (List.map (fun (a : T) => ISym.terminal a) v)) : g.DerivesIn (m + n) [ISym.indexed A σ, ISym.indexed B τ] (List.map (fun (a : T) => ISym.terminal a) (u ++ v))

theorem IndexedGrammar.transforms_append_cases_of_append {T : Type} {g : IndexedGrammar T} {u v w : List g.ISym} (hstep : g.Transforms (u ++ v) w) : (∃ (u' : List g.ISym), g.Transforms u u' ∧ w = u' ++ v) ∨ ∃ (v' : List g.ISym), g.Transforms v v' ∧ w = u ++ v'

A one-step indexed rewrite of an appended sentential form rewrites either the left side or the right side of the append.

theorem IndexedGrammar.derivesIn_append_split {T : Type} {g : IndexedGrammar T} {n : ℕ} {u v x : List g.ISym} (hder : g.DerivesIn n (u ++ v) x) : ∃ (m : ℕ) (k : ℕ) (u' : List g.ISym) (v' : List g.ISym), m + k = n ∧ x = u' ++ v' ∧ g.DerivesIn m u u' ∧ g.DerivesIn k v v'

A counted derivation from an appended sentential form can be factored into counted derivations from the two sides of the append. The two side budgets add up to the original budget.

theorem IndexedGrammar.append_eq_map_terminal_split {T : Type} {g : IndexedGrammar T} {u v : List g.ISym} {w : List T} (h : u ++ v = List.map (fun (a : T) => ISym.terminal a) w) : ∃ (wu : List T) (wv : List T), w = wu ++ wv ∧ u = List.map (fun (a : T) => ISym.terminal a) wu ∧ v = List.map (fun (a : T) => ISym.terminal a) wv

theorem IndexedGrammar.derives_append_to_terminals_split {T : Type} {g : IndexedGrammar T} {u v : List g.ISym} {w : List T} (hder : g.Derives (u ++ v) (List.map (fun (a : T) => ISym.terminal a) w)) : ∃ (wu : List T) (wv : List T), w = wu ++ wv ∧ g.Derives u (List.map (fun (a : T) => ISym.terminal a) wu) ∧ g.Derives v (List.map (fun (a : T) => ISym.terminal a) wv)

theorem IndexedGrammar.derivesIn_append_to_terminals_split {T : Type} {g : IndexedGrammar T} {n : ℕ} {u v : List g.ISym} {w : List T} (hder : g.DerivesIn n (u ++ v) (List.map (fun (a : T) => ISym.terminal a) w)) : ∃ (m : ℕ) (k : ℕ) (wu : List T) (wv : List T), m + k = n ∧ w = wu ++ wv ∧ g.DerivesIn m u (List.map (fun (a : T) => ISym.terminal a) wu) ∧ g.DerivesIn k v (List.map (fun (a : T) => ISym.terminal a) wv)

Counted split of an appended terminal derivation.

theorem IndexedGrammar.derivesIn_pair_to_terminals_split {T : Type} {g : IndexedGrammar T} {n : ℕ} {A B : g.nt} {σ τ : List g.flag} {w : List T} (hder : g.DerivesIn n [ISym.indexed A σ, ISym.indexed B τ] (List.map (fun (a : T) => ISym.terminal a) w)) : ∃ (m : ℕ) (k : ℕ) (u : List T) (v : List T), m + k = n ∧ w = u ++ v ∧ g.DerivesIn m [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) u) ∧ g.DerivesIn k [ISym.indexed B τ] (List.map (fun (a : T) => ISym.terminal a) v)

Counted split for the pair produced by a normal-form binary branch.

theorem IndexedGrammar.not_transforms_from_terminals {T : Type} {g : IndexedGrammar T} {w : List T} {x : List g.ISym} : ¬g.Transforms (List.map (fun (a : T) => ISym.terminal a) w) x

theorem IndexedGrammar.derives_from_terminals_eq {T : Type} {g : IndexedGrammar T} {u : List T} {w : List g.ISym} (hder : g.Derives (List.map (fun (a : T) => ISym.terminal a) u) w) : w = List.map (fun (a : T) => ISym.terminal a) u

theorem IndexedGrammar.derives_terminals_inj {T : Type} {g : IndexedGrammar T} {u w : List T} (hder : g.Derives (List.map (fun (a : T) => ISym.terminal a) u) (List.map (fun (a : T) => ISym.terminal a) w)) : w = u

theorem IndexedGrammar.derives_terminal_singleton_eq {T : Type} {g : IndexedGrammar T} {a : T} {w : List T} (hder : g.Derives [ISym.terminal a] (List.map (fun (b : T) => ISym.terminal b) w)) : w = [a]

theorem IndexedGrammar.derivesIn_from_terminals_eq {T : Type} {g : IndexedGrammar T} {n : ℕ} {u : List T} {w : List g.ISym} (hder : g.DerivesIn n (List.map (fun (a : T) => ISym.terminal a) u) w) : w = List.map (fun (a : T) => ISym.terminal a) u

theorem IndexedGrammar.not_derivesIn_succ_from_terminals {T : Type} {g : IndexedGrammar T} {n : ℕ} {u : List T} {w : List g.ISym} : ¬g.DerivesIn (n + 1) (List.map (fun (a : T) => ISym.terminal a) u) w

theorem IndexedGrammar.derivesIn_terminal_singleton_eq {T : Type} {g : IndexedGrammar T} {n : ℕ} {a : T} {w : List T} (hder : g.DerivesIn n [ISym.terminal a] (List.map (fun (b : T) => ISym.terminal b) w)) : w = [a]

theorem IndexedGrammar.derivesIn_terminal_singleton_steps_eq_zero {T : Type} {g : IndexedGrammar T} {n : ℕ} {a : T} {w : List T} (hder : g.DerivesIn n [ISym.terminal a] (List.map (fun (b : T) => ISym.terminal b) w)) : n = 0

Normal-form rule decomposition

def IndexedGrammar.TransformIsBinaryStep {T : Type} (g : IndexedGrammar T) (w₁ w₂ : List g.ISym) : Prop

Equations

• One or more equations did not get rendered due to their size.

def IndexedGrammar.TransformIsPopStep {T : Type} (g : IndexedGrammar T) (w₁ w₂ : List g.ISym) : Prop

A normal-form flag-pop step A[f :: σ] ↦ B[σ].

Equations

• One or more equations did not get rendered due to their size.

def IndexedGrammar.TransformIsPushStep {T : Type} (g : IndexedGrammar T) (w₁ w₂ : List g.ISym) : Prop

A normal-form flag-push step A[σ] ↦ B[f :: σ].

Equations

• One or more equations did not get rendered due to their size.

def IndexedGrammar.TransformIsTerminalStep {T : Type} (g : IndexedGrammar T) (w₁ w₂ : List g.ISym) : Prop

A normal-form terminal-emission step A[σ] ↦ a.

Equations

• One or more equations did not get rendered due to their size.

theorem IndexedGrammar.transforms_cases_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : (∃ (A : g.nt) (B : g.nt) (C : g.nt) (u : List g.ISym) (v : List g.ISym) (σ : List g.flag), B ≠ g.initial ∧ C ≠ g.initial ∧ w₁ = u ++ [ISym.indexed A σ] ++ v ∧ w₂ = u ++ [ISym.indexed B σ, ISym.indexed C σ] ++ v) ∨ (∃ (A : g.nt) (B : g.nt) (f : g.flag) (u : List g.ISym) (v : List g.ISym) (σ : List g.flag), B ≠ g.initial ∧ w₁ = u ++ [ISym.indexed A (f :: σ)] ++ v ∧ w₂ = u ++ [ISym.indexed B σ] ++ v) ∨ (∃ (A : g.nt) (B : g.nt) (f : g.flag) (u : List g.ISym) (v : List g.ISym) (σ : List g.flag), B ≠ g.initial ∧ w₁ = u ++ [ISym.indexed A σ] ++ v ∧ w₂ = u ++ [ISym.indexed B (f :: σ)] ++ v) ∨ ∃ (A : g.nt) (a : T) (u : List g.ISym) (v : List g.ISym) (σ : List g.flag), w₁ = u ++ [ISym.indexed A σ] ++ v ∧ w₂ = u ++ [ISym.terminal a] ++ v

A one-step rewrite in normal form has exactly one of the four indexed-normal-form shapes: binary split, flag pop, flag push, or terminal emission.

theorem IndexedGrammar.transforms_kind_cases_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : g.TransformIsBinaryStep w₁ w₂ ∨ g.TransformIsPopStep w₁ w₂ ∨ g.TransformIsPushStep w₁ w₂ ∨ g.TransformIsTerminalStep w₁ w₂

theorem IndexedGrammar.transforms_singleton_binary_iff_rule_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {A B C : g.nt} {σ : List g.flag} : g.Transforms [ISym.indexed A σ] [ISym.indexed B σ, ISym.indexed C σ] ↔ ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]

theorem IndexedGrammar.transforms_singleton_pop_iff_rule_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {A B : g.nt} {f : g.flag} {ρ : List g.flag} : g.Transforms [ISym.indexed A (f :: ρ)] [ISym.indexed B ρ] ↔ ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none]

theorem IndexedGrammar.transforms_singleton_push_iff_rule_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {A B : g.nt} {f : g.flag} {σ : List g.flag} : g.Transforms [ISym.indexed A σ] [ISym.indexed B (f :: σ)] ↔ ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B (some f)]

theorem IndexedGrammar.transforms_singleton_terminal_iff_rule_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {A : g.nt} {σ : List g.flag} {a : T} : g.Transforms [ISym.indexed A σ] [ISym.terminal a] ↔ ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.terminal a]

theorem IndexedGrammar.derivesIn_singleton_to_terminals_cases_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {n : ℕ} {A : g.nt} {σ : List g.flag} {w : List T} (hder : g.DerivesIn (n + 1) [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)) : (∃ (B : g.nt) (C : g.nt) (m : ℕ) (k : ℕ) (u : List T) (v : List T), m + k = n ∧ w = u ++ v ∧ g.Transforms [ISym.indexed A σ] [ISym.indexed B σ, ISym.indexed C σ] ∧ g.DerivesIn m [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u) ∧ g.DerivesIn k [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) ∨ (∃ (f : g.flag) (ρ : List g.flag) (B : g.nt), σ = f :: ρ ∧ g.Transforms [ISym.indexed A σ] [ISym.indexed B ρ] ∧ g.DerivesIn n [ISym.indexed B ρ] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ (∃ (B : g.nt) (f : g.flag), g.Transforms [ISym.indexed A σ] [ISym.indexed B (f :: σ)] ∧ g.DerivesIn n [ISym.indexed B (f :: σ)] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ ∃ (a : T), g.Transforms [ISym.indexed A σ] [ISym.terminal a] ∧ w = [a] ∧ n = 0

Counted first-step analysis for a terminal derivation from one indexed nonterminal in normal form. The binary case splits both the terminal word and the remaining step budget.

theorem IndexedGrammar.derivesIn_singleton_to_terminals_iff_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {n : ℕ} {A : g.nt} {σ : List g.flag} {w : List T} : g.DerivesIn (n + 1) [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w) ↔ (∃ (B : g.nt) (C : g.nt) (m : ℕ) (k : ℕ) (u : List T) (v : List T), m + k = n ∧ w = u ++ v ∧ g.Transforms [ISym.indexed A σ] [ISym.indexed B σ, ISym.indexed C σ] ∧ g.DerivesIn m [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u) ∧ g.DerivesIn k [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) ∨ (∃ (f : g.flag) (ρ : List g.flag) (B : g.nt), σ = f :: ρ ∧ g.Transforms [ISym.indexed A σ] [ISym.indexed B ρ] ∧ g.DerivesIn n [ISym.indexed B ρ] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ (∃ (B : g.nt) (f : g.flag), g.Transforms [ISym.indexed A σ] [ISym.indexed B (f :: σ)] ∧ g.DerivesIn n [ISym.indexed B (f :: σ)] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ ∃ (a : T), g.Transforms [ISym.indexed A σ] [ISym.terminal a] ∧ w = [a] ∧ n = 0

Exact counted recursive characterization of terminal derivations from one indexed nonterminal in normal form.

theorem IndexedGrammar.derivesIn_singleton_to_terminals_rule_iff_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {n : ℕ} {A : g.nt} {σ : List g.flag} {w : List T} : g.DerivesIn (n + 1) [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w) ↔ (∃ (B : g.nt) (C : g.nt) (m : ℕ) (k : ℕ) (u : List T) (v : List T), ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none] ∧ m + k = n ∧ w = u ++ v ∧ g.DerivesIn m [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u) ∧ g.DerivesIn k [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) ∨ (∃ (f : g.flag) (ρ : List g.flag) (B : g.nt), ∃ r ∈ g.rules, σ = f :: ρ ∧ r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none] ∧ g.DerivesIn n [ISym.indexed B ρ] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ (∃ (B : g.nt) (f : g.flag), ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B (some f)] ∧ g.DerivesIn n [ISym.indexed B (f :: σ)] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ ∃ (a : T), ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.terminal a] ∧ w = [a] ∧ n = 0

Counted recursive characterization using concrete normal-form rules from g.rules. This is the finite-search-facing form of singleton terminal derivability.

theorem IndexedGrammar.derives_singleton_to_terminals_length_pos_of_noEpsilon {T : Type} {g : IndexedGrammar T} (hne : g.NoEpsilon') {A : g.nt} {σ : List g.flag} {w : List T} (hder : g.Derives [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)) : 0 < w.length

theorem IndexedGrammar.binary_subderivations_lengths_pos_of_noEpsilon {T : Type} {g : IndexedGrammar T} (hne : g.NoEpsilon') {B C : g.nt} {σ : List g.flag} {u v : List T} (hleft : g.Derives [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u)) (hright : g.Derives [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) : 0 < u.length ∧ 0 < v.length

theorem IndexedGrammar.binary_subderivations_lengths_lt_parent_of_noEpsilon {T : Type} {g : IndexedGrammar T} (hne : g.NoEpsilon') {B C : g.nt} {σ : List g.flag} {w u v : List T} (hw : w = u ++ v) (hleft : g.Derives [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u)) (hright : g.Derives [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) : u.length < w.length ∧ v.length < w.length

theorem IndexedGrammar.binary_subderivations_lengths_lt_parent_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {B C : g.nt} {σ : List g.flag} {w u v : List T} (hw : w = u ++ v) (hleft : g.Derives [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u)) (hright : g.Derives [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) : u.length < w.length ∧ v.length < w.length

theorem IndexedGrammar.binary_subderivation_words_sublist_parent {T : Type} {w u v : List T} (hw : w = u ++ v) : u.Sublist w ∧ v.Sublist w

The two words generated by a binary branch are sublists of the parent word.

theorem IndexedGrammar.binary_subderivation_words_sublist_target {T : Type} {w u v target : List T} (hw : w = u ++ v) (hwt : w.Sublist target) : u.Sublist target ∧ v.Sublist target

Binary branch words remain inside any target word containing the parent as a sublist.

theorem IndexedGrammar.derivesIn_singleton_to_terminals_rule_cases_with_target_bounds_of_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {n : ℕ} {A : g.nt} {σ : List g.flag} {w target : List T} (hwt : w.Sublist target) (hder : g.DerivesIn (n + 1) [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)) : (∃ (B : g.nt) (C : g.nt) (m : ℕ) (k : ℕ) (u : List T) (v : List T), ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none] ∧ m + k = n ∧ m < n + 1 ∧ k < n + 1 ∧ w = u ++ v ∧ 0 < u.length ∧ 0 < v.length ∧ u.length < w.length ∧ v.length < w.length ∧ u.Sublist target ∧ v.Sublist target ∧ g.DerivesIn m [ISym.indexed B σ] (List.map (fun (a : T) => ISym.terminal a) u) ∧ g.DerivesIn k [ISym.indexed C σ] (List.map (fun (a : T) => ISym.terminal a) v)) ∨ (∃ (f : g.flag) (ρ : List g.flag) (B : g.nt), ∃ r ∈ g.rules, σ = f :: ρ ∧ r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none] ∧ n < n + 1 ∧ g.DerivesIn n [ISym.indexed B ρ] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ (∃ (B : g.nt) (f : g.flag), ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B (some f)] ∧ n < n + 1 ∧ g.DerivesIn n [ISym.indexed B (f :: σ)] (List.map (fun (a : T) => ISym.terminal a) w)) ∨ ∃ (a : T), ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.terminal a] ∧ w = [a] ∧ n = 0

Counted forward rule-level singleton decomposition with explicit decreasing sub-budgets and target-compatible child yields. This is the finite-search form of the first-step analysis: every recursive premise has a strictly smaller counted budget, and binary premises also have nonempty, strictly smaller terminal yields contained in the ambient target.