def
EDT0LGrammar.HasDeadEnds
{T : Type u_1}
{N : Type u_2}
{H : Type u_3}
[Fintype H]
[Fintype N]
(E : EDT0LGrammar T N H)
(𝔇 : Finset N)
:
Equations
- E.HasDeadEnds 𝔇 = ∀ 𝔡 ∈ 𝔇, ∀ (τ : H), ∃ 𝔡' ∈ 𝔇, Symbol.nonterminal 𝔡' ∈ E.tables τ 𝔡
Instances For
def
EDT0LGrammar.DeadWord
{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))
:
Equations
- E.DeadWord w = ∃ (𝔇 : Finset N) (_ : E.HasDeadEnds 𝔇), ∃ 𝔡 ∈ 𝔇, Symbol.nonterminal 𝔡 ∈ w
Instances For
theorem
EDT0LGrammar.dead_end_singleton
{T : Type u_1}
{N : Type u_2}
{H : Type u_3}
[Fintype H]
[Fintype N]
(E : EDT0LGrammar T N H)
(𝔡 : N)
(h : ∀ (τ : H), Symbol.nonterminal 𝔡 ∈ E.tables τ 𝔡)
:
E.HasDeadEnds {𝔡}
theorem
EDT0LGrammar.rewrite_word_dead_end
{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)
(𝔇 : Finset N)
(h₁ : E.HasDeadEnds 𝔇)
(h₂ : ∃ 𝔡 ∈ 𝔇, Symbol.nonterminal 𝔡 ∈ w)
:
∃ 𝔡' ∈ 𝔇, Symbol.nonterminal 𝔡' ∈ E.RewriteWord τ w
theorem
EDT0LGrammar.rewrites_dead_end
{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))
(𝔇 : Finset N)
(h₁ : E.HasDeadEnds 𝔇)
(h₂ : ∃ 𝔡 ∈ 𝔇, Symbol.nonterminal 𝔡 ∈ w)
(h₃ : E.Rewrites w w')
:
∃ 𝔡' ∈ 𝔇, Symbol.nonterminal 𝔡' ∈ w'
theorem
EDT0LGrammar.derives_dead_end
{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))
(𝔇 : Finset N)
(h₁ : E.HasDeadEnds 𝔇)
(h₂ : ∃ 𝔡 ∈ 𝔇, Symbol.nonterminal 𝔡 ∈ w)
(h₃ : E.Derives w w')
:
∃ 𝔡' ∈ 𝔇, Symbol.nonterminal 𝔡' ∈ w'
theorem
EDT0LGrammar.rewrite_dead_word
{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)
(h : E.DeadWord w)
:
E.DeadWord (E.RewriteWord τ w)