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

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

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

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

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

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

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

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
      (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
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 :
  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 stack visited) ⊆ ↑(dft_aux g stack visited).toFinset

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 stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
Tactic:
apply ih
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 visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset

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 visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
Tactic:
trans (x :: stack).toFinset.toSet ∪ visited.toFinset.toSet
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 visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset

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
⊢ ↑(x :: stack).toFinset ∪ ↑visited.toFinset ⊆ ↑stack.toFinset ∪ ↑visited.toFinset

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 visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
Tactic:
exact h1
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 :
  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
⊢ ↑(x :: stack).toFinset ∪ ↑visited.toFinset ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
Tactic:
exact extracted_3 visited stack x c1
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 :
  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:
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 :
  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
      (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

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

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 (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
Tactic:
apply ih
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 (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 (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset

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 (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset
Tactic:
simp only [list_direct_succ_set_cons]
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 (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
⊢ ↑(direct_succ_list g x).toFinset ∪ list_direct_succ_set g visited ⊆
    ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset

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
⊢ ↑(direct_succ_list g x).toFinset ∪ list_direct_succ_set g visited ⊆
    ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset
Tactic:
exact extracted_4 (direct_succ_list g x) visited stack (list_direct_succ_set g visited) x h1
State after:
no goals