internlm/Lean-Github huggingface dataset:
Theorem: visited_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Tactic:
trans (x :: visited)
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ visited ⊆ x :: visited

Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Theorem: visited_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ visited ⊆ x :: visited
Tactic:
simp
Proof state after:
no goals
Theorem: visited_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Tactic:
exact ih
Proof state after:
no goals
Theorem: extracted_1
Proof state before:
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x :: zs ⊆ xs
Tactic:
simp
Proof state after:
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs ∧ zs ⊆ xs
Theorem: extracted_1
Proof state before:
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs ∧ zs ⊆ xs
Tactic:
constructor
Proof state after:
case left
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs

case right
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ zs ⊆ xs
Theorem: extracted_1
Proof state before:
case left
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs
Tactic:
apply Set.mem_of_subset_of_mem h3 h2
Proof state after:
no goals
Theorem: extracted_1
Proof state before:
case right
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ zs ⊆ xs
Tactic:
exact h1
Proof state after:
no goals
Theorem: extracted_2
Proof state before:
α : Type
ws xs ys zs : List α
x : α
h1 : ws ++ ys ⊆ zs
h2 : x :: xs ⊆ zs
⊢ x :: ys ⊆ zs
Tactic:
simp at *
Proof state after:
α : Type
ws xs ys zs : List α
x : α
h1 : ws ⊆ zs ∧ ys ⊆ zs
h2 : x ∈ zs ∧ xs ⊆ zs
⊢ x ∈ zs ∧ ys ⊆ zs
Theorem: extracted_2
Proof state before:
α : Type
ws xs ys zs : List α
x : α
h1 : ws ⊆ zs ∧ ys ⊆ zs
h2 : x ∈ zs ∧ xs ⊆ zs
⊢ x ∈ zs ∧ ys ⊆ zs
Tactic:
tauto
Proof state after:
no goals
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
⊢ stack ⊆ dft_aux g stack visited
Tactic:
induction stack, visited using dft_aux.induct g
Proof state after:
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
⊢ [] ⊆ dft_aux g [] visited✝

case case2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∈ visited✝
ih1✝ : xs✝ ⊆ dft_aux g xs✝ visited✝
⊢ x✝ :: xs✝ ⊆ dft_aux g (x✝ :: xs✝) visited✝

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ : direct_succ_list g x✝ ++ xs✝ ⊆ dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)
⊢ x✝ :: xs✝ ⊆ dft_aux g (x✝ :: xs✝) visited✝
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ [] ⊆ dft_aux g [] visited
Tactic:
case _ visited =>
  simp only [dft_aux]
  simp
Proof state after:
no goals
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ dft_aux g (x :: stack) visited
Tactic:
case _ visited x stack c1 ih =>
  simp only [dft_aux]
  simp only [if_pos c1]
  apply extracted_1 (dft_aux g stack visited) visited stack x ih c1
  exact visited_subset_dft_aux g stack visited
Proof state after:
no goals
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: stack ⊆ dft_aux g (x :: stack) visited
Tactic:
case _ visited x stack c1 ih =>
  simp only [dft_aux]
  simp only [if_neg c1]
  apply extracted_2 (direct_succ_list g x) visited stack (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) x ih
  apply visited_subset_dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Proof state after:
no goals
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ [] ⊆ dft_aux g [] visited
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ [] ⊆ visited
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ [] ⊆ visited
Tactic:
simp
Proof state after:
no goals
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ dft_aux g (x :: stack) visited
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Tactic:
simp only [if_pos c1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ dft_aux g stack visited
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ dft_aux g stack visited
Tactic:
apply extracted_1 (dft_aux g stack visited) visited stack x ih c1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g stack visited
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g stack visited
Tactic:
exact visited_subset_dft_aux g stack visited
Proof state after:
no goals
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: stack ⊆ dft_aux g (x :: stack) visited
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: stack ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: stack ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Tactic:
simp only [if_neg c1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Tactic:
apply extracted_2 (direct_succ_list g x) visited stack (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) x ih
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Theorem: stack_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : direct_succ_list g x ++ stack ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Tactic:
apply visited_subset_dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Proof state after:
no goals
Theorem: extracted_3
Proof state before:
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑(x :: ys).toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
simp only [list_cons_to_set_union]
Proof state after:
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Theorem: extracted_3
Proof state before:
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
apply Set.union_subset
Proof state after:
case sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

case tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Theorem: extracted_3
Proof state before:
case sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
apply Set.union_subset
Proof state after:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

case sr.tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Theorem: extracted_3
Proof state before:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
simp
Proof state after:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ ys ∨ x ∈ xs
Theorem: extracted_3
Proof state before:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ ys ∨ x ∈ xs
Tactic:
right
Proof state after:
case sr.sr.h
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ xs
Theorem: extracted_3
Proof state before:
case sr.sr.h
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ xs
Tactic:
exact h1
Proof state after:
no goals
Theorem: extracted_3
Proof state before:
case sr.tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
exact Set.subset_union_left ys.toFinset.toSet xs.toFinset.toSet
Proof state after:
no goals
Theorem: extracted_3
Proof state before:
case tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
exact Set.subset_union_right ys.toFinset.toSet xs.toFinset.toSet
Proof state after:
no goals
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ ↑(x :: zs).toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp only [list_cons_to_set_union] at h1
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp only [Set.subset_def] at h1
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, x_1 ∈ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, x_1 ∈ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp at h1
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp only [list_cons_to_set_union]
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ({x} ∪ ↑ys.toFinset)
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ({x} ∪ ↑ys.toFinset)
Tactic:
simp only [list_append_to_set_union]
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)
Tactic:
simp only [Set.subset_def]
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ x_1 ∈ ↑xs.toFinset ∪ S, x_1 ∈ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ x_1 ∈ ↑xs.toFinset ∪ S, x_1 ∈ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)
Tactic:
simp
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ (x_1 : Node), x_1 ∈ xs ∨ x_1 ∈ S → x_1 = x ∨ (x_1 ∈ xs ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ (x_1 : Node), x_1 ∈ xs ∨ x_1 ∈ S → x_1 = x ∨ (x_1 ∈ xs ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
Tactic:
intro a a1
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
a : Node
a1 : a ∈ xs ∨ a ∈ S
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
a : Node
a1 : a ∈ xs ∨ a ∈ S
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys
Tactic:
specialize h1 a
Proof state after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x a : Node
a1 : a ∈ xs ∨ a ∈ S
h1 : a ∈ S → (a = x ∨ a ∈ zs) ∨ a ∈ ys
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys
Theorem: extracted_4
Proof state before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x a : Node
a1 : a ∈ xs ∨ a ∈ S
h1 : a ∈ S → (a = x ∨ a ∈ zs) ∨ a ∈ ys
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys
Tactic:
tauto
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
h1 : list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
Tactic:
induction stack, visited using dft_aux.induct g
Proof state after:
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
h1 : list_direct_succ_set g visited✝ ⊆ ↑[].toFinset ∪ ↑visited✝.toFinset
⊢ list_direct_succ_set g (dft_aux g [] visited✝) ⊆ ↑(dft_aux g [] visited✝).toFinset

case case2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∈ visited✝
ih1✝ :
  list_direct_succ_set g visited✝ ⊆ ↑xs✝.toFinset ∪ ↑visited✝.toFinset →
    list_direct_succ_set g (dft_aux g xs✝ visited✝) ⊆ ↑(dft_aux g xs✝ visited✝).toFinset
h1 : list_direct_succ_set g visited✝ ⊆ ↑(x✝ :: xs✝).toFinset ∪ ↑visited✝.toFinset
⊢ list_direct_succ_set g (dft_aux g (x✝ :: xs✝) visited✝) ⊆ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ :
  list_direct_succ_set g (x✝ :: visited✝) ⊆ ↑(direct_succ_list g x✝ ++ xs✝).toFinset ∪ ↑(x✝ :: visited✝).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)) ⊆
      ↑(dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)).toFinset
h1 : list_direct_succ_set g visited✝ ⊆ ↑(x✝ :: xs✝).toFinset ∪ ↑visited✝.toFinset
⊢ list_direct_succ_set g (dft_aux g (x✝ :: xs✝) visited✝) ⊆ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ ↑[].toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g [] visited) ⊆ ↑(dft_aux g [] visited).toFinset
Tactic:
case _ visited =>
  simp at h1
  simp only [dft_aux]
  simp
  exact h1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (x :: stack) visited) ⊆ ↑(dft_aux g (x :: stack) visited).toFinset
Tactic:
case _ visited x stack c1 ih =>
  simp only [dft_aux]
  simp only [if_neg c1]
  apply ih
  simp only [list_direct_succ_set_cons]
  exact extracted_4 (direct_succ_list g x) visited stack (list_direct_succ_set g visited) x h1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ ↑[].toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g [] visited) ⊆ ↑(dft_aux g [] visited).toFinset
Tactic:
simp at h1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g (dft_aux g [] visited) ⊆ ↑(dft_aux g [] visited).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g (dft_aux g [] visited) ⊆ ↑(dft_aux g [] visited).toFinset
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g visited ⊆ ↑visited.toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g visited ⊆ ↑visited.toFinset
Tactic:
simp
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g visited ⊆ {a | a ∈ visited}
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g visited ⊆ {a | a ∈ visited}
Tactic:
exact h1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (x :: stack) visited) ⊆ ↑(dft_aux g (x :: stack) visited).toFinset
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g
      (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset