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

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

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

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

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

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

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

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

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

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

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