theorem List.split_commute_of_not_mem {α : Type u_1} (x y x' y' mid : List α) (a : α) (h : x ++ mid ++ y = x' ++ a :: y') (h_not_mem : a ∉ mid) : (∃ (z : List α), x' = x ++ mid ++ z ∧ y = z ++ a :: y') ∨ ∃ (z : List α), x = x' ++ a :: z ∧ y' = z ++ mid ++ y

theorem ContextFreeRule.Rewrites.map {T : Type u_1} {N : Type u_2} {T' : Type u_3} {N' : Type u_4} (f : Symbol T N → Symbol T' N') (r : ContextFreeRule T N) (r' : ContextFreeRule T' N') (u v : List (Symbol T N)) (h : r.Rewrites u v) (h_input : f (Symbol.nonterminal r.input) = Symbol.nonterminal r'.input) (h_output : r'.output = List.map f r.output) : r'.Rewrites (List.map f u) (List.map f v)

theorem ContextFreeRule.Rewrites.map_inv {T : Type u_1} {N : Type u_2} {T' : Type u_3} {N' : Type u_4} (f : Symbol T N → Symbol T' N') (hf : Function.Injective f) (r : ContextFreeRule T N) (r' : ContextFreeRule T' N') (u : List (Symbol T N)) (v' : List (Symbol T' N')) (h : r'.Rewrites (List.map f u) v') (h_input : f (Symbol.nonterminal r.input) = Symbol.nonterminal r'.input) (h_output : r'.output = List.map f r.output) : ∃ (v : List (Symbol T N)), v' = List.map f v ∧ r.Rewrites u v

theorem ContextFreeRule.Rewrites.mem_terminal_of_mem_target {T N : Type} (r : ContextFreeRule T N) (u v : List (Symbol T N)) (h : r.Rewrites u v) (a : T) (ha : Symbol.terminal a ∈ v) : Symbol.terminal a ∈ u ∨ Symbol.terminal a ∈ r.output

theorem ContextFreeRule.Rewrites.commute_of_not_mem_output {T N : Type} (r1 r2 : ContextFreeRule T N) (u v w : List (Symbol T N)) (h1 : r1.Rewrites u v) (h2 : r2.Rewrites v w) (h_disjoint : Symbol.nonterminal r2.input ∉ r1.output) : ∃ (v' : List (Symbol T N)), r2.Rewrites u v' ∧ r1.Rewrites v' w

theorem ContextFreeRule.Rewrites.split_append {T N : Type} (r : ContextFreeRule T N) (u v w : List (Symbol T N)) (h : r.Rewrites (u ++ v) w) : (∃ (u' : List (Symbol T N)), r.Rewrites u u' ∧ w = u' ++ v) ∨ ∃ (v' : List (Symbol T N)), r.Rewrites v v' ∧ w = u ++ v'

theorem ContextFreeGrammar.Derives.distrib_prod {T : Type} {g : ContextFreeGrammar T} (S : List (Symbol T g.NT)) (W : List (List (Symbol T g.NT))) (h : List.Forall₂ (fun (s : Symbol T g.NT) (w : List (Symbol T g.NT)) => g.Derives [s] w) S W) : g.Derives S W.flatten

theorem ContextFreeGrammar.Produces.split_append {T : Type} {g : ContextFreeGrammar T} (u v w : List (Symbol T g.NT)) (h : g.Produces (u ++ v) w) : (∃ (u' : List (Symbol T g.NT)), g.Produces u u' ∧ w = u' ++ v) ∨ ∃ (v' : List (Symbol T g.NT)), g.Produces v v' ∧ w = u ++ v'

theorem ContextFreeGrammar.Derives.split_append {T : Type} {g : ContextFreeGrammar T} (u v w : List (Symbol T g.NT)) (h : g.Derives (u ++ v) w) : ∃ (u' : List (Symbol T g.NT)) (v' : List (Symbol T g.NT)), g.Derives u u' ∧ g.Derives v v' ∧ w = u' ++ v'

theorem ContextFreeGrammar.no_rewrites_of_all_terminal {T N : Type} (r : ContextFreeRule T N) (w : List T) (v : List (Symbol T N)) : ¬r.Rewrites (List.map Symbol.terminal w) v

theorem ContextFreeGrammar.no_produces_of_all_terminal {T : Type} (g : ContextFreeGrammar T) (w : List T) (v : List (Symbol T g.NT)) : ¬g.Produces (List.map Symbol.terminal w) v

theorem ContextFreeGrammar.derives_of_all_terminal {T : Type} (g : ContextFreeGrammar T) (w : List T) (v : List (Symbol T g.NT)) : g.Derives (List.map Symbol.terminal w) v → v = List.map Symbol.terminal w

theorem ContextFreeGrammar.derives_commute_of_not_mem_output {T N : Type} {R₁ R₂ : Finset (ContextFreeRule T N)} (h : ∀ r₁ ∈ R₁, ∀ r₂ ∈ R₂, Symbol.nonterminal r₂.input ∉ r₁.output) {u v w : List (Symbol T N)} (h₁ : Relation.ReflTransGen (fun (u v : List (Symbol T N)) => ∃ r ∈ R₁, r.Rewrites u v) u v) (h₂ : Relation.ReflTransGen (fun (u v : List (Symbol T N)) => ∃ r ∈ R₂, r.Rewrites u v) v w) : ∃ (v' : List (Symbol T N)), Relation.ReflTransGen (fun (u v : List (Symbol T N)) => ∃ r ∈ R₂, r.Rewrites u v) u v' ∧ Relation.ReflTransGen (fun (u v : List (Symbol T N)) => ∃ r ∈ R₁, r.Rewrites u v) v' w