internlm/Lean-Github huggingface dataset:
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
⊢ (if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) = []
Tactic:
split_ifs
Proof state after:
case pos
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
h✝ : hd.1 = x
⊢ hd.2 ++ direct_succ_list tl x = []

case neg
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
h✝ : ¬hd.1 = x
⊢ direct_succ_list tl x = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : hd.1 = x
⊢ hd.2 ++ direct_succ_list tl x = []
Tactic:
case pos c1 =>
  subst c1
  simp at h1
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : ¬hd.1 = x
⊢ direct_succ_list tl x = []
Tactic:
case neg c1 =>
  tauto
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : hd.1 = x
⊢ hd.2 ++ direct_succ_list tl x = []
Tactic:
subst c1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x : List Node), (hd.1, x) ∉ tl) →
    (∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x) → direct_succ_list tl hd.1 = []
h1 :
  ¬hd.1 = hd.1 ∧
    (∀ (x : List Node), (hd.1, x) ∉ tl) ∧ hd.1 ∉ hd.2 ∧ ∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x
⊢ hd.2 ++ direct_succ_list tl hd.1 = []
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x : List Node), (hd.1, x) ∉ tl) →
    (∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x) → direct_succ_list tl hd.1 = []
h1 :
  ¬hd.1 = hd.1 ∧
    (∀ (x : List Node), (hd.1, x) ∉ tl) ∧ hd.1 ∉ hd.2 ∧ ∀ (x : List Node) (x_1 : Node), (x_1, x) ∈ tl → hd.1 ∉ x
⊢ hd.2 ++ direct_succ_list tl hd.1 = []
Tactic:
simp at h1
Proof state after:
no goals
Theorem: not_mem_imp_no_direct_succ
Proof state before:
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : ¬hd.1 = x
⊢ direct_succ_list tl x = []
Tactic:
tauto
Proof state after:
no goals
Theorem: List.erase_diff_len_lt_diff_len
Proof state before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.erase x).diff l2).length < (l1.diff l2).length
Tactic:
simp only [← List.diff_erase]
Proof state after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Theorem: List.erase_diff_len_lt_diff_len
Proof state before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Tactic:
have s1 : x ∈ l1.diff l2 := List.mem_diff_of_mem h1 h2
Proof state after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Theorem: List.erase_diff_len_lt_diff_len
Proof state before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Tactic:
have s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred := List.length_erase_of_mem s1
Proof state after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Theorem: List.erase_diff_len_lt_diff_len
Proof state before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length
Tactic:
simp only [s2]
Proof state after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ (l1.diff l2).length.pred < (l1.diff l2).length
Theorem: List.erase_diff_len_lt_diff_len
Proof state before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
⊢ (l1.diff l2).length.pred < (l1.diff l2).length
Tactic:
have s3 : 0 < (l1.diff l2).length := List.length_pos_of_mem s1
Proof state after:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
s3 : 0 < (l1.diff l2).length
⊢ (l1.diff l2).length.pred < (l1.diff l2).length
Theorem: List.erase_diff_len_lt_diff_len
Proof state before:
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
s1 : x ∈ l1.diff l2
s2 : ((l1.diff l2).erase x).length = (l1.diff l2).length.pred
s3 : 0 < (l1.diff l2).length
⊢ (l1.diff l2).length.pred < (l1.diff l2).length
Tactic:
exact Nat.pred_lt' s3
Proof state after:
no goals
Theorem: dft_aux_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
x : Node
h1 : x ∈ visited
⊢ dft_aux g (x :: stack) visited = dft_aux g stack visited
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
x : Node
h1 : x ∈ visited
⊢ (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) =
    dft_aux g stack visited
Theorem: dft_aux_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
x : Node
h1 : x ∈ visited
⊢ (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) =
    dft_aux g stack visited
Tactic:
simp only [if_pos h1]
Proof state after:
no goals
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys zs : List Node
⊢ dft_aux g (xs ++ ys) zs = dft_aux g ys (dft_aux g xs zs)
Tactic:
induction xs, zs using dft_aux.induct g
Proof state after:
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited✝ : List Node
⊢ dft_aux g ([] ++ ys) visited✝ = dft_aux g ys (dft_aux g [] visited✝)

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

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ :
  dft_aux g (direct_succ_list g x✝ ++ xs✝ ++ ys) (x✝ :: visited✝) =
    dft_aux g ys (dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝))
⊢ dft_aux g (x✝ :: xs✝ ++ ys) visited✝ = dft_aux g ys (dft_aux g (x✝ :: xs✝) visited✝)
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
⊢ dft_aux g ([] ++ ys) visited = dft_aux g ys (dft_aux g [] visited)
Tactic:
case _ visited =>
  simp only [dft_aux]
  simp
Proof state after:
no goals
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g (x :: xs) visited)
Tactic:
case _ visited x xs c1 ih =>
  simp only [dft_aux]
  simp only [if_pos c1]
  simp only [← ih]
  simp
  simp only [dft_aux]
  simp only [if_pos c1]
Proof state after:
no goals
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g (x :: xs) visited)
Tactic:
case _ visited x xs c1 ih =>
  simp only [dft_aux]
  simp only [if_neg c1]
  simp only [← ih]
  simp
  simp only [dft_aux]
  simp only [if_neg c1]
Proof state after:
no goals
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
⊢ dft_aux g ([] ++ ys) visited = dft_aux g ys (dft_aux g [] visited)
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
⊢ dft_aux g ([] ++ ys) visited = dft_aux g ys visited
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
⊢ dft_aux g ([] ++ ys) visited = dft_aux g ys visited
Tactic:
simp
Proof state after:
no goals
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g (x :: xs) visited)
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited =
    dft_aux g ys (if x ∈ visited then dft_aux g xs visited else dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited =
    dft_aux g ys (if x ∈ visited then dft_aux g xs visited else dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
Tactic:
simp only [if_pos c1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
Tactic:
simp only [← ih]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g (xs ++ ys) visited
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g (xs ++ ys) visited
Tactic:
simp
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: (xs ++ ys)) visited = dft_aux g (xs ++ ys) visited
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: (xs ++ ys)) visited = dft_aux g (xs ++ ys) visited
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ (if x ∈ visited then dft_aux g (xs ++ ys) visited
    else dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)) =
    dft_aux g (xs ++ ys) visited
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ (if x ∈ visited then dft_aux g (xs ++ ys) visited
    else dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)) =
    dft_aux g (xs ++ ys) visited
Tactic:
simp only [if_pos c1]
Proof state after:
no goals
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g (x :: xs) visited)
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited =
    dft_aux g ys (if x ∈ visited then dft_aux g xs visited else dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited =
    dft_aux g ys (if x ∈ visited then dft_aux g xs visited else dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
Tactic:
simp only [if_neg c1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
Tactic:
simp only [← ih]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited)
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited)
Tactic:
simp
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: (xs ++ ys)) visited = dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: (xs ++ ys)) visited = dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ (if x ∈ visited then dft_aux g (xs ++ ys) visited
    else dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)) =
    dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)
Theorem: dft_aux_append
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ (if x ∈ visited then dft_aux g (xs ++ ys) visited
    else dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)) =
    dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)
Tactic:
simp only [if_neg c1]
Proof state after:
no goals
Theorem: visited_subset_dft_aux
Proof 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
Proof 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✝
Theorem: visited_subset_dft_aux
Proof 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
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 : 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
Proof state after:
no goals
Theorem: visited_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ dft_aux g [] visited
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ visited
Theorem: visited_subset_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ 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 : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ 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 : 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)
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 : 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]
Proof 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
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 : visited ⊆ dft_aux g stack visited
⊢ visited ⊆ dft_aux g stack visited
Tactic:
exact ih
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)
⊢ visited ⊆ 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 : 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)
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 ⊆ 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 : 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)