α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : ∃ L, y = List.join L ∧ ∀ (y : List α), y ∈ L → y ∈ {x}
⊢ evalFrom M s y = s
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : y ∈ {x}∗
⊢ evalFrom M s y = s
rw [Language.mem_kstar] at hy
case intro.intro
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ {x}
⊢ evalFrom M s (List.join S) = s
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : ∃ L, y = List.join L ∧ ∀ (y : List α), y ∈ L → y ∈ {x}
⊢ evalFrom M s y = s
rcases hy with ⟨S, rfl, hS⟩
case intro.intro.nil
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS✝ : ∀ (y : List α), y ∈ S → y ∈ {x}
hS : ∀ (y : List α), y ∈ [] → y ∈ {x}
⊢ evalFrom M s (List.join []) = s

case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
case intro.intro
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ {x}
⊢ evalFrom M s (List.join S) = s
induction' S with a S ih
no goals
case intro.intro.nil
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS✝ : ∀ (y : List α), y ∈ S → y ∈ {x}
hS : ∀ (y : List α), y ∈ [] → y ∈ {x}
⊢ evalFrom M s (List.join []) = s
rfl
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
have ha := hS a (List.mem_cons_self _ _)
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join (a :: S)) = s
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
rw [Set.mem_singleton_iff] at ha
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join S) = s
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join (a :: S)) = s
rw [List.join, evalFrom_of_append, ha, hx]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ ∀ (y : List α), y ∈ S → y ∈ {x}
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join S) = s
apply ih
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
z : List α
hz : z ∈ S
⊢ z ∈ {x}
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ ∀ (y : List α), y ∈ S → y ∈ {x}
intro z hz
no goals
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
z : List α
hz : z ∈ S
⊢ z ∈ {x}
exact hS z (List.mem_cons_of_mem a hz)