internlm/Lean-Github huggingface dataset:
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
simp at h1
Proof state after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
simp only [Set.subset_def]
Proof state after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ ↑xs.toFinset
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ ↑xs.toFinset
Tactic:
simp
Proof state after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ xs
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ xs
Tactic:
intro a a1
Proof state after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a : α
a1 : a ∈ reachable_from_list g xs
⊢ a ∈ xs
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a : α
a1 : a ∈ reachable_from_list g xs
⊢ a ∈ xs
Tactic:
induction a1
Proof state after:
case base
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
a✝ : x✝ ∈ xs
⊢ x✝ ∈ xs

case step
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
e✝ : α × List α
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g xs e✝.1
a_ih✝ : e✝.1 ∈ xs
⊢ x✝ ∈ xs
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
ih : x✝ ∈ xs
⊢ x✝ ∈ xs
Tactic:
case _ _ ih =>
  exact ih
Proof state after:
no goals
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x : α
e : α × List α
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g xs e.1
ih_4 : e.1 ∈ xs
⊢ x ∈ xs
Tactic:
case _ x e ih_1 ih_2 _ ih_4 =>
  exact h1 x e.fst ih_4 e.snd ih_2 ih_1
Proof state after:
no goals
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x✝ : α
ih : x✝ ∈ xs
⊢ x✝ ∈ xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
a x : α
e : α × List α
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g xs e.1
ih_4 : e.1 ∈ xs
⊢ x ∈ xs
Tactic:
exact h1 x e.fst ih_4 e.snd ih_2 ih_1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_reachable_from_list
Proof state before:
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset = reachable_from_list g xs
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs

case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Theorem: list_direct_succ_set_closed_reachable_from_list
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs
Tactic:
apply base_of_reachable_from_list_is_subset_of_reachable_from_list
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_reachable_from_list
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
exact extracted_5 g xs h1
Proof state after:
no goals
Theorem: reachable_from_list_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
have s1 : (dft_aux g stack []).toFinset.toSet = reachable_from_list g (dft_aux g stack []) :=
by
  apply list_direct_succ_set_closed_reachable_from_list g (dft_aux g stack [])
  exact list_direct_succ_set_closed_dft_aux g stack
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
Theorem: reachable_from_list_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
simp only [s1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ reachable_from_list g (dft_aux g stack [])
Theorem: reachable_from_list_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ reachable_from_list g (dft_aux g stack [])
Tactic:
apply reachable_from_list_mono g stack (dft_aux g stack [])
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ stack ⊆ dft_aux g stack []
Theorem: reachable_from_list_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ stack ⊆ dft_aux g stack []
Tactic:
exact stack_subset_dft_aux g stack []
Proof state after:
no goals
Theorem: reachable_from_list_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
Tactic:
apply list_direct_succ_set_closed_reachable_from_list g (dft_aux g stack [])
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g (dft_aux g stack []) ⊆ ↑(dft_aux g stack []).toFinset
Theorem: reachable_from_list_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g (dft_aux g stack []) ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
exact list_direct_succ_set_closed_dft_aux g stack
Proof state after:
no goals
Theorem: dft_aux_eq_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
have s1 : (dft_aux g stack []).toFinset.toSet ⊆ reachable_from_list g stack ∪ [].toFinset.toSet := dft_aux_is_subset_of_reachable_from_list_and_visited g stack []
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack ∪ ↑[].toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Theorem: dft_aux_eq_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack ∪ ↑[].toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
simp only [List.toFinset_nil, Finset.coe_empty, Set.union_empty] at s1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Theorem: dft_aux_eq_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
have s2 : reachable_from_list g stack ⊆ (dft_aux g stack []).toFinset.toSet := reachable_from_list_closed_dft_aux g stack
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
s2 : reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Theorem: dft_aux_eq_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
s2 : reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
exact Set.eq_of_subset_of_subset s1 s2
Proof state after:
no goals
Theorem: dft_iff
Proof state before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : (fun x => s' ∈ x) ↑(dft_aux g S []).toFinset = (fun x => s' ∈ x) (reachable_from_list g S)
⊢ s' ∈ dft g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
simp at this
Proof state after:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ dft g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Theorem: dft_iff
Proof state before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ dft g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
simp [dft, this]
Proof state after:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Theorem: dft_iff
Proof state before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
this : s' ∈ dft_aux g S [] ↔ s' ∈ reachable_from_list g S
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
clear this
Proof state after:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Theorem: dft_iff
Proof state before:
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S ↔ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S → ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'

case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ (∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s') → s' ∈ reachable_from_list g S
Theorem: dft_iff
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ s' ∈ reachable_from_list g S → ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
intro h
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
h : s' ∈ reachable_from_list g S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Theorem: dft_iff
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
h : s' ∈ reachable_from_list g S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
Tactic:
induction h with
| base _ h => exact ⟨_, h, .refl⟩
| step _ _ h1 h2 _ ih =>
  have ⟨_, h3, h4⟩ := ih
  exact ⟨_, h3, .tail h4 ⟨_, h1, h2⟩⟩
Proof state after:
no goals
Theorem: dft_iff
Proof state before:
case mp.base
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
h : x✝ ∈ S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Tactic:
exact ⟨_, h, .refl⟩
Proof state after:
no goals
Theorem: dft_iff
Proof state before:
case mp.step
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
e✝ : α × List α
h1 : e✝ ∈ g
h2 : x✝ ∈ e✝.2
a✝ : reachable_from_list g S e✝.1
ih : ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s e✝.1
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Tactic:
have ⟨_, h3, h4⟩ := ih
Proof state after:
case mp.step
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
e✝ : α × List α
h1 : e✝ ∈ g
h2 : x✝ ∈ e✝.2
a✝ : reachable_from_list g S e✝.1
ih : ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s e✝.1
w✝ : α
h3 : w✝ ∈ S
h4 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) w✝ e✝.1
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Theorem: dft_iff
Proof state before:
case mp.step
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' x✝ : α
e✝ : α × List α
h1 : e✝ ∈ g
h2 : x✝ ∈ e✝.2
a✝ : reachable_from_list g S e✝.1
ih : ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s e✝.1
w✝ : α
h3 : w✝ ∈ S
h4 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) w✝ e✝.1
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s x✝
Tactic:
exact ⟨_, h3, .tail h4 ⟨_, h1, h2⟩⟩
Proof state after:
no goals
Theorem: dft_iff
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ (∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s') → s' ∈ reachable_from_list g S
Tactic:
intro ⟨s, h1, h2⟩
Proof state after:
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
h2 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
⊢ s' ∈ reachable_from_list g S
Theorem: dft_iff
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
h2 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
⊢ s' ∈ reachable_from_list g S
Tactic:
induction h2 with
| refl => exact reachable_from_list.base _ h1
| tail _ h ih =>
  have ⟨_, h3, h4⟩ := h
  exact reachable_from_list.step _ _ h3 h4 ih
Proof state after:
no goals
Theorem: dft_iff
Proof state before:
case mpr.refl
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
⊢ s ∈ reachable_from_list g S
Tactic:
exact reachable_from_list.base _ h1
Proof state after:
no goals
Theorem: dft_iff
Proof state before:
case mpr.tail
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
b✝ c✝ : α
a✝ : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s b✝
h : ∃ l, (b✝, l) ∈ g ∧ c✝ ∈ l
ih : b✝ ∈ reachable_from_list g S
⊢ c✝ ∈ reachable_from_list g S
Tactic:
have ⟨_, h3, h4⟩ := h
Proof state after:
case mpr.tail
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
b✝ c✝ : α
a✝ : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s b✝
h : ∃ l, (b✝, l) ∈ g ∧ c✝ ∈ l
ih : b✝ ∈ reachable_from_list g S
w✝ : List α
h3 : (b✝, w✝) ∈ g
h4 : c✝ ∈ w✝
⊢ c✝ ∈ reachable_from_list g S
Theorem: dft_iff
Proof state before:
case mpr.tail
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
b✝ c✝ : α
a✝ : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s b✝
h : ∃ l, (b✝, l) ∈ g ∧ c✝ ∈ l
ih : b✝ ∈ reachable_from_list g S
w✝ : List α
h3 : (b✝, w✝) ∈ g
h4 : c✝ ∈ w✝
⊢ c✝ ∈ reachable_from_list g S
Tactic:
exact reachable_from_list.step _ _ h3 h4 ih
Proof state after:
no goals
Theorem: DA.memAccepts
Proof state before:
α σ : Type
D : DA α σ
input : List α
⊢ D.accepts input ↔ D.evalFrom D.startingState input ∈ D.acceptingStates
Tactic:
rfl
Proof state after:
no goals
Theorem: NA.memAccepts
Proof state before:
α σ : Type
N : NA α σ
input : List α
⊢ N.accepts input ↔ ∃ s ∈ N.evalFrom N.startingStates input, s ∈ N.acceptingStates
Tactic:
rfl
Proof state after:
no goals
Theorem: NAtoDAisEquiv
Proof state before:
α σ : Type
N : NA α σ
⊢ N.toDA.accepts = N.accepts
Tactic:
ext cs
Proof state after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.accepts cs ↔ N.accepts cs
Theorem: NAtoDAisEquiv
Proof state before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.accepts cs ↔ N.accepts cs
Tactic:
simp only [DA.memAccepts]
Proof state after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔ N.accepts cs
Theorem: NAtoDAisEquiv
Proof state before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔ N.accepts cs
Tactic:
simp only [NA.memAccepts]
Proof state after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Tactic:
simp only [NA.toDA]
Proof state after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∈
      {S | ∃ s ∈ S, s ∈ N.acceptingStates} ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∈
      {S | ∃ s ∈ S, s ∈ N.acceptingStates} ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Tactic:
simp
Proof state after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Tactic:
constructor
Proof state after:
case h.a.mp
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) →
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a.mp
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) →
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates
Tactic:
all_goals
  simp
  intro s a1 a2
  apply Exists.intro s
  tauto
Proof state after:
no goals
Theorem: NAtoDAisEquiv
Proof state before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates
Tactic:
simp
Proof state after:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ ∀ x ∈ N.evalFrom N.startingStates cs,
    x ∈ N.acceptingStates →
      ∃
        s ∈
          { step := N.stepSet, startingState := N.startingStates,
                acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
            N.startingStates cs,
        s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ ∀ x ∈ N.evalFrom N.startingStates cs,
    x ∈ N.acceptingStates →
      ∃
        s ∈
          { step := N.stepSet, startingState := N.startingStates,
                acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
            N.startingStates cs,
        s ∈ N.acceptingStates
Tactic:
intro s a1 a2
Proof state after:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ ∃
    s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs,
    s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ ∃
    s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs,
    s ∈ N.acceptingStates
Tactic:
apply Exists.intro s
Proof state after:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∧
    s ∈ N.acceptingStates
Theorem: NAtoDAisEquiv
Proof state before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∧
    s ∈ N.acceptingStates
Tactic:
tauto
Proof state after:
no goals