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

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

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

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

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

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]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
⊢ dft_aux g ([] ++ ys) visited = dft_aux g ys visited

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

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

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

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

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

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

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

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

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

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

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

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

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