def EDT0LGrammar.DeriveSequence {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (s : List H) (w : List (Symbol T N)) : List (Symbol T N)

Equations

• E.DeriveSequence s w = List.foldl (fun (w' : List (Symbol T N)) (τ : H) => E.RewriteWord τ w') w s

@[simp]

theorem EDT0LGrammar.DeriveSequence.derives_seq_refl {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (w : List (Symbol T N)) : E.DeriveSequence [] w = w

theorem EDT0LGrammar.DeriveSequence.rewrite_word_iff_derive_seq_singleton {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (w : List (Symbol T N)) (τ : H) : E.RewriteWord τ w = E.DeriveSequence [τ] w

theorem EDT0LGrammar.DeriveSequence.rewrites_iff_derive_seq_singleton {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (w w' : List (Symbol T N)) : E.Rewrites w w' ↔ ∃ (τ : H), E.DeriveSequence [τ] w = w'

theorem EDT0LGrammar.DeriveSequence.derives_iff_derive_seq {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (w w' : List (Symbol T N)) : E.Derives w w' ↔ ∃ (s : List H), E.DeriveSequence s w = w'