Theorem: visited_subset_dft_aux (FOL/Parsing/DFT.lean)

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
⊢ visited ⊆ dft_aux g stack visited
Tactic:
induction stack, visited using dft_aux.induct g
State after:
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
⊢ visited✝ ⊆ 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✝ : visited✝ ⊆ dft_aux g xs✝ visited✝
⊢ visited✝ ⊆ 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✝ : x✝ :: visited✝ ⊆ dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)
⊢ visited✝ ⊆ dft_aux g (x✝ :: xs✝) visited✝

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ dft_aux g [] visited
Tactic:
case _ visited =>
  simp only [dft_aux]
  simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g (x :: stack) visited
Tactic:
case _ visited x stack c1 ih =>
  simp only [dft_aux]
  simp only [if_pos c1]
  exact ih
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ dft_aux g [] visited
Tactic:
simp only [dft_aux]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ visited

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ visited
Tactic:
simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g (x :: stack) visited
Tactic:
simp only [dft_aux]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ 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]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g stack visited

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g stack visited
Tactic:
exact ih
State after:
no goals

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 (x :: stack) visited
Tactic:
simp only [dft_aux]
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 ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)

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 ⊆ 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]
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 ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)

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)
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)

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
State after:
no goals

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
State after:
no goals